A toy calculator for playing with the Lambda Calculus I made a while ago. Uses de Bruijn representation of lambda terms internally to avoid 伪-headaches. Written in Haskell. Still very much incomplete and subject to whatever changes I feel like making.
The term will be silently 伪-converted so that variables are chosen in alphabetical order.
>> (位xy.x)(位x.x)
(位ab.a)(位a.a)
Use the :leftmost or :lm command to perform leftmost reduction.
>> :leftmost (位xy.x)(位x.x)
位ab.b
>> :lm (位x.xx)(位x.xx)
(位a.aa)(位a.aa)
You can't leftmost reduce something which is in 尾-normal form.
>> :lm (位x.xx)
(尾-normal) 位a.aa
Use :betanormal or :bn to find the 尾-normal form.
>> :bn (位x.xx)(位x.x)
位a.a
Use :debruijn or :db to view the De Bruijn notation.
>> :debruijn (位x.xx)(位x.xx)
(位 0 0) (位 0 0)
>> :db (位x.xx)(位xyz.xz)(位x.xx)
(位 0 0) (位 位 位 2 0) (位 0 0)
Compile with ghc -O2 main.hs -o lambda and run ./lambda. It is often a good idea to run it with rlwrap (use rlwrap ./lambda) so you can edit what you write.