Pure Lambda Calculus Interpreter.
This is an interpreter made for anyone who might be interested in experimenting with the pure lambda calculus.
Supports environment variables for lambda-terms, showing the contents of an environtment variable, displaying the list of environment variables, checking for alpha-equivalence, checking for beta-normal-form, evaluating n-steps at a time (in-place, for environment variables), applicative-order reduction and normal-order reduction.
I'll be adding a couple more features, eventually. Also, the parser is not the greatest as some parenthesis, which could be left out, can't be omitted. I'll fix that (eventually as well).
Haskell and Cabal should both be installed.
cabal build
cabal run
Type :?, :h or :help for help within the program.
| Syntax | Semantics |
|---|---|
| \x.t | An abstraction. If x appears in t, it has to be bound to the most recent abstraction of x |
| t1 t2 | An application. If t1 is an abstraction \x.t11, then (t1 t2) is a redex, and t2 may replace any x within t11 that may be bound to the abstraction |
| x | A variable. It can contain any combination of lowercase characters and end in any number of primes. It can either be bound or free, in which case (the latter) it's name can't change and neither can it be replaced due to a reduction of a redex. |
The λ (lambda) symbol is a synonym of \.
Applications are conventionally left associative, and abstractions right associative.
Abstracted variables can be curried, which means that \x.\y.\z.(x z) (y z) is the same as \x y z.(x z) (y z).
Do not forget to report any bugs. Contact me, otherwise you can create a new issue on this repository. Thanks!