ADD [m][n] = (\p q x y. p x (q x y)) [m] [n] = \x y. [m] x ([n] x y) = \x y. x ^{m}(x^{n}y)= \x y. x ^{m+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. (x ^{n}(x^{n}(...(x^{n}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.

- Observe that the equation M N P = P (M P) is satisfied if the equation M = (\x y z. z (x z)) M is satisfied. Then define M =def= Y (\x y z. z (x z)) where Y is the fixpoint operator seen in class.
- Observe that the equation M N P P = M P N is satisfied if the equation
M = (\x y z w. x z y) M is satisfied. Then define M =def= Y (\x y z w. x z y)

Alternatively, consider that the equation M N P P = M P N is satisfied if the equation (\x y z. x z y y) M = M is satisfied. Then define M =def= Y (\x y z. x z y y).

Note that the two definitions are not equivalent, but they are both solutions.

- [nil] =def= \z. [true]
- [cons] =def= Pair = \x y z. z x y
- [head] =def= First = \p. p [true]
- [tail] =def= Second = \p. p [false]
- [is_empty] =def= \l. l (\x y. [false])

[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.