This assignment has to be solved individually and handed in using the fire system before Monday 23 Nov (i.e. Sunday midnight). Please give me a text file or pdf. No scanned hand writings!
The predecessor function for Church numerals is not trivial:
zz == pair 0 0
ss == \p. pair (snd p) (succ (snd p))
prd == \n. fst (n ss zz)
Here we can interpret the == sign as an explicit definition in the meta language. To the left of the == sign we have a name and to the right an expression in lambda-calculus.
Explain why this is a correct definition! You don't have to give a strict mathematical proof (using induction), it is enough if you give the intuition.
Use prd to define a subtraction function in lambda calculus. Explain it! There is no need to give a proof of its correctness.
Define a function equal that tests two numbers for equality and returns a Church boolean. Explain it! No need to give a proof of its correctness.
There is a definition of the substitution operation in John Harrison's lecture notes. Give a simplified definition of d[x:=e] (the result of substituting the expression e for all free occurrences of x in d) for the case when the expression e is closed (i.e. contains no free variables). Explain also why this simplification can be made.