是否可以有效地评估 lambda 演算项？

Question

我最近在 lambda 演算中编写了很多程序，我希望我可以实时运行其中的一些程序。然而，尽管趋势函数范式基于 lambda 演算和 B 归约规则，但我找不到一个不是玩具、不是为了提高效率的评估器。函数式语言应该很快，但我知道的那些实际上并不提供对正常形式的访问（请参阅 Haskell 的惰性求值器、Scheme 的闭包等），所以不要用作 LC 求值器。

这让我想知道：是否无法有效地评估 lambda 演算项，是否只是历史事故/没有人决定为其创建快速评估器的兴趣缺乏，还是我只是遗漏了什么？

Answer 1

在目前的知识状态下，评估 lambda 项的最佳方法是所谓的最优图缩减技术。该技术于 1989 年由 J.Lamping 在他的 POPL 文章“An algorithm for optimal lambda calculus reduction”中介绍，然后由几位作者进行了修订和改进。您可以在我与 S.Guerrini "The optimal implementation of functional programming languages" 合着的书中找到一份调查，Cambridge Tracts in Theoretical Computer Science n.45, 1998。

术语“优化”是指共享管理。在 lambda 演算中，你有很多重复，减少的效率至关重要 基于避免重复工作。在一阶设置中，有向无环 图形（dags）足以管理共享，但是一旦您输入更高阶的设置，您就需要更复杂的图形结构，包括 共享和取消共享。

在纯 lambda 项上，最优图形缩减比所有其他已知的更快 减少技术（环境机器，超级组合器或其他）。 上面的书中给出了一些基准（参见第 296-301 页），其中我们 证明我们的实现优于caml-light（前身 ocaml）和 Haskell（真的很慢）。 所以，如果你听到人们说它从未被证明是最优的 减少比其他技术更快，这是不正确的：证明了两者 理论和实验。

函数式语言还没有以这种方式实现的原因是 在函数式编程的实践中，你很少使用函数式 具有非常高的等级，并且当您这样做时，它们通常是线性的。 一旦你提高等级，lambda 的内在复杂性 条款可能会变得危险地高。有一种技术可以让你 及时减少一个术语 O(2^n) 而不是 O(2^(2^n)) 并不能使所有 这种差异，在实践中：两种计算都是不可行的。

我最近写了一篇短文试图解释这些问题： “About the efficient reduction of lambda terms”。 在同一篇文章中，我还讨论了超最优的可能性 减少技术。

Answer 2

评估 lambda 项有多种方法。根据类型信息是否可用，您可以获得更高效和更安全的评估器（不需要运行时检查，因为程序表现良好）。我将粗略地介绍一些技术。

大步评估员

与其反复定位 lambda-redexes 并触发它们（这意味着多次遍历该术语），您可以设计一种算法，通过“大步骤”评估一个术语来尝试最小化工作。

例如如果你想规范化的术语是t u，那么你规范化t和u，如果norm t是一个lambda抽象，你触发相应的redex并在你刚刚得到的术语上重新开始规范化。

抽象/虚拟机

现在，您可以使用抽象机器完成基本相同的工作，但速度要快得多。这些小型虚拟机具有自己的指令集和缩减规则，您可以用自己喜欢的语言实现这些指令并将 lambda-terms 编译成。

历史上的例子是SECD machine。

Danvy et al. 表明，众所周知的抽象机器可以通过延续传递风格和去功能化的组合从前面提到的评估器中派生出来。

要从抽象机器中获取 lambda 项，您需要实现一个reification / read back 函数，根据机器所处的状态构建一个 lambda 项。Grégoire and Leroy 展示如何这样的事情可以在语言的类型论是 Coq 的上下文中完成。

通过评估归一化

通过评估标准化是利用宿主语言的评估机制来实现另一种语言的标准化过程的做法。

Lambda 抽象变成宿主语言中的函数，应用程序变成宿主语言的应用程序，等等，等等。

这种技术可以以类型化方式使用（例如，标准化简单类型的 lambda 演算 in Haskell 或 in OCaml）或无类型的（例如，简单类型的 lambda-演算 once more 或 Coq terms编译为 OCaml (!))。