M = \np.(n M)(M p)This latter equation is equivalent to the following fixpoint equation:

M = (\mnp.(n m)(m p)) MHence the solution can be obtained by applying the fixpoint operator:

M = Y (\mnp.(n m)(m p))

Iterate = \fzx.zfxIn fact, we then have

Iterate F [n] X = (\fzx.zfx) F [n] X = [n] F X = F^{n}X

[minus] = \xy.Iterate [Predecessor] y xwhere

[minus] [m] [n] = (\xy.Iterate [Predecessor] y x) [m] [n] = Iterate [Predecessor] [n] [m] = [Predecessor]and it is easy to see that^{n}[m]

[Predecessor]^{n}[m] = [m - n] if m >= n [Predecessor]^{n}[m] = [0] if m < n

smallest_prime_factor n = 2 + min k. n mod (k+2) = 0where

We can also semplify the computation by starting the iteration from 2 instead than 0:

smallest_prime_factor n = min k > 1. n mod k = 0where

Following the standard technique illustrated in Lecture 5, we can therefore define:

Spf = (Y F) [2]where

F = \f z k. [if_then_else] ([is_zero] ([mod] z k)) k (f z ([S] k))It remains to define the lambda term

mod = \z k. if z < k then z else mod (z-k) kand, in fixpoint version:

mod = (\f z k. if z < k then z else f (z-k) k) mod>From which, using the fixpoint operator, we can define:

[mod] = Y (\f z k. [if_then_else] ([smaller_than] z k) z (f ([minus] z k) k))We know already how to lambda define

smaller_than = \z k. if k = 0 then false else if z = 0 then true else smaller_than (z-1)(k-1)Hence we can define:

[smaller_than] = Y (\f z k. [if_then_else] ([is_zero] k) [false] ([if_then_else] ([is_zero] z) [true] (f ([Predecessor] z)([Predecessor] k))) )

- Not normalizing. In fact the only possible reductions are:
((\x.xxx)(\x.xx))(\yz.z) -> ((\x.xx)(\x.xx)(\x.xx))(\yz.z) -> ((\x.xx)(\x.xx)(\x.xx))(\yz.z) -> ...

- Weakly normalizing. In fact we have an infinite reduction chain:
(\yz.z)((\x.xxx)(\x.xx)) -> (\yz.z)((\x.xx)(\x.xx)(\x.xx)) -> (\yz.z)((\x.xx)(\x.xx)(\x.xx)) -> ...

and also we have the following finite reduction chain:(\yz.z)((\x.xxx)(\x.xx)) -> \z.z (normal form)

- Strongly normalizing. In fact we have only one possible reduction chain,
and it is finite:
(\yz.z)(\x.xxx)(\x.xx) -> (\z.z)(\x.xx) -> (\x.xx) (normal form)

- False. For instance, take
`M = (\x.xx)`. Then`M`is in normal form (hence strongly normalizing), but`M M = (\x.xx)(\x.xx)`is the term`Omega`(see Lecture 6), which we know is not normalizing. - True. In fact the only possible reduction chains
from
`\x.M`are those of the form\x.M -> \x.M

which are obtained via the xi rule from reduction chains from_{1}-> \x.M_{2}-> \x.M_{3}->...`M`of the form:M -> M

If the first were infinite, so would be the latter._{1}-> M_{2}-> M_{3}->... - True. In fact for every reduction chain from
`N`of the formN -> N

we have, via the Congruence 1 rule, a corresponding reduction chain from_{1}-> N_{2}-> N_{3}->...`M`of the formM = N P -> N

If the first were infinite, so would be the latter._{1}P -> N_{2}P -> N_{3}P ->...We can prove in an analogous way that also

`P`must be strongly normalizing.

- Not possible.
`Y M`cannot be strongly normalizing. In fact we always have the infinite reduction chain:Y M = (\f.(\x.f(xx)(\x.f(xx)) M -> (\x.M(xx)(\x.M(xx)) -> M((\x.M(xx))(\x.M(xx))) -> M(M((\x.M(xx))(\x.M(xx)))) -> ...

- Possible. For example,
`M = \xy.y`satisfies the requirement. In fact we have:Y M = (\f.(\x.f(xx)(\x.f(xx)) M -> (\x.M(xx)(\x.M(xx)) -> M((\x.M(xx))(\x.M(xx))) = (\xy.y)((\x.M(xx))(\x.M(xx))) -> \y.y (normal form)

So`Y M`is weakly normalizing. And clearly it is not strongly normalizing for the argument given in previous point. - Possible. For example,
`M = \x.x`satisfies the requirement. In fact using redexes containing`M`in this case does not help:Y M = (\f.(\x.f(xx)(\x.f(xx)) M -> (\x.M(xx)(\x.M(xx)) -> M((\x.M(xx))(\x.M(xx))) = (\x.x)((\x.M(xx))(\x.M(xx))) -> (\x.M(xx)(\x.M(xx)) -> ...

- Convertible. In fact both
`M`and`N`have normal form`[1]`. - Not convertible. In fact
`M`has normal form`[1]`and`N`has normal form`[0]`. If they were convertible they would have the same normal form.