Fall 2001, CSE 520: Solution of Assignment 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.)
- 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.
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.
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)
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)  ([if_then_else] ([is_zero](f ([Predecessor] z) )  ))
- Solution 2: Apply n times to 0 the "switch function", which converts 0 into 1 and viceversa.
Switch = \z. z (\x.) 
Note that we have
Switch  = 
Switch [n] =  for n > 0
[rem2] = \z. z Switch