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$.

最近正在阅读《类型论与形式证明》,读完第一章 Untyped Lambda Calculus 最令人感到醍醐灌顶的是第 1.10 节 Fixed Point Theorem 不动点定理。

在 $\lambda$-calculus 中,每个 $\lambda$-term $L$ 都存在一个不动点,即每个 $L$ 都存在一个 $\lambda$-term $M$ 使得 $LM =_\beta M$,即

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

在一般的数学世界,有些函数比如 $f(x) = 2^x$ 或者 $f(x) = x + 1$ 显然并不存在不动点(与直线 $y=x$ 没有交集),然而在函数世界则可以找到。

书中给出了找到不动点的方法(即对定理的证明):令 $M = (\lambda x . L(xx))(\lambda x . L(xx))$。对 $M$ 进行 $\beta$-规约可以得到 $L((\lambda x . L(xx))(\lambda x . L(xx))) \equiv LM$。因此 $LM =_\beta M$。

我们甚至可以构造一个计算 $M$ 的函数 $Y$:

$$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$$

的方程,可以将等式右边的 $M$ abstract 出来得到

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

则方程可以变形为 $M =_{\beta} LM$。此时可以用 $Y$ 组合子求得 $M =_{\beta} YL$。