How to find mk fixed point
This article is about how to get a fixed point in lambda calculus(utlc) system, if you didn't familiar with it, you can read NOTE: what is lambda calculus to get started. What's a fixed point? When a function \(f(x)\) has \(x\) can make \(f(x) = x\) then we say \(x\) is the fixed point of \(f\). Now we can get started to derive one.
In lambda calculus, Peano's number can be represented as:
- z: \(\lambda s . \lambda z . z\)
- s z: \(\lambda s . \lambda z . s \; z\)
- s s z: \(\lambda s . \lambda z . s \; (s \; z)\)
Then *s*(successor) can be found.
\[ s \doteq \lambda n . \lambda s . \lambda z . s \; (n \; s \; z) \]
With s, we can define add, idea is simple: find number \(n\) successor of \(m\).
\[ add \doteq \lambda n . \lambda m . m \; (s \; n) \]
We can check a number is zero or not(assume true/false already defined) and predecessor.
\[
iszero \doteq \lambda n . n \; (\lambda x . false) \; true \\
predecessor \doteq \lambda n . \lambda s . \lambda z . second \; (n \; (wrap \; f)
p.s. <a, b> represents a pair, first is a, and second is b. Assuming
first and second already bound.
With these, we can define mult
\[ mult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (mult \; (predecessor \; n) \; m)) \]
However, lambda didn't have a name(all \(\doteq\) was name tag for human
only, not allowed in lambda calculus), so we cannot refer to mult in
mult! But we can have a proper version.
\[ mkmult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; ((t \; t) \; (predecessor \; n) \; m)) \]
How to use this?
\[ mult \doteq (mkmult \; mkmult) \]
The key was a recursively expanded definition for mult. t t always
take a mkmult and make more mkmult. Thus, can we generalize this?
\[ mk \doteq \lambda t . t (mk \; t) \]
Oops, but wait, we can repeat the pattern.
\[ mkmk \doteq \lambda k . \lambda t . t \; ((k \; k) \; t) \]
Then we have mk, for sure.
\[ mk \doteq (mkmk \; mkmk) \]
With mk we can have mult in a different way.
\[ mkmult' \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (t \; (predecessor \; n) \; m)) \\ mult \doteq (mk \; mkmult') \]
mk can find out the fixed point of any function. Which means
M (mk M) = (mk M). mk is not the only fixed point, the most famous
fixed point is Y combinator, but I'm not going to talk about it here. In
the end, thanks for the read and have a nice day.