Lambda 演算 第5章 ISWIM

第5章 ISWIM

Church发明了λ演算作为了学习计算的一种方式，明显地和机器计算相反。在20世纪60年代，Landin证明了Church的演算，事实上对于大多数编程语言的模型都不太合适。比如，以下λ-演算表达式：

(λx.1) (sub1 λy.y)

将归约到（编码的）1，然而大多数语言会埋怨(sub1 λy.y)。该问题不仅仅在于编码sub1和λy.y，而且对整个表达式的β归约会完全忽略参数(sub1 λy.y)。

这种callby-name是否可取尚待商榷。无论如何，许多语言不支持callby-name。相反，它们支持callby-value，其中在应用函数之前，必须对函数的参数进行完全求值。

在本章中，我们将介绍Landin的ISWIM，它更紧密地模拟了诸如Scheme和ML等callby-value语言的核心。ISWIM的基本语法与λ演算相同，以及自由变量和替代的概念也是相同的。不同于λ-演算，并更像真正的编程语言，ISWIM带有一组基本常量和基本操作。但更本质的区别是ISWIM的call-by-value归约规则。

5.1 ISWIM表达式

ISWIM的语法扩展了λ-演算的语法：

image.png

仅当n = m时表达式（oⁿ M₁ ... M_m）有效。我们可以使用多种方式定义集合 b 和 oⁿ，语言的高级属性将保持不变，为了具体起见，我们将对 b 和 oⁿ使用以下定义：

image.png

其中句法对象 [1] 代表整数 1 。句法对象 + ，代表一个加法操作，↑ 是求幂。此外，我们定义一个有用的宏 if0:

image.png

FV和[←]关系以明显的方式扩展到新语法：

image.png

5.2 ISWIM 归约

由于ISWIM中的函数仅接受完全求值的参数，因此我们必须首先定义值的集合。值集V（别名U和W）是表达式的子集：

image.png

特别是，一个程序表达式绝不是值，而抽象（即函数）不论其形式如何，始终是一个值。

ISWIM的核心归约关系为βv，它类似于β，其不同之处在于参数必须在V中而不是M中：

image.png

将参数限定为V的成员，会在一定程度上强制求值的顺序。例如，((λx.1)(sub1 λy.y))不能用 βv 归约为1，因为(sub1 λy.y)不是V的成员。类似地，必须按顺序将 ((λx.1) (sub1 1)) 归约为 ((λx.1) 0) ，然后归约为1。

ISWIM没有类似于 η 的关系，这反映了一个事实，即编程语言实现通常不会提取应用在另一个主体中的函数功能。 此外，从现在开始，我们通常在比较时使用 α-等价 (=α) 表达式，而不是将α视为简化。

除了函数程序之外，ISWIM归约规则还需要考虑元操作。与 b 和 oⁿ 相同，元操作原则上是抽象的（即使我们定义了具体的集合），与元操作相关联的归约表示为抽象δ。δ关系映射每个 oⁿ 加 n 个基本常数为一个值。

我们选择以下δ：

image.png

通过组合β和δ，我们得出完整的约简关系v：

image.png

像之前一样，→v是v的兼容闭包，→→v 是 →v 的自反传递闭包，=v 是 →→v 的对称闭包。

练习题5.1 通过→v，写出以下表达式的归约值:

image.png

Y_v 组合器

对于纯λ-演算，我们定义了一个函数Y，该函数可找到任何表达式的不动点，因此可以用来定义递归函数。尽管在ISWIM中仍然如此，(f (Y f)) 与任何f的(Y f)相同，事实证明这是无用：

Y f = (λf.(λx.f (x x)) (λx.f (x x))) f
    →v (λx.f (x x)) (λx.f (x x))
    →v f ((λx.f (x x)) (λx.f (x x)))

问题在于上面程序最外层中f的参数不是值，并且无法将其归约为一个值，因此 (Y f) 永远不会产生承诺的不动点函数。

我们可以通过将Y内的每个程序M更改为(λX.M X)来避免无限归约，因为该程序仍然应该返回一个函数。逆-η变换将值替换为无限归约的程序。 最终结果是Y_v组合器：

image.png

Y_v组合器在应用于接受一个函数并返回另一个函数的函数时起作用。

定理 5.1 [Y_v的不定点定理]: If K = λgx.L, then (K (Y_v> K)) =_v (Y_v K).

