跳至正文

TaPL Chapter 5 – The Untyped Lambda-Calculus

本章从零开始,完整地介绍了 untyped pure lambda-calculus 的 syntax、求值规则,并给出了大量的有关 untyped pure lambda-calculus 的使用示例。

Basics

本节主要介绍 pure lambda-calculus 以及它的一些 operational semantics 定义。

Pure lambda-calculus 的语法非常简单:

t ::=
	x
	λx.t
	t t

一个 pure lambda-calculus 的 term t 仅有三种形式:

  1. t 是一个变量 x
  2. t 是一个函数定义,或称之为 abstraction,写作 λx.t,其中 x 表示函数的形式参数,t 是构成函数体的 term;
  3. t 是一个函数调用,或称之为 application,写作 t t,其中第一个 t 表示被调用的函数,第二个 t 表示函数的参数。

在 pure lambda-calculus 中,所有的值都是函数。这意味着每一个变量都是函数,函数的参数也是函数,将函数应用到某个参数上的求值结果仍然是函数。Everything is a function。另外需要注意到,在 pure lambda-calculus 中,所有的函数均有且仅有一个参数。如果希望描述具有多个参数的函数,则需要通过高阶函数(higher-order function)柯里化(currying)来实现。具体内容将在稍后介绍。

Abstract Syntax & Concrete Syntax

程序语言的 syntax 有 abstract syntaxconcrete syntax 之分。简单来说,abstract syntax 就是程序的抽象语法树,而 concrete syntax 就是程序员编写的那一串表示整个程序的字符串代码。将程序从 concrete syntax 转换到 abstract syntax 是编译器前端中的 lexerparser 的工作。

Concrete syntax 相比于 abstract syntax 有更多的噪音,因为需要这些噪音来消除一些语法上的二义性。例如,对于 term a b c,它可能对应两种形式的 abstract syntax,分别可以使用带括号的 concrete syntax 表示为 (a b) c 以及 a (b c)。在接下来的讨论中,当出现类似于 a b c 这样的 concrete syntax 中,我们都假定它的 abstract syntax 是 (a b) c

Scope

在一个 abstraction λx.t 中,如果 t 中出现了 x,那么称 t 中出现的 x约束变量(bounded variable)。在 t 中出现的没有被 bound 的 variable 则称为自由变量(free variable)。例如,在 λx. λy. x y z 中,x y z 中的 xy 是 bounded variable,而 z 是 free variable。

一个不包含 free variable 的 term 称为 closed term,也称为组合子(combinator)。最简单的组合子是 identity function,即 λx. x

Operational Semantics

对于 pure lambda-calculus,执行计算过程的唯一方式是 application,即在计算的每一步,都将一个函数(或者称为 abstraction)应用到这个函数的唯一一个参数上。在进行 application 时,只需要将 application 替换为函数的 body,并将 body 中的 bound variable 替换为实际的参数。我们可以将这个过程写作:

\left(\lambda x.\;t_{12}\right)\;t_2 \rightarrow \left[x \mapsto t_2\right]t_{12}

其中 \left[x \mapsto t_2\right]t_{12} 表示将 t_{12} 中的所有名为 x 的自由变量替换为 t_2 后得到的 term。例如,(λx.x) y 将被求值为 y,而 (λx. x (λx.x)) (u r) 将被求值为 u r (λx. x)

\left(\lambda x.\;t_{12}\right)\;t_2 这种形式的 term 被称为 redex,即 reducible expression。将一个 redex 按照上述方式进行替换、重写、化简的过程叫做 beta-reduction

Pure lambda-calculus 有着四种不同的求值策略:

Full beta-reduction

Full beta-reduction 是限制最少的一种求值策略。具体来说,在 full beta-reduction 的每一步,都从待求值的语句中任选一个 redex 进行化简。例如,假设 id 表示 identity function,那么对于语句 id (id (λz. id z)),它包含三个 redex,分别是:

  1. id (id (λz. id z))
  2. id (id (λz. id z))
  3. id (id (λz. id z))

如果使用 full beta-reduction 求值策略对上述语句进行求值,那么我们可以在每一步任选语句中的一个 redex 进行化简和求值。因此,在求值的第一步,我们可以选择上述三个 redex 中的其中任意一个进行化简和求值。一种可能的求值路径如下所示:

