9/17/19
λx.x (* IDENTITY *)
λx.(x x) (* SELF APPLICATION *)
λx.λy.λz.(x (y z)) (* COMPOSITION *)
λfirst.λsecond.λargument.(first (second argument))) (* composition, again *)
λx.λy.x (* TRUE *)
λfirst.λsecond.first (* true, again *)
λx.λy.y (* FALSE *)
λfirst.λsecond.second (* false, again *)λx.λy.λz.((x y) z) (* IFTHENELSE *)
λcondition.λthen.λelse.((condition then) else) (* if then else, again *)
Lists
λx.T (* NIL, the empty list*)
λlist.(list λh.λt.F) (* NULLQ -- the empty list predicate *)
λa.((a h) t) (*A PAIR*)
λpairAccessor.((pairAccessor firstArg) secondArg) (*A PAIR*)λa.((a h) t) (*A LIST WITH HEAD h AND TAIL h)*)
λh.λt.λa.((a h) t) (*A CONSTRUCTOR TO MAKE A LIST WITH HEAD h AND TAIL t*)
λx.λy.x (*AN ACCESSOR FOR HEAD*)
λx.λy.y (*AN ACCESSOR FOR TAIL*)
Numbers
λx.T (*0 (also NIL) *)
λlist.(list λhλt.F) (* EQ0 (also NULLQ)*)
λx.λy.y (*PREDECESSOR (also AN ACCESSOR FOR TAIL)*)
λt.λa.((a 0) t) (*SUCCESSOR of number t (also A CONSTRUCTOR TO MAKE A LIST WITH HEAD 0 AND TAIL t)*)
Fixpoint
λh.(λx.(h (x x)) λx.(h (x x))) (* Y the fixpoint combinator *)
This satisfies, for any H
(Y H) = (H (Y H))