Lambda Calculus REPL:

A simple REPL for lambda calculus.

Screencast

Run

To run the REPL, just type in:

cabal run

Examples:

To switch normal order reduction strategy
:n
(λx.xx)((λxy.yx)y)
→(λx.xx)((λxy.yx)y)
→((λxy.yx)y)((λxy.yx)y)
→(λa.ay)((λxy.yx)y)
→((λxy.yx)y)y
→(λa.ay)y
yy

:a
(λx.xx)((λxy.yx)y)
→(\x.xx)((λxy.yx)y)
→(λx.xx)(λa.ay)
yy

— Alpha Equivalence
:eq (\x.xx) (\y.yy)
:eq (\xy.xy) (\yx.yx)
:eq (\xy.xy) (\yx.yy)

— Convert to Debruijn Index
:d (\xysz.xs(ysz))
:d (\x.x(\y.xx))

— Explain
(λx.(λy.xy))y (\x.xx)

TODO
:eq y x not equal