We have used the pure -calculus to construct natural numbers and encoded some operations on them. In such encoding, a number n is encoded as a function f z. fn z (denoted as n). In this problem, we will dene more useful operations on numbers. If you get stuck in any question, try to proceed by assuming the previous function is properly dened. You can reuse any encoding given in lectures and previous questions.

a) Dene a function ISZERO in -calculus, so that given a number n, it returns TRUE (the encoding of true) if n = 0; FALSE (the encoding of false) if n 6= 0. Hint: try to dene two terms so that applying the second term multiple times to the rst term returns FALSE; otherwise, the application returns TRUE. 1/2

b) Dene a function PRED in -calculus, so that given a number n, the function returns its predecessor, assuming the predecessor of 0 is 0 Hint: follow the idea in Problem 4a. You might need to use PAIR.

c) Use your encoding of PRED to dene a subtraction function MINUS, so that MINUS n1 n2 returns n1 n2 when n1 n2, and 0 otherwise.

d) Recall that in we have dened MULT (the encoding of ) basedon PLUS (the encoding of +): MULT, n1 n2. (n1 (PLUS n2) 0). Try to dene MULT on Church numerals without using PLUS (replacing PLUS with an equivalent term under / reduction doesnt count as a solution). Hint: by denition, we have n f = z. fn z, which can be interpreted as repeating an arbitrary function f for n times to parameter z. The goal here is to repeat an arbitrary function f for n1 n2 times (according to the denition of n1 n2).