expr :=  identifier                           ::   ident
       | (L identifier. expr)                 ::   sub { my $x=shift; expr}
       | (expr expr)              : apply     ::   expr(expr)

left associative:
    f g x  ==   (f g) x                       ::   f(g(x))

free-occurence:
    - V,   V is an indentifier -> V is occurring freely
    - (L V. E),  free in E, except those of V
    - (E E')   : free are free in E, and free in E'

bound:
    - (L V. E),  V is bound in E by L
    

E[V:=W]  : every free occurence of V is replaced with W

alpha-conversion
    (L V. E) == (L W. E[V:=W])     if W not freely in E, and not bound in E

beta-reduction
    ( (L V. E) E') ==   E[V:=E']   if all free in E'  are free in E[V:=E']

eta-conversion
    (L x. f x)  = f    if x is not free in f


l(x){ l(y){x-y} }   = l(x,y){x-y}
    * x-y         : x,y are free
    * l(y){x-y}   : x is free, y is bound




(L x.x x)  o-combinator
( (L x. x x) (L x. x x) )  : O

( (L x. x x x) (L x. x x x) )  : O2


church numerals:

0 = (L f. L x. x)
1 = (L f. L x. f x)
2 = (L f. L x. f f x)
n = (L f. L x. f .. f f x)


SUCC := L n f x. f ((n f) x)
PLUS := L m n f x. n f (m f x)
MULT := L m n. m (PLUS n) 0
MULT := L m n f. m (n f)
PRED := L n f x. n (L g h. h (g f)) (L u. x) (L u. u) 
PRED := L n. n (L g k. (g 1) (L u. PLUS (g k) 1) k) (L v. 0) 0


TRUE := L x y. x
FALSE := L x y. y
AND := L p q. p q FALSE
OR := L p q. p TRUE q
NOT := L p. p FALSE TRUE
IFTHENELSE := L p x y. p x y

ISZERO := L n. n (L x. FALSE) TRUE

Y = L g. (L x. g (x x)) (L x. g (x x))