\begin{align*}& \text{id}\;\left(\text{id}\;\left(\lambda z.\;\underline{\text{id}\;z}\right)\right) \\ \rightarrow\; & \text{id}\;\underline{\left(\text{id}\; \left(\lambda z.\;z\right)\right)} \\ \rightarrow\;& \underline{\text{id}\;\left(\lambda z.\;z\right)} \\ \rightarrow\; & \lambda z.\;z\end{align*}

Normal order

在 normal order 求值策略下,在求值的每一步,只能对处在语句最左端、最外层的 redex 进行化简和求值。在这种求值策略下,前面的语句的求值路径如下:

\begin{align*} &\underline{\text{id}\;\left(\text{id}\;\left(\lambda z.\;\text{id}\;z\right)\right)} \\ \rightarrow\; & \underline{\text{id}\;\left(\lambda z.\;\text{id}\;z\right)} \\ \rightarrow\; & \lambda z.\;\underline{\text{id}\;z} \\ \rightarrow\; &  \lambda z.\;z \end{align*}

Call by name strategy

在 call by name 求值策略下,处在一个 abstraction 内部的 redex 不能化简和求值。在这种求值策略下, 前面的语句的求值路径如下:

\begin{align*}&\underline{\text{id}\;\left(\text{id}\;\left(\lambda z.\;\text{id}\;z\right)\right)} \\ \rightarrow\; & \underline{\text{id}\;\left(\lambda z.\;\text{id}\;z\right)} \\ \rightarrow\; & \lambda z.\;\text{id}\;z\end{align*}

注意这里与 normal order 的区别。当上述求值过程到达最后一步后,虽然 id z 仍然是一个 redex,但是它处于一个 abstraction 中,因此按照 call by name 策略的规则,它不能被化简和求值。

Call by name 求值策略是许多支持惰性求值(lazy evaluation)的编程语言的求值策略的基础,例如 Haskell 等。

Call by value strategy

Call by value 求值策略要求在求值的每一步都化简语句最外层的 redex,且一个 redex 只有在其 application 的参数已经被化简到 normal form 后才能被化简。在这种求值策略下,前面的语句的求值路径如下:

\begin{align*} & \text{id}\;\underline{\left(\text{id}\;\left(\lambda z.\;\text{id}\;z\right)\right)} \\ \rightarrow\; & \underline{\text{id}\;\left(\lambda z.\;\text{id}\;z\right)} \\ \rightarrow\; & \lambda z.\;\text{id}\;z\end{align*}

Call by value 求值策略正是大部分编程语言的求值策略的基础。在这种求值策略下,函数的参数会在函数被调用前被求值出来。

除非特别说明外,本书接下来的所有讨论都是基于 call by value 求值策略的讨论。

Programming in the Lambda-Calculus

本节介绍了一系列使用 lambda-calculus 进行编程的例子。这些例子可以帮助我们更好地 get the feel of pure lambda-calculus。

Multiple Arguments

Pure lambda-calculus 中的函数(即 abstraction)有且仅有一个参数。为了表示具有多个参数的函数,我们需要借助高阶函数(higher-order function)这一工具。所谓高阶函数,即返回值为函数的函数。当然,在 pure lambda-calculus 中,由于所有的值都是函数,因此所有的 abstraction 都是高阶函数。

具体地,假如我们希望抽象一个具有两个参数 xy 的函数,其函数体记做 z。我们可以按照如下方式在 pure lambda-calculus 中构造出这个函数:

\lambda x.\; \lambda y. \; z

注意到,最外层的 abstraction 接收一个参数 x,并返回一个 abstraction,这个 abstraction 继续接收一个参数 y,并最终返回 z。求值过程如下:

\begin{align*}& \underline{\left(\lambda x.\; \lambda y.\;z\right)\;u}\;v \\ \rightarrow\; & \underline{\left(\lambda y.\;\left[x \mapsto u\right]z\right)\;v} \\ \rightarrow\; & \left[y \mapsto v\right]\left[x \mapsto u\right] z\end{align*}

可以看到,最终的求值效果与我们在其他编程语言中调用包含多个参数的函数的效果是一致的。这种将具有多个参数的函数转化为一系列的只接收一个参数的高阶函数的过程叫做柯里化(Currying)

Church Booleans

这一小节中我们将讨论应该如何在 pure lambda-calculus 中表示出 boolean 类型的值。一个 boolean 类型的值只会有两种取值:true 或者 false。

在 pure lambda-calculus 中,所有的值都是函数。因此,我们不可能像其他编程语言中那样直接有一个 boolean 值的表示。相反地,我们需要思考我们应该如何将普遍意义上的 boolean 类型的两个值映射到两个函数上,使得 boolean 值和它映射到的函数有一些共同的属性。

