This is a simple REPL shell for untyped lambda expressions. I wrote it mostly for playing around a little bit with the lambda calculus. Some parts of it are wildly inefficient, but it is fine for education purposes.
The shell can evaluate lambda expressions, assignments and macros.
There are builtin terms SUCC and NIL to create natural numbers using church numerals:
[λ] @usestd
@usestd
[λ] one := SUCC NIL
one := SUCC NIL
[λ] two := SUCC (SUCC NIL)
two := SUCC (SUCC NIL)
[λ] !normalize (ADD one two)
\f . \x . f (f (f x))
You can select different reduction strategies at runtime:
[λ] @usestd
@usestd
[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
(\q . (\y . q) TRUE) FALSE
(\q . q) FALSE
FALSE
[λ] @set strategy normal
@set strategy normal
[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
TRUE FALSE TRUE
(\y . FALSE) TRUE
FALSE
- normal (leftmost-outermost) and applicative (leftmost-innermost) reduction strategies
- capture-avoiding substitution
- simple constructs provided via builtins
- macros for processing lambda terms
You can find more information about installation and building from source here.