Problem 1 [6pt] For the following term:
(λx. λy. y x) (λz. y)
a) Calculate its free variables FV() and connect all bound variables to their definitions with lines. For
example, the bound variables for this term, λx. x x y should be λ x. x x y.
b) Do reduction on the term until no more β-reduction is possible. Show every steps.
Problem 2 [8pt] In hw6, you have defined a few functions on church numerals on paper. Please implement
ISZERO, PRED and MINUS functions in hw7.rkt file that works on church numerals. We have already
implemented some helper functions to help you get started with your implementation. Your implementation
can only use (lambda …), function application of the form (a b c) and predefined constants/constructs such
as TRUE, FALSE, IF, PAIR, LEFT, RIGHT, SUCC, PLUS and ZERO.
The ENCODE and DECODE functions are strictly for testing. Your implementation should not involve
either of these two functions.
a) (2pt) Define a function ISZERO so that given a church numeral n, it returns TRUE (the encoding of true)
if n = 0; FALSE (the encoding of false) if n 6= 0.

DETAILED ASSIGNMENT

20210316054449hw7__3_