Boolean 值的最重要的属性是它可以用于条件判断。例如,对于表达式 if b then x else y,如果 b 为 true,那么表达式的值为 x;否则表达式的值为 y。在这里,boolean 值 b 起到的作用是,它可以根据自身是 true 还是 false,从 xy 两个值中进行相应的选择

现在我们可以尝试将上述的讨论落实到 pure lambda-calculus 上来。我们不妨将 boolean 值可以在两个值之间进行选择这一属性利用 pure lambda-calculus 进行表达。为了达到这一目标,我们可以将 true 和 false 分别在 pure lambda-calculus 中定义为如下的 abstraction:

\begin{align*} \text{tru} &= \lambda t.\; \lambda f.\; t \\ \text{fls} &= \lambda t.\; \lambda f.\; f \end{align*}

这里将 true 和 false 分别命名为 trufls 是为了将其与其他编程语言中的 truefalse 区分开。对于表达式 tru x y,其求值结果为 x,就像是 tru 这一 boolean 值在 xy 之间选择了 x 一样;对于表达式 fls x y,其求值结果为 y,就像是 fls 这一 boolean 值在 xy 之间选择了 y 一样。按照这种方式定义的 pure lambda-calculus 中的 boolean 值称为 church boolean

Boolean 类型还可以参与到逻辑运算中,例如逻辑与(and)、逻辑或(or)、逻辑非(not)等。事实证明,我们也可以在 church boolean 上定义这些逻辑运算,使得这些运算的效果和普遍意义上的逻辑运算效果如出一辙:

\begin{align*} \text{and} &= \lambda b.\; \lambda c.\; b\;c\;\text{fls} \\ \text{or} &= \lambda b.\; \lambda c.\; b\;\text{tru}\;c \\ \text{not} &= \lambda b.\; b\;\text{fls}\;\text{tru} \end{align*}

这些逻辑运算的正确性是很容易进行 reasoning 的:

  • 对于逻辑与,它的行为是如果输入的两个 boolean 值都为 true,那么结果也为 true;否则结果为 false。我们看 and 的定义,它是在利用第一个输入的 boolean 值去选择第二个输入的 boolean 值和 fls 这两个值中的一个。当第一个输入的 boolean 值为 tru 时,结果为第二个输入的 boolean 值,符合预期;当第一个输入的 boolean 值为 fls 时,结果为 fls,也符合预期;
  • 同理,对于 or,当第一个输入的 boolean 值为 tru 时,结果为 tru,符合预期;当第一个输入的 boolean 值为 fls 时,结果为第二个输入的 boolean 值,也符合预期;
  • not 则更加直观。当输入的 boolean 值为 tru 时,它选择出 fls 作为结果,符合预期;当输入的 boolean 值为 fls 时,它选择出 tru 作为结果,也符合预期。

Pairs

一个 pair 即一个包含了两个值的聚合对象,对应于 C++ 中的 std::pair,对应于其他编程语言中的二元组。为了在 pure lambda-calculus 中表示出一个 pair,与 boolean 值类似,我们需要考虑利用 pure lambda-calculus 表达出 pair 的哪些属性。

在利用简单的值构造复杂的数据结构时,我们一般会首先考虑两个问题:

  1. 如何使用简单的值构造出复杂数据结构?
  2. 如何在复杂的数据结构中提取出简单的值?

对于 pair,这两个问题便可以具体化为:

  1. 如何通过两个值构造出一个 pair?
  2. 如何抽取出一个 pair 中包含的两个值?

我们不妨将一个由 x 和 y 这两个值组成的 pair 表示为如下所示的函数:

\lambda b.\; b\;x\;y

其中 b 是一个 church boolean。因此,一个 pair 就是一个函数,该函数接收一个 church boolean,并利用这个 church boolean 来选择这个 pair 中包含的两个值之一。那么,构造这样的一个 pair 的方法也很简单:

\text{pair} = \lambda x.\; \lambda y.\; \lambda b.\; b\;x\;y

上述的 pair 即为一个 pair 的构造函数。它接收两个参数,并返回一个 pair。

抽取出一个 pair 中包含的两个值的方法也非常容易写出:

\begin{align*} \text{fst} &= \lambda p.\; p\;\text{tru} \\ \text{snd} &= \lambda p.\; p\;\text{fls}  \end{align*}

fstsnd 是 pair 的两个选择函数。前者负责从一个 pair 中抽取出其包含的第一个值,后者负责从一个 pair 中抽取出其包含的第二个值。

