How to find mk fixed point
Published: 2020-11-19 01:09:48

---
title: How to find mk fixed point
published: true
date: 2020-07-26 00:00:00 UTC
tags: 
canonical_url: https://dannypsnl.github.io/blog/2020/07/26/cs/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](/blog/2020/01/01/cs/note-what-is-lambda-calculus/) to get start. What's a fixed point? When a function <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x)</annotation></semantics></math>f(x) has <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>x can make <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">f(x) = x</annotation></semantics></math>f(x)=x then we say <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>x is the fixed point of <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>f. Now we can get start to derive one.

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

1. z: <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi>z</mi></mrow><annotation encoding="application/x-tex">\lambda s . \lambda z . z</annotation></semantics></math>λs.λz.z
2. s z: <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi>s</mi><mtext>  </mtext><mi>z</mi></mrow><annotation encoding="application/x-tex">\lambda s . \lambda z . s \; z</annotation></semantics></math>λs.λz.sz
3. s s z: <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi>s</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>s</mi><mtext>  </mtext><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\lambda s . \lambda z . s \; (s \; z)</annotation></semantics></math>λs.λz.s(sz)

Then **s** (successor) can be found.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>s</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi>s</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>n</mi><mtext>  </mtext><mi>s</mi><mtext>  </mtext><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">s \doteq \lambda n . \lambda s . \lambda z . s \; (n \; s \; z)</annotation></semantics></math>s≐λn.λs.λz.s(nsz)

