Lambda calculus and CL reduction tool by Freek Wiedijk

Freek Wiedijk developed a tool for λ- and CL-reduction. It is currently used in the course Term Rewiting Systems at the VU.

• Mac OS X executable file
  Instructions for installation on a Mac:
  • Transfer the file to your Mac OS X machine as lambda1, in your home directory
  • In a terminal, give the command "chmod a+x lambda1".
  • For execution of the tool type "./lambda1".
• source code
  In the presence of OCAML this source code file can be compiled, under UNIX, for example by the command
  • ocamlopt lambda1.ml -o lambda1

How to use the λ- and CL-tool

     I=\x.x
     K=\xy.x
     S=\xyz.xz(yz)
     B=\xyz.x(yz)
     C=\xyz.xzy
     W=\xy.xyy
     1=\xy.xy
     Y=\f.(\x.f(xx))\x.f(xx)
     T=\xy.x
     F=\xy.y
     D=\x.xx
     J=\abcd.ab(adc)
     C'=JII
     .li leftmost innermost
     .lo leftmost outermost [default]
     .po parallel outermost
     .gk gross knuth
     .l lambda reduction [default]
     .c combinator reduction
     .ex eta reduction
     .in no eta reduction [default]
     ./ fold combinators
     ./IKS translate to IKS
     .//IKS translate to IKS using eta
     ./IKBCS translate to IKBCS
     .//IKBCS translate to IKBCS using eta
     ./IJK translate to IJK
     .//IJK translate to IJK using eta
     .. normalize
     .<< previous input term
     .< previous term
     .> next term
     .>> next input term
     .? help
     . exit

Subsequently you can try to type CL-terms like ISIS or lambda-terms like (\xx.xx)(\xy.xy) and create a reduction sequence by continuing to type return-return-return-... .

Last modified: Wed Apr 13 15:04:03 CEST 2005