Church Numerals

这一小节中我们将讨论如何在 pure lambda-calculus 中表示出一个自然数。我们将从自然数的数学意义角度入手寻找答案。

皮亚诺公理规定了什么是自然数,并在自然数上建立起了一套算术系统的基础。皮亚诺公理实际包含五条公理,我们在这里只关心其前四条即可:

  1. 0 是自然数;
  2. 每一个确定的自然数 a,都有一个确定的后继数 \text{succ}\left(a\right)\text{succ}\left(a\right) 也是自然数;
  3. 对于自然数 bcb=c 当且仅当 \text{succ}\left(b\right) = \text{succ}\left(c\right)
  4. 0 不是任何自然数的后继数。

仿照皮亚诺公理的定义,我们可以在 pure lambda-calculus 中定义一个自然数的表示。具体地,在 pure lambda-calculus 中定义自然数 0 为:

c_0 = \lambda s.\; \lambda z.\;z

然后,对于所有的 i \ge 1,在 pure lambda-calculus 中定义自然数 i 为:

c_i = \lambda s.\; \lambda z.\; s\; \left(c_{i-1}\;s\;z\right)

我们可以尝试展开前几个自然数在 pure lambda-calculus 中的定义:

\begin{aligned} c_0 &= \lambda s.\; \lambda z.\; z \\ c_1 &= \lambda s.\; \lambda z.\; s\; z \\ c_2 &= \lambda s.\; \lambda z.\; s\; \left(s\; z\right) \\ c_3 &= \lambda s.\; \lambda z.\; s\; \left(s\; \left(s\; z\right)\right) \end{aligned}

可以看出,c_i 是一个函数,其接受两个参数 sz,其中 z 表示一个具体的 “0” 值,s 表示一个用于计算自然数的 “后继” 的函数。c_i 会反复地将 s 应用到 zi 次,计算出 “0” 值的第 i 个后继,也即一个具体的自然数 i。通过这种方式在 pure lambda-calculus 中表示的自然数称为 Church numeral

下面我们基于 church numeral 的定义,编写一些常见的自然数上的运算函数,包括判断是否为零、判断是否相等、计算后继(即将自然数加 1)、计算前驱、加法运算、减法运算、乘法运算、幂运算等。

判断是否为零的思路很简单,如下:

\text{iszro} = \lambda m.\; m\; \left(\lambda x.\; \text{fls}\right) \text{tru}

iszro 是一个函数,它接受一个 church numeral m,若 m 是零,则 iszro 将求值为 church boolean 值 tru;否则 iszro 将求值为 church boolean 值 fls。前面我们提到过,church numeral 本质上是一个(在柯里化之前)能够接受“两个”参数的函数,这个函数会将第一个参数反复地作用于第二个参数上 n 次,这个 n 即是 church numeral 所表示的自然数。再来看 iszro 的定义,如果 m 是零,那么在 iszro 中传给 m 的第一个参数将不会被调用,因此最终求值结果是 tru;如果 m 不是零,那么在 iszro 中传给 m 的第一个参数将至少被调用一次,而这个参数一旦被调用便会导致 iszro 的求值结果变为 fls。因此,iszro 正确地实现了要求的功能。

计算后继的方法如下:

\text{scc} = \lambda n.\; \lambda s.\; \lambda z.\; s\; \left(n\; s\; z\right)

scc 是一个函数(更确切地说,它是一个组合子),它接收一个 church numeral 作为参数 n,返回 n 的后继。思路也很容易理解,只需要让返回的 church numeral 再一次将其第一个参数应用到 n 的求值结果上即可。在 scc 的定义中,n s z 即是先将 s 反复应用到 z 上面 n 次,然后再将 s 应用到这个结果上一次即可得到 n 的后继。

这里还有一个小问题。即,求值 \text{scc}\; c_1 的结果是什么?是 c_2 吗?我们可以尝试求值一下 \text{scc}\; c_1

\begin{aligned} & \text{scc}\; c_1 \\ =\;& \underline{\left(\lambda n.\; \lambda s.\; \lambda z.\; s\; \left(n\; s\; z\right)\right)\; \left(\lambda s.\; \lambda z.\; s\; z\right)} \\ \rightarrow\;& \lambda s.\; \lambda z.\; s\; \left(\left(\lambda s^\prime.\; \lambda z^\prime.\; s^\prime\; z^\prime\right)\; s\; z\right) \end{aligned}

