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 start. What's a fixed point? When a function f(x)f(x)f(x) has xxx can make f(x)=xf(x) = xf(x)=x then we say xxx is the fixed point of fff. Now we can get start to derive one.

In lambda calculus, Peano's number can be represented as:

1. z: λs.λz.z\lambda s . \lambda z . zλs.λz.z
2. s z: λs.λz.s  z\lambda s . \lambda z . s \; zλs.λz.sz
3. s s z: λs.λz.s  (s  z)\lambda s . \lambda z . s \; (s \; z)λs.λz.s(sz)

Then s (successor) can be found.

s≐λn.λs.λz.s  (n  s  z)s \doteq \lambda n . \lambda s . \lambda z . s \; (n \; s \; z)s≐λn.λs.λz.s(nsz)

With s , we can define add , idea is simple: find number nnn successor of mmm.

add≐λn.λm.m  (s  n)add \doteq \lambda n . \lambda m . m \; (s \; n)add≐λn.λm.m(sn)

We can check a number is zero or not(assume true/false already defined) and predecessor.

iszero≐λn.n  (λx.false)  truepredecessor≐λn.λs.λz.second  (n  (wrap  f)<true,x>)wrapf≐λp.<false,if  (first  p)  (second  p)  (f  (second  p))>iszero \doteq \lambda n . n \; (\lambda x . false) \; true \
predecessor \doteq \lambda n . \lambda s . \lambda z . second \; (n \; (wrap \; f) <true, x>) \
wrap f \doteq \lambda p . <false, if \; (first \; p) \; (second \; p) \; (f \; (second \; p))>iszero≐λn.n(λx.false)truepredecessor≐λn.λs.λz.second(n(wrapf))wrapf≐λp.

p.s. represents a pair, first is a, and second is b. Assuming first and second already bound.

With these, we can define mult

mult≐λn.λm.if  (iszero  n)  0  (add  m  (mult  (predecessor  n)  m))mult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (mult \; (predecessor \; n) \; m))mult≐λn.λm.if(iszeron)0(addm(mult(predecessorn)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≐λn.λm.if  (iszero  n)  0  (add  m  ((t  t)  (predecessor  n)  m))mkmult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; ((t \; t) \; (predecessor \; n) \; m))mkmult≐λn.λm.if(iszeron)0(addm((tt)(predecessorn)m))

How to use this?

mult≐(mkmult  mkmult)mult \doteq (mkmult \; mkmult)mult≐(mkmultmkmult)

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≐λt.t(mk  t)mk \doteq \lambda t . t (mk \; t)mk≐λt.t(mkt)

Oops, but wait, we can repeat the pattern.

mkmk≐λk.λt.t  ((k  k)  t)mkmk \doteq \lambda k . \lambda t . t \; ((k \; k) \; t)mkmk≐λk.λt.t((kk)t)

Then we have mk, for sure.

mk≐(mkmk  mkmk)mk \doteq (mkmk \; mkmk)mk≐(mkmkmkmk)

With mk we can have mult by a different way.

mkmult′≐λn.λm.if  (iszero  n)  0  (add  m  (t  (predecessor  n)  m))mult≐(mkmkmult′)mkmult' \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (t \; (predecessor \; n) \; m))
mult \doteq (mk mkmult')mkmult′≐λn.λm.if(iszeron)0(addm(t(predecessorn)m))mult≐(mkmkmult′)

mk can find out 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. At the end, thanks for the read and have a nice day.