With **s** , we can define **add** , idea is simple: find number <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>n successor of <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi></mrow><annotation encoding="application/x-tex">m</annotation></semantics></math>m.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>a</mi><mi>d</mi><mi>d</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>m</mi><mi mathvariant="normal">.</mi><mi>m</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>s</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">add \doteq \lambda n . \lambda m . m \; (s \; n)</annotation></semantics></math>add≐λn.λm.m(sn)

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

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>i</mi><mi>s</mi><mi>z</mi><mi>e</mi><mi>r</mi><mi>o</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>n</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>λ</mi><mi>x</mi><mi mathvariant="normal">.</mi><mi>f</mi><mi>a</mi><mi>l</mi><mi>s</mi><mi>e</mi><mo stretchy="false">)</mo><mtext>  </mtext><mi>t</mi><mi>r</mi><mi>u</mi><mi>e</mi><mspace linebreak="newline"></mspace><mi>p</mi><mi>r</mi><mi>e</mi><mi>d</mi><mi>e</mi><mi>c</mi><mi>e</mi><mi>s</mi><mi>s</mi><mi>o</mi><mi>r</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>z</mi><mi mathvariant="normal">.</mi><mi>s</mi><mi>e</mi><mi>c</mi><mi>o</mi><mi>n</mi><mi>d</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>n</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>w</mi><mi>r</mi><mi>a</mi><mi>p</mi><mtext>  </mtext><mi>f</mi><mo stretchy="false">)</mo><mo>&lt;</mo><mi>t</mi><mi>r</mi><mi>u</mi><mi>e</mi><mo separator="true">,</mo><mi>x</mi><mo>&gt;</mo><mo stretchy="false">)</mo><mspace linebreak="newline"></mspace><mi>w</mi><mi>r</mi><mi>a</mi><mi>p</mi><mi>f</mi><mo>≐</mo><mi>λ</mi><mi>p</mi><mi mathvariant="normal">.</mi><mo>&lt;</mo><mi>f</mi><mi>a</mi><mi>l</mi><mi>s</mi><mi>e</mi><mo separator="true">,</mo><mi>i</mi><mi>f</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>f</mi><mi>i</mi><mi>r</mi><mi>s</mi><mi>t</mi><mtext>  </mtext><mi>p</mi><mo stretchy="false">)</mo><mtext>  </mtext><mo stretchy="false">(</mo><mi>s</mi><mi>e</mi><mi>c</mi><mi>o</mi><mi>n</mi><mi>d</mi><mtext>  </mtext><mi>p</mi><mo stretchy="false">)</mo><mtext>  </mtext><mo stretchy="false">(</mo><mi>f</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>s</mi><mi>e</mi><mi>c</mi><mi>o</mi><mi>n</mi><mi>d</mi><mtext>  </mtext><mi>p</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>&gt;</mo></mrow><annotation encoding="application/x-tex">iszero \doteq \lambda n . n \; (\lambda x . false) \; true \\
predecessor \doteq \lambda n . \lambda s . \lambda z . second \; (n \; (wrap \; f) &lt;true, x&gt;) \\
wrap f \doteq \lambda p . &lt;false, if \; (first \; p) \; (second \; p) \; (f \; (second \; p))&gt;</annotation></semantics></math>iszero≐λn.n(λx.false)truepredecessor≐λn.λs.λz.second(n(wrapf)<true,x>)wrapf≐λp.<false,if(firstp)(secondp)(f(secondp))>

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`

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>m</mi><mi mathvariant="normal">.</mi><mi>i</mi><mi>f</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>i</mi><mi>s</mi><mi>z</mi><mi>e</mi><mi>r</mi><mi>o</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mn>0</mn><mtext>  </mtext><mo stretchy="false">(</mo><mi>a</mi><mi>d</mi><mi>d</mi><mtext>  </mtext><mi>m</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>p</mi><mi>r</mi><mi>e</mi><mi>d</mi><mi>e</mi><mi>c</mi><mi>e</mi><mi>s</mi><mi>s</mi><mi>o</mi><mi>r</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mi>m</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (mult \; (predecessor \; n) \; m))</annotation></semantics></math>mult≐λn.λm.if(iszeron)0(addm(mult(predecessorn)m))

However, lambda didn't have a name(all <math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mo>≐</mo></mrow><annotation encoding="application/x-tex">\doteq</annotation></semantics></math>≐ 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.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>k</mi><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>m</mi><mi mathvariant="normal">.</mi><mi>i</mi><mi>f</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>i</mi><mi>s</mi><mi>z</mi><mi>e</mi><mi>r</mi><mi>o</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mn>0</mn><mtext>  </mtext><mo stretchy="false">(</mo><mi>a</mi><mi>d</mi><mi>d</mi><mtext>  </mtext><mi>m</mi><mtext>  </mtext><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>t</mi><mtext>  </mtext><mi>t</mi><mo stretchy="false">)</mo><mtext>  </mtext><mo stretchy="false">(</mo><mi>p</mi><mi>r</mi><mi>e</mi><mi>d</mi><mi>e</mi><mi>c</mi><mi>e</mi><mi>s</mi><mi>s</mi><mi>o</mi><mi>r</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mi>m</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mkmult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; ((t \; t) \; (predecessor \; n) \; m))</annotation></semantics></math>mkmult≐λn.λm.if(iszeron)0(addm((tt)(predecessorn)m))

How to use this?

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mo>≐</mo><mo stretchy="false">(</mo><mi>m</mi><mi>k</mi><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mtext>  </mtext><mi>m</mi><mi>k</mi><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mult \doteq (mkmult \; mkmult)</annotation></semantics></math>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?

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>k</mi><mo>≐</mo><mi>λ</mi><mi>t</mi><mi mathvariant="normal">.</mi><mi>t</mi><mo stretchy="false">(</mo><mi>m</mi><mi>k</mi><mtext>  </mtext><mi>t</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mk \doteq \lambda t . t (mk \; t)</annotation></semantics></math>mk≐λt.t(mkt)

Oops, but wait, we can repeat the pattern.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>k</mi><mi>m</mi><mi>k</mi><mo>≐</mo><mi>λ</mi><mi>k</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>t</mi><mi mathvariant="normal">.</mi><mi>t</mi><mtext>  </mtext><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>k</mi><mtext>  </mtext><mi>k</mi><mo stretchy="false">)</mo><mtext>  </mtext><mi>t</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mkmk \doteq \lambda k . \lambda t . t \; ((k \; k) \; t)</annotation></semantics></math>mkmk≐λk.λt.t((kk)t)

Then we have `mk`, for sure.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>k</mi><mo>≐</mo><mo stretchy="false">(</mo><mi>m</mi><mi>k</mi><mi>m</mi><mi>k</mi><mtext>  </mtext><mi>m</mi><mi>k</mi><mi>m</mi><mi>k</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mk \doteq (mkmk \; mkmk)</annotation></semantics></math>mk≐(mkmkmkmk)

With `mk` we can have `mult` by a different way.

<math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>m</mi><mi>k</mi><mi>m</mi><mi>u</mi><mi>l</mi><msup><mi>t</mi><mo mathvariant="normal" lspace="0em" rspace="0em">′</mo></msup><mo>≐</mo><mi>λ</mi><mi>n</mi><mi mathvariant="normal">.</mi><mi>λ</mi><mi>m</mi><mi mathvariant="normal">.</mi><mi>i</mi><mi>f</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>i</mi><mi>s</mi><mi>z</mi><mi>e</mi><mi>r</mi><mi>o</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mn>0</mn><mtext>  </mtext><mo stretchy="false">(</mo><mi>a</mi><mi>d</mi><mi>d</mi><mtext>  </mtext><mi>m</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>t</mi><mtext>  </mtext><mo stretchy="false">(</mo><mi>p</mi><mi>r</mi><mi>e</mi><mi>d</mi><mi>e</mi><mi>c</mi><mi>e</mi><mi>s</mi><mi>s</mi><mi>o</mi><mi>r</mi><mtext>  </mtext><mi>n</mi><mo stretchy="false">)</mo><mtext>  </mtext><mi>m</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mi>m</mi><mi>u</mi><mi>l</mi><mi>t</mi><mo>≐</mo><mo stretchy="false">(</mo><mi>m</mi><mi>k</mi><mi>m</mi><mi>k</mi><mi>m</mi><mi>u</mi><mi>l</mi><msup><mi>t</mi><mo mathvariant="normal" lspace="0em" rspace="0em">′</mo></msup><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">mkmult' \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (t \; (predecessor \; n) \; m))
mult \doteq (mk mkmult')</annotation></semantics></math>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.