注意上述的求值过程已经将 \text{scc}\; c_1 求值为 normal form,最后一行无法在 call-by-value 求值规则下进一步被求值。因此很显然,\text{scc}\; c_1 并不是 c_2。但这并不是因为设计或实现不当,也不会实际造成问题,因为 \text{scc}\; c_1c_2 有着完全一样的效果和性质。即,它们都是一个带有两个参数的函数,且它们最终都会将第一个参数反复地应用到第二个参数上两次。

计算两个 church numeral 的加和的方法如下:

\text{plus} = \lambda m.\; \lambda n.\; \lambda s.\; \lambda z.\; m\; s\; \left(n\; s\; z\right)

如果你理解了如何计算后继,那么上述计算加和的方法是非常容易理解的。因此不再过多赘述。

其实还有一种更简便的计算加和的方法:

\text{plus} = \lambda m.\; \lambda n.\; m\; \text{scc}\; n

同样地,这个方法也非常容易理解,因此不做进一步解释。

计算两个 church numeral 的乘积的方法如下:

\text{times} = \lambda m.\; \lambda n.\; m\; \left(\text{plus}\; n\right)\; c_0

注意 c_0 是表示零的 church numeral,即 \lambda s.\; \lambda z.\; z。计算乘积的方法的巧妙之处在于,我们将原本的用于运算后继的函数(即传递给 church numeral 的第一个参数)替换成了运算加上一个乘数的函数。如果你已经熟悉柯里化,那么你应该知道,plus n 是一个函数,它接收一个参数,返回这个参数加上 n 后的值。知道这一点后,times 函数就很容易理解了,它利用 m 这个乘数,将 plus n 这个函数反复地应用 m 次到 [/katex]c_0[/katex] 上,得到的最终结果当然就是将后继函数 s 反复地应用了 nm 次到 c_0 上,因此得到了表示 nm 的乘积的 church numeral。

知道了乘法运算的定义技巧后,我们可以立即比照着写出计算 m^n 的方法:

\text{power} = \lambda m.\; \lambda n.\; n\; \left(\text{times}\; m\right)\; c_0

原理可以由读者自行思考,需要特别注意 mn 的顺序问题(它们不能互换)。

到此为止,从计算一个 church numeral 的后继出发,我们最终写出了计算幂的方法。下面,我们将从计算一个 church numeral 的前驱出发,最终写出计算减法的方法。你应该可以隐隐感觉到,计算一个 church numeral 的前驱将比计算后继更加复杂和困难。

首先,我们必须对前驱下一个良好的定义。对于表示非零的自然数,其前驱自然地是将这个自然数减一得到的值;对于零,我们定义其前驱仍然是零。

我们可以按照如下方式定义计算前驱的方法:

\begin{aligned} \text{zz} &= \text{pair}\; c_0\; c_0 \\ \text{ss} &= \lambda p.\; \text{pair}\; \left(\text{snd}\; p\right)\; \left(\text{succ}\; \left(\text{snd}\; p\right)\right) \\ \text{prd} &= \lambda m.\; \text{fst}\; \left(m\; \text{ss}\; \text{zz}\right) \end{aligned}

我们调整了后继函数(即 church numeral 的第一个函数参数)和零值(即 church numeral 的第二个函数参数)的形式,将前驱这一信息编码进了 church numeral 中。具体地,新的零值 \text{zz} 是一个二元组,其第一个域表示原先的零值的前驱,即零值本身;第二个域表示原先的零值。新的后继函数 \text{ss} 也进行了调整,使得最终表示自然数 i 的 church numeral 将是一个具有形式 \left(c_{i-1}, c_i\right) 的二元组,即:

\begin{aligned} C_0 &= \text{zz} = \left(c_0, c_0\right) \\ C_1 &= \left(c_0, c_1\right) \\ C_2 &= \left(c_1, c_2\right) \\ C_3 &= \left(c_2, c_3\right) \end{aligned}

在这样的体系下,\text{prd} 的定义方法就非常简单了,只需要取出 C_i 的第一个域即可。

基于 prd 的定义,我们可以写出计算 m-n 的方法:

\text{sub} = \lambda m.\; \lambda n.\; n\; \text{pred}\; m

其原理非常简单,因此不再过多赘述。

最后,我们来看如何判断两个 church numeral 是否相等。方法是判断这两个 church numeral 相减后是否为零,如下:

\text{equal} = \lambda m.\; \lambda n.\; \text{and}\; \left(\text{iszro}\; \left(\text{sub}\; m\; n\right)\right) \left(\text{iszro}\; \left(\text{sub}\; n\; m\right)\right)

