ADD [m][n] = (\p q x y. p x (q x y)) [m] [n] = \x y. [m] x ([n] x y) = \x y. xm (xn y) = \x y. xm+n y = [m+n]
MULT [m][n] = (\p q x. p (q x)) [m] [n] = \x. [m] ([n] x) = \x (\w y. w m y) ([n] x) = \x y. ([n] x)m y = \x y. ([n] x ([n] x (...([n] x y)...))) m times = \x y. (xn (xn (...(xn y)...))) m times = [m*n]
[is_zero] = \z. z ([true][false])[true]We have that [is_zero] ([predecessor] [1]) = [is_zero] [0]= [true] and [is_zero] ([predecessor] [2]) = [is_zero] [1] = [false]. If [1] = [2], then by the congruence rule we have [true] = [false], from which we derive, for every term M and N:
[predecessor] = \z. Second (z [aux] (Pair [0] [0]))
M = [true] M N = [false] M N = N.
OR = \a b. [if_then_else] a [true] bwhere [if_then_else] is the encoding of the conditional operator seen in class:
[if_then_else] = \x y z. x y z
Another (simpler, but equivalent) definition is
OR = \a b. a [true] bNote that in both cases OR is short-circuit, i.e. if the first argument is [true], then the second does not need to be evaluated.
[is_empty] [nil] = (\l. l (\x y. [false])) (\z. [true]) = (\z. [true]) (\x y. [false]) = [true]and
[is_empty] ([cons] A L) = (\l. l (\x y. [false])) (\z. z A L) = (\z. z A L) (\x y. [false]) = (\x y. [false]) A L = [false]
append l k = if is_empty l then k else cons (head l) (append (tail l) k)or equivalently, using the lambda notation:
append = (\f l k. if is_empty l then k else cons (head l) (f (tail l) k)) appendThis is a fixpoint equation, hence we can solve it by using the fixpoint operator Y. Therefore we can define
[append] =def= Y (\f l k. ([is_empty] l) k ([cons] ([head] l) (f ([tail] l) k))Where [is_empty], [cons], [head] and [tail] are the lambda terms previously defined.