定理 5.1 的证明: 该证明是一个简单的计算，其中所有基本证明步骤是β_v步骤：

(Yv K)
= ((λf.λx.((λg.(f (λx.((g g) x)))) (λg.(f (λx.((g g) x)))) x)) K)
→v λx.(((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x))))) x)
→v λx.((K (λx.(((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x))))) x))) x)
→v λx.(((λgx.L) (λx.(((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x))))) x))) x)
→v λx.((λx.L[g ← (λx.(((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x))))) x))]) x)
→v λx.L[g ← (λx.((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x)))) x))]
v← ((λgx.L) (λx.((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x)))) x)))
= (K (λx.((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x)))) x)))
v← (K (Yv K))

定理5.1的证明看起来过于复杂，因为应用过程的参数必须是β_v的值。 因此，而不是计算

  λx.((K (λx.(((λg.(K (λx.((g g) x)))) (λg.(K (λx.((g g) x))))) x))) x)
= λx.((K (Yv K)) x)
= λx.((λgx.L) (Yv K)) x)

我们需要持有由(Yv K)计算的值。为了在将来避免这种复杂性，一个被我们证明的论点（即可证明等于一个值的论点（但不一定是值））已经可以使用，就好像它是=_v的值一样。

定理 5.2: If M =_v V , then for all (λX.N), ((λX.N) M) =_v N[X ← M].

定理 5.2 的证明: 证明的初始部分是一个简单的计算：

((λX.N) M) =v ((λX.N) V ) =v N[X ← V ] =v N[X ← M]

但是，此计算的最后一步需要通过归纳法单独证明N，如果M =v L，则N[X←M] =v N[X←L]：

• Base cases:
    – Case N = b
      b[X ← M] = b =v b = b[X ← L].
    – Case N = Y
      If Y = X, then X[X ← M] = M =v L = X[X ← L]. Otherwise,
      Y [X ← M] = Y =v Y = Y [X ← L].