即我们判断 n-mm-n 是否均同时为零。需要同时判断两个条件的原因是 church numeral 中没有负数值,因此当 n-m 为零时只能推断出 n \le m ,而不能推断出 n = m

本节以及前几节相继介绍了 church boolean、pair 以及 church numeral。这些在 pure lambda-calculus 中表示出各种不同意义的值的编码称为 church encoding。有关 church encoding 的系统介绍可以参见相应的 wikipedia 页面

Enriching the Calculus

在 pure lambda-calculus 中,所有的值都是函数。因此我们前面提到,我们没法像其他的程序设计语言那样直接拥有 boolean 值或自然数值的表示。为了解决这个问题,前面我们在 pure lambda-calculus 中引入了 church encoding。但是 church encoding 并没有给 pure lambda-calculus 引入全新的语言元素,只是利用了已有的语言设施进行编码。在实际处理 lambda-calculus 时,我们更希望能够有一种 boolean 值和自然数值的、“内嵌”进入程序设计语言本身的表示,就像其他语言那样。在本节中我们将在 pure lambda-calculus 的基础上引入“真正”的 boolean 值和自然数值,构成的 lambda-calculus 系统称为 $\lambda \text{NB}$。在 $\lambda \text{NB}$ 中,值除了可以是函数(abstraction)以外,还可以是 boolean 值或自然数值。

首先,我们引入“真正”的 boolean 值 truefalse。它们可以很容易地与 church boolean 值进行转换:

\begin{aligned} \text{realbool} &= \lambda b.\; b\; \text{true}\; \text{false} \\ \text{churchbool} &= \lambda b. \; \text{if}\; b\; \text{then}\; \text{tru}\; \text{else}\; \text{fls} \end{aligned}

realbool 接受一个 church boolean 值,返回对应的“真正”的 boolean 值。churchbool 接受一个“真正”的 boolean 值,返回对应的 church boolean 值。注意,“真正”的 boolean 值可以直接参与到 if 等常见的条件判断结构的运算中。realboolchurchbool 的原理都非常简单,因此不再过多赘述。

然后,我们引入“真正”的自然数值 0123……,并定义它们与 church numeral 的对应值的转换关系:

\text{realnat} = \lambda m.\; m\; \left(\lambda x.\; \text{succ}\; x\right)\; 0

Recursion

本节将介绍一个广为人知的问题及其解决方案,即如何在 pure lambda-calculus 中实现递归。它的解决方法将引出不动点组合子(Fixed-Point Combinator)的概念,最著名的不动点组合子便是 Y 组合子(Y Combinator)

你应该很清楚递归的概念。例如,我们可以使用如下方式计算一个 church numeral 的阶乘:

\text{fct} = \lambda n.\; \left(\text{iszro}\; n\right)\; c_1\; \left(\text{times}\; n\; \left(\text{fct}\; \left(\text{prd}\; n\right)\right)\right)

上述算法非常简单易懂,我们不再解释算法本身。上面的写法的问题在于,我们在定义 fct 时又用到了 fct 本身,即 fct 是个递归函数,而这种写法在 pure lambda-calculus 中是不被允许的。在定义 fct 时,我们不能使用 fct 本身。

看起来 pure lambda-calculus 的这一限制导致我们没法编写需要进行递归的函数。但是,数学家们已经证明,pure lambda-calculus 和图灵机具备同样的计算能力。因此,虽然我们没办法直接在 pure lambda-calculus 中写出类似于上面 fct 那样的递归函数,但一定存在某种方法能够在 pure lambda-calculus 中模拟出递归的效果。

我们发现,像上面那样直接在 fct 的定义中引用 fct 本身存在的问题在于,fct 的定义中出现的 fct 是自由变量,并没有被绑定到 fct 自己。那么,我们定义一个全新的函数 g,并用一个 abstraction 包裹住 fct 的定义,强行让 fct 变成约束变量:

g = \lambda \text{fct}.\; \lambda n. \left(\text{iszro}\; n\right)\; c_1\; \left(\text{times}\; n\; \left(\text{fct}\; \left(\text{prd}\; n\right)\right)\right)

这样,我们将 fct 从自由变量变为了约束变量。

这样的变换好像并没有解决什么问题,治标不治本。变换后的形式好像并没有告诉我们应该如何去定义 fct。那么这一步变换有什么意义?

假设我们最终找到了一个满足要求的 fct 函数,记做 F。我们考虑将 g 应用到 F 上,得到:

