This is a small lambda calculus interpreter, it contains no built-in functions, datatypes etc. so you have to define everything yourself!
The only small QoL feature is that natural numbers (1, 2, ...) get parsed to their respective church encoding (\f.\a.f a, \f.\a.f (f a)), ...) and the interpreter tries to parse results as some standard church encodings.
For best results you should run it using Nix, but using plain cabal should work in most cases as well!
To run the interpreter just do
cabal run lambda
A lambda calculus term can be one of:
- a variable
- application of two terms
- lambda abstracion
This interpreter can handle lambda-terms and also supports declarations (assigning a name to a lambda-term). Following example should showcase all features:
> i = \x.x
> s = \x.\y.\z.x z (y z)
> k = \x.\y.x
> s k k x
s k k x
(\x.\y.\z.x z (y z)) k k x
(\v$0.\v$1.k v$1 (v$0 v$1)) k x
(\v$0.k v$0 (k v$0)) x
k x (k x)
(\x.\y.x) x (k x)
(\v$0.x) (k x)
x
Behind the scenes the interpreter just exhaustively applies beta- and eta-reductions.
You can supply a prelude (a collection of functions that are loaded when the interpreter is started) to the interpreter in a file prelude.lmd.