Fall 2000, CSE 520: Solution of MT exam
A possible solution is
M =def= Y (\m n p. n m (p n))
In fact the equation
M N P = N M (P N)
is satisfied if the equation
M = (\m n p. n m (p n)) M
is satisfied. This is a fixpoint equation that can be solved
by applying the fixpoint operator Y.
One solution is to give a recursive definition and then
make the usual fixpoint construction. Note in fact that factorial can be defined
factorial(0) = 1
factorial(n) = n * factorial(n-1) if n > 0
hence we can define
[factorial] =def= Y (\f x. [if_then_else] ([is_zero] x)  ([mult] x (f ([Predecessor] x))))
- False: Omega has an infinite chain of reductions:
Omega -> Omega -> Omega -> ...
Hence, for any M, also the term M Omega has an infinite chain of reductions:
M Omega -> M Omega -> M Omega -> ...
- True. For instance,
[true]  Omega -> (\y. ) Omega -> Omega
hence it is sufficient to consider M = [true] .
- False. Following the same resoning as in (1) we get an infiite chain
of reductions also for Omega M:
Omega M -> Omega M -> Omega M -> ...
- False. Even if M has a normal form, Omega M does not have a
normal form. In fact, Omega only reduces to itself, so Omega M can never
reduce to a lambda redex. Therefore Omega and M reduce independently, and,
even if M reduces to a normal form N, the Omega in front keeps reducing to
Omega M -> ... -> Omega N -> Omega N -> Omega N -> ...
- Not typeable
- (A -> (A -> B)) -> A -> B
- ((A -> B) -> (B -> C)) -> (A -> B) -> A -> C
- (B -> A) -> A is not inhabited. In fact, this type, seen as a formula, is not classically valid.
In fact for B = true and A = false the formula is false.
- A -> B -> B -> A is inhabited. One term with this type is \x y z. x.
note that it is not the principal type, though. The principal type is A ->
B -> C -> A
- (A -> B) -> B -> A is not inhabited. For A = false and B = true the
formula is false.