\begin{aligned} g\; F &= \left(\lambda \text{fct}.\; \lambda n. \left(\text{iszro}\; n\right)\; c_1\; \left(\text{times}\; n\; \left(\text{fct}\; \left(\text{prd}\; n\right)\right)\right)\right)\; F \\ &\rightarrow \lambda n. \left(\text{iszro}\; n\right)\; c_1\; \left(\text{times}\; n\; \left(F\; \left(\text{prd}\; n\right)\right)\right) \end{aligned}

而根据定义,我们还希望 $F$ 有如下的性质:

F = \lambda n. \left(\text{iszro}\; n\right)\; c_1\; \left(\text{times}\; n\; \left(F\; \left(\text{prd}\; n\right)\right)\right)

综合上面两个式子,我们得到:

g\; F = F

即满足我们要求的 fct 函数正是函数 g不动点(fix point)。一个函数 f 的不动点是一个值 x 使得 f\; x = x。因此,只要我们能够计算出 g 函数的不动点,计算出的不动点就是我们需要的 fct 函数。那么现在问题变成如何计算一个函数的不动点。

幸运的是,数学家和计算机科学家们已经找到了许多专门用于计算函数不动点的组合子。最著名的用于计算函数不动点的组合子是 Y 组合子(Y combinator)。限于篇幅,本文不会介绍 Y 组合子的推导过程。如果你对 Y 组合子是如何被推导出的感兴趣,你可以参阅这篇文章

Y 组合子在 call-by-name 和 call-by-value 求值策略下的形式是不同的,在 call-by-name 求值策略下的形式更加广为人知:

Y = \lambda f.\; \left(\lambda x.\; f\; \left(x\; x\right)\right)\; \left(\lambda x.\; f\; \left(x\; x\right)\right)

Y 组合子在 call-by-value 求值策略下的形式则稍有不同,某些文献中将其称为 Z 组合子

Y = \lambda f.\; \left(\lambda x.\; f\; \left(\lambda y.\; x\; x\; y\right)\right)\; \left(\lambda x.\; f\; \left(\lambda y.\; x\; x\; y\right)\right)

显然,Y 组合子是个组合子(废话),它接收一个函数作为参数,Y 组合子将计算出这个函数的不动点。借助 Y 组合子,我们最终可以写出我们需要的 fct 函数为:

\text{fct} = Y\; g

我们可以对尝试对上式进行求值:

\begin{aligned} \text{fct} =&\; \underline{Y}\; g \\ =&\; \underline{\left(\lambda f.\; \left(\lambda x.\; f\; \left(\lambda y.\; x\; x\; y\right)\right)\; \left(\lambda x.\; f\; \left(\lambda y.\; x\; x\; y\right)\right)\right)\; g} \\ \rightarrow&\; \underline{\left(\lambda x.\; g\; \left(\lambda y.\; x\; x\; y\right)\right)\; \left(\lambda x.\; g\; \left(\lambda y.\; x\; x\; y\right)\right)} \\ \rightarrow&\; g\; \left(\lambda y.\; \underline{\left(\lambda x.\; g\; \left(\lambda y^\prime.\; x\; x\; y^\prime\right)\right)\; \left(\lambda x.\; g\; \left(\lambda y^\prime.\; x\; x\; y^\prime\right)\right)}\; y\right) \\ =&\; g\; \left(\lambda y.\; \underline{Y\; g}\; y\right) \\ =&\; g\; \underline{\left(\lambda y.\; \text{fct}\; y\right)} \\ =&\; g\; \text{fct} \end{aligned}

因此,fct 确实是 g 的不动点。问题解决!

Formalities

本节将介绍 pure lambda-calculus 的 syntax 以及 operational semantics。

Syntax

V 表示所有合法的变量名的集合。 Pure lambda-calculus 的 syntax,即所有可能的 term 的集合 T,可以由以下三条规则递归地定义出:

  1. \forall x \in V\; \left(x \in T\right);
  2. 如果 t_1 \in Tx \in V,那么 \lambda x.\; t_1 \in T
  3. 如果 t_1 \in Tt_2 \in T,那么 t_1\; t_2 \in T

上述定义是很容易理解的,在此不做赘述。

我们可以基于 pure lambda-calculus 的 syntax 定义出一个后文需要使用的集合 FV,即一个 term 中所有的自由变量的集合:

