###
*Fall 2001, CSE 520: Solution of Assignment 1*

## Exercise 1

- No (y and z are free)
- No (y occurs free in the first term, but not in the second)
- Yes, by using alpha conversion
- Yes, by using beta conversion two times
- Yes, by usingbeta conversion two times, and Congruence 1
- No, \z.y can be obtained from (\xz.x)((\w.w)y), but note that the structure is different
- Yes, by using beta conversion two times, and Congruence 1
- Yes, by using beta conversion three times, xi and Congruence 2
- Yes, because both are convertible to \z.z. We need to use the same rules as above, plus symmetry
- No, because \z.z is not convertible to \xz.xz. (We would need the eta rule or the extensionality axiom.)

## Exercise 2

` SKK = (\xyz.xz(yz))KK = \z.Kz(Kz) = \z.z = I`
` S(KS)K = (\xyz.xz(yz))(KS)K = \z.(KS)z(Kz) = \z.S(Kz) = \z.(\xyw.xw(yw))(Kz) = \zyw.Kzw(yw)) = \zyw.w(yw)) = B`
`S(KI) = (\xyz.xz(yz))(KI) = \yz.(KI)z(yz) = \yz.(KI)z(yz) = \yz.I(yz) = \yz.yz` and
`BI = (\xyz.x(yz))I = \yz.I(yz) = \yz.yz`.

## Exercise 3

Given two arbitrary terms M and N, we prove that we can derive M = N. Consider the terms P = \x.M and Q = \y.N.
If \xy.xy = \xy.yx holds, then we can also derive , by the congruence 1 rule, that (\xy.xy)PQ = (\xy.yx)PQ.
Then, by applying beta conversion (two times) on both sides we get PQ = QP, namely (\x.M)(\y.N) = (\x.N)(\y.M).
By applying beta conversion on both sides, we derive M = N.
## Exercise 4

The definition of `exp(m,n)` can be given by primitive recursion as follows:
exp(0,n) = 1
exp(m+1,n) = exp(m,n)*n

The functions g and f need to be defined as follows:
g(n) = 1, hence g = S o Z
h(m,exp(m,n),n) = exp(m,n)*n, hence h = times o (U^{3}_{2},U^{3}_{3})

## Exercise 5

We propose two different solutions:
**Solution 1**: The standard approach based on the recursive definition of `rem2`.
The definition of `rem2` can be given by primitive recursion as follows:

rem2(0) = 0
rem2(n+1) = if rem2(n) = 0 then 1 else 0

Hence, it is sufficient to define [rem2] = Y [F], where Y is the fixpoint operator and
F is the function:
F = \f.\z. if z = 0 then 1 else if f (z-1) = 0 then 1 else 0

Using the functions defined in class and in the lecture notes, we have
[F] = \f.\z. [if_then_else] ([is_zero] z) [1] ([if_then_else] ([is_zero](f ([Predecessor] z) ) [1] [0]))

**Solution 2**: Apply n times to 0 the "switch function", which converts 0 into 1 and viceversa.
Define

Switch = \z. z (\x.[0]) [1]

Note that we have
Switch [0] = [1]
Switch [n] = [0] for n > 0

Finally define
[rem2] = \z. z Switch [0]