Graphical Lambda Calculator

The lambda calculator is a graphical tool for reducing (untyped) lambda terms. Similar implementations exist, but most are either closed source, use a proprietary license, or are non-graphical (e.g. the lambda calculator of Freek Wiedijk). The latter makes it very hard to read the lambda terms and follow the reduction, which is the reason for developing a graphical lambda calculator. If you have java installed, then you can directly execute the calculator in your browser. This program is free software; you can redistribute it and/or modify it under the GNU General Public License version 2.



System requirements:
  • Java 1.6

Usage:
  • redex positions are marked red
  • left click on a redex position for reducing
  • right click for hiding subterms
  • mouse wheel for zooming
  • drag and drop for moving (left/right/up/down)

Try it online:
Source code: Example Inputs:
  • Curry's fixed point combinator: 
    Init = Y;
Y = \f.(\x.f (x x))(\x.f (x x));
  • Turings's fixed point combinator: 
    Init = Y;
Y = (\x.\f.f (x x f))(\x.\f.f (x x f));
  • Building new fixed point combinators using the generating vector (S(AI))I: 
    Init = Y (S (A I)) I;

S = \a.\b.\c. a c (b c);
I = \a.a;
A = B S;
B = \a.\b.\c. a (b c);
Y = \f.(\x.f (x x))(\x.f (x x));
  • First term in Scott's [75] equation BY = BYS with Curry's fixed point combinator Y: 
    Init = B Y;

S = \a.\b.\c. a c (b c);
B = \a.\b.\c. a (b c);
Y = \f.(\x.f (x x))(\x.f (x x));
  • Second term in Scott's [75] equation BY = BYS with Curry's fixed point combinator Y: 
    Init = B Y S;

S = \a.\b.\c. a c (b c);
B = \a.\b.\c. a (b c);
Y = \f.(\x.f (x x))(\x.f (x x));
  • A lambda term generating the Thue--Morse sequence: 
    Init = Y (\Morse.P A (zip (inv Morse) (tail Morse)));

zip = Y (\z.\l.\r.P (l A) (P (r A) (z (l B) (r B))));
inv = Y (\i.\s. P (s A B A) (i (s B)));
tail = \s.s B;

P = \x.\y.\c.c x y; A = \x.\y.x; B = \x.\y.y;
Y = \f.(\x.f (x x))(\x.f (x x));