• Inductive cases:
    – Case N = (λY.N')
      If Y = X, then N[M ← X] = N =v N = N[L ← X]. Otherwise, by induction, N'[X ← M] =v N'[X ← L]. Then,
          (λY.N')[X ← M]
          = (λY.N'[X ← M])
          =v (λY.N'[X ← L])
          = (λY.N')[X ← L]
    – Case N = (N1 N2)
      By induction, Ni[X ← M] =v Ni[X ← L] for i ∈ [1, 2]. Then,
          (N1 N2)[X ← M]
          = (N1[X ← M] N2[X ← M])
          =v (N1[X ← L] N2[X ← L])
          = (N1N2)[X ← L]

    – Case N = (on N1 ... Nn)
      Analogous to the previous case.

5.4 求值

对于定义一个求值器，ISWIM中把函数作为值，衍生了与λ-演算同样多的问题。例如，以下表达式：

(λx.x) (λy.(λx.x) [0])

显然等于

λy.(λx.x) [0]

和

λy.[0]

我们应该选择哪个作为求值器的结果？虽然所有这些结果都有望代表一个相同的函数，也很显然，有无数种方法可以代表一个函数。因此，我们采用的解决方案基本上是所有实际编程系统实现：当程序归约到一个函数值时，eval_v函数仅仅返回一个token表明该值是一个函数。

我们将A定义为求值ISWIM函数的结果集：

image.png

偏函数eval_v定义如下：

image.png

如果evalv(M)不存在，我们说M是发散的。例如，Ω是发散的.

练习题 5.2 假设我们想要加强求值函数，如下所示：

image.png

eval₁ 是函数吗？如果是，请证明。如果不是，提出反例。

5.5 一致性

ISWIM求值器的定义取决于ISWIN等式演算。尽管演算基于直观的论证，且几乎与算数系统一样容易使用，然而该求值器作为程序的函数，它是否返回唯一结果，远非显而易见。但对于需要确定、可靠编程语言的程序员而言，这个问题至关重要。简而言之，为了ISWIM的eval_v，我们需要修改eval_r的一致性定理。这个定理的证明还很遥远，尽管它遵循相同的规范，但它比eval_r更为复杂。

我们从基本定理开始，该定理断定了ISWIM演算的Church-Rosser属性。

定理 5.3 [eval_v的一致性] 关系eval_v是一个偏函数。

定理 5.3 证明 假设Church-Rosser属性有： 如果 M =_v N，则存在一个表达式L，使得 M →→_v L 且 N →→_v L。

设 evalv(M) = A1 and evalv(M) = A2 ，其中A1 和 A2 是结果，我们需要证明 A1 = A2。基于ISWIM结果的定义，我们分两种情况：

• Case A1 ∈ b, A2 ∈ b
  由Church-Rosser得出结论是，当且仅当两个基本常数相同时，两个基本常数才可证明相等，因为这两个常数都是不可约的。

• Case A1 = function, A2 ∈ b
  根据 eval_v的定义，对于某些N，有 M =_v A2 和 M =_v λx.N，所以 A2 =_v λx.N。再次由Church-Rosser和常数的不可约性，得λx.N →→_v A2。但根据归约关系→→_v的定义，λx.N →→_v K 表明，K = λx.K0。因此，λx.N不可能减小到A2，这意味着该情况的假设是矛盾的。

• Case A1 ∈ b, A2 = function
  与前面的情况类似。

• Case A1 = function, A2 = function
  Then A1 = A2.

这些都是可能的情况，因此，A1 = A2总是正确的，因此eval_v是一个函数。

通过前面的证明，我们将一致性属性归约为关于ISWIM的Church-Rosser属性。

定理 5.4 [Church-Rosser for ISWIM] 如果 M =_v N，那么存在一个表达式L，使得M →→_v L 且 N →→_v L。

定理 5.4 证明 该证明本质上是 =_r 证明的副本（定理3.2），对于归约关系→→_v，它假设为菱形。

处理一致性和Church-Rosser定理后，我们来到了该问题的核心部分。现在我们需要证明ISWIM的菱形属性。

定理 5.5 [关于 →→v 的菱形属性] 如果L→→v M 且 L→→v N，那么存在一个表达式 K，使得 M →→v K 且 N →→v K。

对于→→r，一个类菱形属性有单步关系→r，菱形由此产生传递闭包的属性很容易理解。 但是，类似于前面章节的示例，很明显菱形属性不能满足→v。βv归约可以复制函数参数中的redexes，可防止共同合约的存在在某些菱形中。例如，考虑表达式:

image.png

其中包含两个重叠且带下划线的βv-redex。 由两者之一，我们得到表达式：

image.png

这两个表达式都包含redexe，但如下图所示，从这些表达式开始的单步归约，不会得到通用表达式。

image.png

因此，单步归于关系 →v 不能满足菱形属性。

由于基于v的单步归约的问题是由重复redexes的归约导致的，我们考虑一个表达式,→v，它在单步归约→v基础上，并行收缩多个不重叠的redex。如果该扩展满足菱形属性，并且如果它的传递-自反闭包等同于→v，我们就可以证明→→v的菱形属性了。
并行扩展 ,→v 的定义如下：

image.png

该关系满足菱形属性。

定理 5.6 [Diamond Property for ,→v] 如果 L ,→v M 且 L ,→v N, 那么存在一个表达式 K ，使得 M ,→v K 且 N ,→v K。

定理 5.6 证明 通过归纳 L ,→v M 的证明树结构。

image.png
image.png

为了完成前面的证明，我们需要证明，与并行归约相关的表达式中的替换，不影响归约步骤。

image.png image.png

观察等价

除了程序求值外，程序的转换在以下两个方面扮演重要角色：编程的实践以及编程语言的实现。例如，如果M是一个过程，如果我们认为另一个过程N，它可执行与M相同的计算，并且速度更快，那么我们想知道M是否真的可以与N互换。对于这个问题的一个特殊实例，ISWIM显然提供了一种解决方案：如果两个表达式都完成程序，我们知道M =_v N，然后eval_v(M) = eval_v(N)，我们知道我们可以用N代替M。

然而，通常来讲，M和N是某个程序的子表达式，我们可能无法独立求值它们。因此，我们真正需要的是一个通用关系，该关系解释表达式何时“在功能上等价”。

要理解“功能等价”的概念，我们必须记得，程序的用户只能观察输出，并且主要对输出感兴趣。 程序员通常不知道程序的文本或文本的任何方面。 换句话说，这种观察者将程序视为黑箱，以未知的方式产生一些值。因此，很自然地说表达式的结果就是当它成为程序的一部分时所具有的结果。

在继续之前，我们需要一个表达式上下文的概念。以下语法C定义了一组近似表达式。它们不完全是表达式，因为在一个子表达式的位置，C的每个成员都包含一个空（书写为[]）。

image.png
image.png

与替换不同，填补上下文的空可以捕获变量。

通过上下文的这种定义，我们可以表达观察等价性的概念。当且仅当它们在所有上下文C中都无法区分时，两个表达式M和N在观察上是等价的，记为M '=v N。

image.png

该定义意味着，如果M '=v N，那么对于任何给定的C，必须要么同时定义evalv(C[M])和evalv(C[N]) ，要么未定义。

观察等价显然在eval_v上扩展了程序的等价性。 如果程序 M 和 N 在观察上等价，则它们是空上下文的程序，因此 evalv(M) = evalv(N)。但这也是我们从具有同等功能的表达式理论中所期望的最低要求。 顾名思义，观察等价是等价关系。最后，如果两个表达式在观察上是等价的，则将这些表达式嵌入上下文中应会产生在观察上等价的表达式。毕竟，添加的片段是相同的，并且不应影响表达式对程序输出。简而言之，观察等价关系是一个等价关系，即它对上下文的封闭也是等价关系。

image.png

事实证明，观察等价是满足我们直觉标准的最大的等价关系。

image.png image.png

该命题表明，观察等价是表达式上最基本，最基本的全等关系。所有其他关系仅近似于观察等价标识表达式的准确性。从这样的命题也可以得出，ISWIM在观测等效性方面是合理的。不幸的是，它也不完整。该演算不能证明所有的观测等价关系。

image.png

想要完成不完全性定理的证明，我们仍然缺少一些工具。在开发了有关ISWIM的一些基础知识之后，我们将在下一章中返回证明。

5.7 历史

在1960年代中期的一系列论文中[5]，Landin阐述了关于编程语言的两个重要观点。首先，他认为所有编程语言都共享一组用于指定计算的基本功能，但是在数据和数据原语的选择上有所不同。通用功能集包含名称，过程，应用程序，异常机制，可变数据结构，以及可能的其他形式的非本地控制。用于数字应用程序的语言通常包括几种形式的数字常量和大量数字原语，而用于字符串操作的语言通常提供有效的字符串匹配和操作原语。

其次，他敦促程序员和语言实现者都应将编程语言视为算术和代数的高级符号形式。由于我们所有人都习惯于计算幼儿园，高中时期的数字，布尔值，甚至更复杂的数据结构，因此使用程序进行计算也应该很容易。程序求值，程序编辑的许多形式，程序转换和优化只是不同的，更复杂的计算形式。它们处理程序和程序段，而不是简单算术表达式罢了。

Landin定义了编程语言ISWIM。他的设计基础是丘奇（Church）的λ演算，这个自然的起点给了Landin深刻见解，这个程序的中心作用，就像所有语言的通用设施。但是，为了支持基本数据和相关原语以及赋值和控制构造，Landin用适当的构造扩展了λ演算。他用抽象机器指定了扩展语言的语义，因为他不知道如何将λ微积分的方程式理论扩展到完整的编程语言的理论。事实证明，由于ISWIM始终会评估过程的参数，因此λ演算甚至都不能解释纯函数子语言的语义。 因此，Landin并没有完成他打算要做的事情，即定义所有编程语言的理想化核心和定义其语义的方程式演算。

从普洛特金（Plotkin）在1970年代中期开始研究抽象机与方程式计算之间的关系[7]以来，兰丹的工作中的空白已经被包括费勒森，梅森，塔尔科特及其合作者在内的许多研究人员填补。 Plotkin的工作涵盖了ISWIM的基本功能子语言，该语言需要定义λ演算的按值调用变体。 费莱森和他的同事们用公理扩展了等式理论，这些公理解释了几种不同的命令式语言设施。 梅森（Mason）和塔尔科特（Talcott）研究了将方程式理论用于类似于ISWIM的完整语言，作为程序验证和转换编程的工具。

尽管ISWIM尚未成为一种积极使用的语言，但ISWIM的哲学仍然存在于现代编程语言中，最显着的是Scheme和ML，它的语言分析和设计方法基本上适用于所有编程语言。 本书的目标之一是在编程语言设计和分析的背景下，说明λ演算等方程式理论的设计，分析和使用。