Review of Lambda Combinators

Topic

λ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))