简单易懂的程序语言入门小册子(5):基于文本替换的解释器,递归,不动点,fix表达式,letrec表达式

这个系列有个显著的特点,那就是标题越来越长。忽然发现今天是读书节,读书节多读书。

==下面是没有意义的一段话================================================

我是一个喜欢从学习知识中获得乐趣并乐于分享这种乐趣的人。我认为大部分知识只要花点时间都是能学会的。几年前,我迷上微分几何。我对每个朋友说这东西很有意思花点时间精力就能学会。他们回答说唉没时间时间不知去哪儿了。后来,我迷上量子力学。我对每个朋友说这东西值得一学,只要花点时间精力。他们回答说唉烦心事太多没精力去学。再后来,我迷上程序语言。我对每个朋友说只要使劲挤点时间就能掌握这个。他们回答说唉浑浑噩噩不知道一直在忙什么没时间唉。现在,他们都结婚了,我依然单身。

==然后,正文开始======================================================

不动点

唉,又是一个数学概念, 又是没有实际意义的一节。 但是作为递归相关的常识,还是得提一下。 话说回来,把这玩意儿当作常识,我大概是价值观扭曲,重要性排行颠倒吧。 据说很多研究程序语言,研究偏微分方程的人都这样。

然后,一个——呃——东西$x$被称为函数$f$的不动点,如果它满足下面条件: \[ (f \; x) = x \]

不动点和递归有什么关系呢? $({Y} \; f)$不仅是关于辅助函数$f$的递归函数,同时也是$f$的不动点。 证明如下: \begin{eqnarray*} ({Y} \; f) &=& (\lambda x.(\lambda v.(v \; v) \; \lambda f.(x \; (f \; f))) \; f) \\               &=& (\lambda x.(\lambda v.(v \; v) \; \lambda p.(x \; (p \; p))) \; f) \\               &=& (\lambda v.(v \; v) \; \lambda p.(f \; (p \; p))) \\               &=& (\lambda p.(f \; (p \; p)) \; \lambda p.(f \; (p \; p))) \\               &=& (f \; (\lambda p.(f \; (p \; p)) \; \lambda p.(f \; (p \; p)))) \\               &=& (f \; (\lambda v.(v \; v) \; \lambda p.(f \; (p \; p)))) \\               &=& (f \; (\lambda x.(\lambda v.(v \; v) \; \lambda p.(x \; (p \; p))) \; f)) \\               &=& (f \; ({Y} \; f)) \end{eqnarray*} 由于递归函数肯定能写成$({Y} \; f)$的形式(参见之前mkdouble的构造方法),递归函数必定是某个函数$f$的不动点。

加入fix表达式

用Y组合子构造递归函数总归太麻烦。 所以需要能直接构造递归函数的表达式。 先来看这个表达式需要哪些元素。 首先,递归函数要调用自己,需要一个指向自己的变量,记为$X_1$。 其次,递归函数有个参数,记为$X_2$。 最后,递归函数的函数体,记为$M$。 构造递归函数其实是寻找不动点的过程,所以这个表达式叫fix表达式(不动点叫fixed point)。 fix表达式长这个样: \[ ({fix} \; X_1 \; X_2 \; M) \] 加入fix表达式最简单的方法是定义为宏: \[ ({fix} \; X_1 \; X_2 \; M) = ({Y} \; \lambda X_1.\lambda X_2.M) \] 但是这样做又重新引入了Y组合子。 这次采用另一种方法,不定义宏,而是把fix表达式加入语法: \begin{eqnarray*}   M, N, L &=& ... \\           &|& ({fix} \; X_1 \; X_2 \; M) \end{eqnarray*}

现在考察fix表达式的求值过程。 fix表达式的求值结果是个函数,参数是$X_2$: \[ eval(({fix} \; X_1 \; X_2 \; M)) = \lambda X_2.? \] 最适合放在问号处的函数体的是$M$,但是$M$包含了*变量$X_1$,使用$M$之前得先想方法除掉$X_1$。 $X_1$代表递归函数本身,也就是$({fix} \; X_1 \; X_2 \; M)$。 为了去掉$M$中的*变量$X_1$,将$X_1$替换为递归函数$({fix} \; X_1 \; X_2 \; M)$。 综上,fix表达式的求值过程为: \[ eval(({fix} \; X_1 \; X_2 \; M)) = \lambda X_2.M[X_1 \leftarrow ({fix} \; X_1 \; X_2 \; M)] \] 代码:

简单易懂的程序语言入门小册子(5):基于文本替换的解释器,递归,不动点,fix表达式,letrec表达式

加入了新语法,要添加相应的替换过程(这个替换过程和$\lambda X.M$的替换过程类似,但是麻烦了点): \begin{eqnarray*}   ({fix} \; X_1 \; X_2 \; M)[X_1 \leftarrow N] &=& ({fix} \; X_1 \; X_2 \; M) \\   ({fix} \; X_1 \; X_2 \; M)[X_2 \leftarrow N] &=& ({fix} \; X_1 \; X_2 \; M) \\   ({fix} \; X_1 \; X_2 \; M)[X_3 \leftarrow N] &=& ({fix} \; X_4 \; X_5 \; M[X_2 \leftarrow X_5][X_1 \leftarrow X_4][X_3 \leftarrow N]) \\   &其中&X_3 \neq X_1, X_3 \neq X_2, \\   &&X_4 \notin FV(N), X_4 \notin FV(M)\backslash\{X_1\}, \\   &&X_5 \notin FV(N), X_5 \notin FV(M)\backslash\{X_2\} \end{eqnarray*} 代码:

简单易懂的程序语言入门小册子(5):基于文本替换的解释器,递归,不动点,fix表达式,letrec表达式

测试一下:

'((fix f n (if (iszero n) 0 (+ 2 (f (- n 1))))) 4)

>> 8

加入letrec表达式

let表达式不能定义递归函数,所以有个letrec表达式专门用来定义递归函数。 letrec表达式长这个样: \[ ({letrec} \; X_1 \; X_2 \; N \; M) \] $X_1$,$X_2$和$N$定义了一个递归函数,$M$是用到这个递归函数的一个表达式。

类似let表达式,将letrec表达式定义为宏: \[ ({letrec} \; X_1 \; X_2 \; N \; M) = (\lambda X_1.M \; ({fix} \; X_1 \; X_2 \; N)) \] 代码:

简单易懂的程序语言入门小册子(5):基于文本替换的解释器,递归,不动点,fix表达式,letrec表达式

简单易懂的程序语言入门小册子(5):基于文本替换的解释器,递归,不动点,fix表达式,letrec表达式

上一篇:使用Ansible实现数据中心自动化运维管理


下一篇:简单易懂的程序语言入门小册子(4):基于文本替换的解释器,递归,如何构造递归函数,Y组合子