## Exercise 1

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

## Exercise 2

1. SKK = (\xyz.xz(yz))KK = \z.Kz(Kz) = \z.z = I
2. 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
3. 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 (U32,U33)
```

## Exercise 5

We propose two different solutions:
1. 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]))
```

2. 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]
```