33 lines
850 B
Markdown
33 lines
850 B
Markdown
# lambda
|
|
|
|
Basic untyped lambda calculus interpreter. Running the program will drop you
|
|
into a repl where you can type an expression in lambda calculus. Upon parsing
|
|
this, you will be put into a new repl, where pressing enter will beta reduce
|
|
the current term by one step. You can exit this by typing 'q' and pressing
|
|
enter. I would recommend using `rlwrap`, as the repls are rather basic.
|
|
|
|
Here's an example interaction showing each step of the beta reduction.
|
|
```
|
|
> (lambda x y z. x z (y z)) (lambda x y. x) (lambda x y. x)
|
|
(λx y z. x z (y z)) (λx y. x) (λx y. x)
|
|
?
|
|
(λy z. (λx y. x) z (y z)) (λx y. x)
|
|
?
|
|
λz. (λx y. x) z ((λx y. x) z)
|
|
?
|
|
λz. (λy. z) (λy. z)
|
|
?
|
|
λz. z
|
|
? q
|
|
```
|
|
|
|
It will even handle name collisions and automatically alpha-rename.
|
|
```
|
|
> (lambda x y. x y) (lambda x. y)
|
|
(λx y. x y) (λx. y)
|
|
?
|
|
λz. (λx. y) z
|
|
?
|
|
λz. y
|
|
? q
|
|
```
|