\begin{aligned} FV\left(x\right) &= \left\{x\right\} \\ FV\left(\lambda x.\; t_1\right) &= FV\left(t_1\right) \backslash \left\{x\right\} \\ FV\left(t_1\; t_2\right) &= FV\left(t_1\right) \cup FV\left(t_2\right) \end{aligned}

其定义也非常容易理解,在此不做赘述。

Substitution

前文已经介绍了 pure lambda-calculus 中的 substitution 操作,即 \left[x \mapsto y\right] t 表示将 t 中所有的名为 x 的自由变量替换为 y 后所得到的结果。这一过程可以严格地基于 pure lambda-calculus 的 syntax 递归地定义出来:

\begin{aligned} \left[x \mapsto s\right]x &= s & \\ \left[x \mapsto s\right]y &= y & \text{if}\; x \ne y \\ \left[x \mapsto s\right]\left(\lambda y.\; t_1\right) &= \lambda y.\; \left[x \mapsto s\right] t_1 & \text{if}\; x \ne y \;\text{and}\; y \notin FV\left(s\right) \\ \left[x \mapsto s\right]\left(t_1\; t_2\right) &= \left[x \mapsto s\right]t_1\; \left[x \mapsto s\right]t_2 \end{aligned}

上面的定义的大部分内容应该是很容易理解的。这里重点讨论一下第三行定义的规则。第三行规则规定了如何对一个 abstraction 进行 substitution。这时存在一些需要特殊处理的情况,如下:

\begin{aligned} \left[x \mapsto s\right]\left(\lambda x.\; x\right) \\ \left[x \mapsto s\right]\left(\lambda s.\; x\right) \end{aligned}

对于第一种情况,如果不加以限制,我们会将一个约束变量替换为一个自由变量,显然破坏了程序的含义,因此需要对第三行规则施加 x \ne y 这一约束;同理,对于第二种情况,如果不加以限制,我们会将一个自由变量替换为一个约束变量,同样破坏了程序的含义,因此需要对第三行规则施加 y \notin FV\left(s\right) 这一约束。

然而,在向第三行规则添加上述的两个约束条件后,我们发现我们无法对上面的两种情况进行 substitution 了。解决这个问题的方法非常简单,我们只需要首先将变量名冲突的约束变量进行重命名,重命名后冲突即消除,可以正常执行 substitution。例如,对于 \left[x \mapsto s\right]\left(\lambda x.\; x\right),我们可以首先将其中的约束变量 x 重命名为 y,重命名后即是 \left[x \mapsto s\right]\left(\lambda y.\; y\right),然后再执行 substitution 即可得出正确结果。同理,对于 \left[x \mapsto s\right]\left(\lambda s.\; x\right),我们可以首先将其中的约束变量 s 重命名为 y,重命名后即是 \left[x \mapsto s\right]\left(\lambda y.\; x\right),然后再执行 substitution 即可得出正确结果。

上述的这个对约束变量进行重命名以消除命名冲突的过程称为 alpha-conversion。利用 alpha-conversion 解决了上述命名冲突问题后的 substitution 称为 substitution up to alpha-conversion,或称 substitution up to renaming of bound variables

Operational Semantics

下图给出了 pure lambda-calculus 在 call-by-value 求值策略下的 operational semantics。

上面的 operational semantics 定义的含义应该非常容易理解,在此不再赘述。其中有几个有意思的点值得讨论。

首先,从左栏的 syntax 中可以得知,所有的值(normal form)都是 abstraction(即函数)。

其次,右栏中定义的求值规则其实经过了精心设计,保证了所有的 term 均按照 call-by-value 策略进行求值,且求值方式是唯一的:

  • 首先,对于一个 application x\; y,如果 x 不是一个值,那么只能应用 E-App1 这一条规则进行求值,单步求值后的结果是将 x 变为一个值;
  • 其次,对于一个 application x\; y,如果 x 是一个值但 y 不是一个值,那么只能应用 E-App2 这一条规则进行求值,单步求值后的结果是将 y 变为一个值;
  • 最后,对于一个 application x\; y,当 xy 都是值时,只能应用 E-AppAbs 这一条规则进行求值,单步求值后的结果即是 substitution 的结果。

综上,右栏中的求值规则对所有的 term 唯一地确定了一条求值路线,即首先将最外层的 application 的第一个操作数(即需要被应用的函数)求值为一个值,然后再将最外层的 application 的第二个操作数(即需要传递给被应用的函数的参数)求值为一个值,最后再执行一次 substitution 作为 application,并不断反复这个过程,直到整个 term 被变换为一个值。这正是 call-by-value 求值策略所规定的求值路线。

标签:

发表回复