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.