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:
- z: λs.λz.z\lambda s . \lambda z . zλs.λz.z
- s z: λs.λz.s z\lambda s . \lambda z . s \; zλs.λz.sz
- 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.
Top comments (0)