Perhaps this page is now superseded by the Mairson constructs.
Safalra shows some ways to do ‘ordinary code’ in the λ calculus. We repeat the stuff here.
Two truth values K = true = (λab.a) and H = false = (λab.b) play a double role. If x is a truth value then (x p q) evaluates to p if x=true and otherwise to q. Both values are calculated and this is usually bad. The construct (x (λd.p) (λe.p) i) evaluates only one of p or q and the other expression is unevaluated. The identifier d should not appear in p freely, nor e in q. The value of i is ignored but that ID must be in scope. The primordial zero test z produces either H or K and other predicates should as well.
The familiar LISP or Scheme value (cons x y) may be had by (λz.zxy). If c is such a value then (c K) is (car c) and (c H) is (cdr c). If you want car and cdr functions then (λx.xK) and (λx.xH) serve. We will also need a nil value and matching null? predicate.
Following Safalra we try the following:
pair = (λabf.fab) first = (λp.p(λab.a)) second = (λp.p(λab.b)) (first (pair 3 5)) = ((λp.p(λab.a)) ((λabf.fab) 3 5)) => 3 (second (pair 3 5)) = ((λp.p(λab.b)) ((λabf.fab) 3 5)) => 5This plan does not allow for lists of unknown length. For those Safalra proposes the following:
nil = (λfx.x) cons = (λalfx.fa(lfx)) car = (λl.l(λab.a)i) cdr = (λl. car (l(λab. cons (cdr b)(cons a (cdr b)))(cons nil nil))) null? = (λl.l(λab.K)H)Running these seems to require a nest of definitions; we use the second letter of each name as our ident:
((λioau.((λd. 42 ; app ) (λl.a(l(λab.o(db)(oa(d b)))(oii))))) (λfx.x) ; i for nil (λalfx.fa(lfx)) ; o for cons (λl.l(λab.a)i) ; a for car (λl.l(λab.K)H) ; u for null? )Reduction:
(cons 3 5) = ((λalfx.fa(lfx)) 3 5) (car (cons 3 5)) = ((λl.l(λab.a)i) ((λalfx.fa(lfx)) 3 5)) => number as function ((λalfx.fa(lfx)) 3 5(λab.a)i) ((λlfx.f3(lfx)) 5 (λab.a)i) ((λfx.f3(5fx)) (λab.a)i) ((λfx.f3(5fx)) K i) ((λx.K3(5Kx)) i) (K3(5Ki))3 ; but with (5Ki) evaluated and discarded. Perhaps Safalra assumes lazy evaluation. I think that list semantics in the λ calculus should not allow calling a list element.