Beyond awesome | 越而胜己

I have been reading Type Theory and Formal Proof recently. I have just finished the first chapter, and the most mind-blowing concept that I ran into was Section 1.10 Fixed Point Theorem.

The theorem states the following: in $\lambda$-calculus, every $\lambda$-term $L$ has a fixed point，i.e. for each $L$ there exists a $\lambda$-term $M$ such that $LM =_\beta M$.

$$\forall L \in \Lambda, \exists M \in \Lambda : LM =_\beta M$$

In "normal" math world, some functions do not have fixed points, such as $f(x) = 2^x$ and $f(x) = x + 1$ (which is easily provable since their plots do not intersect with the line $y=x$). But in the lambda world, it is possible to find fixed points for them as well (although the fixed points may be functions themselves).

The book provides the method to find a fixed point for any function $L$, as a proof of the theorem. Let $M := (\lambda x . L(xx))(\lambda x . L(xx))$. We do $\beta$-reduction on $M$ and obtain $L((\lambda x . L(xx))(\lambda x . L(xx))) \equiv LM$. Therefore, $LM =_\beta M$.

We can even construct a function $Y$ that calculates the fixed point of any $\lambda$-term, by abstracting $L$:

$$Y \equiv \lambda y . (\lambda x . y(xx))(\lambda x . y(xx))$$

The $\lambda$-term $Y$ is famously known as the "$Y$-combinator." It is the simplest and the most famous "fixed point combinator." We can easily prove that $YL =_\beta L(YL)$ for any $L$.

One of the most important applications of such fixed point combinators is solving recursive equations. If we have a equation in the shape of

$$M =_\beta \dots\dots M \dots\dots$$

We can abstract $M$ from the right side of the equation and obtain

$$L \equiv \lambda z . (\dots\dots z \dots\dots)$$

Note that the right side is just $LM$, so the equation now becomes $M =_{\beta} LM$. Now we can just use the $Y$-combinator to find the solution $M =_{\beta} YL$.

$$\forall L \in \Lambda, \exists M \in \Lambda : LM =_\beta M$$

$$Y \equiv \lambda y . (\lambda x . y(xx))(\lambda x . y(xx))$$

$Y$ 被称为 $Y$ 组合子，是最简单的不动点组合子，通过 $\beta$-规约可以证得 $YL =_\beta L(YL)$。

$Y$ 组合子的一个重要应用是解递归方程。如果遇到形如

$$M =_\beta \dots\dots M \dots\dots$$

$$L \equiv \lambda z . (\dots\dots z \dots\dots)$$