如何在基于 lambda 演算的系统中将 beta 归约还原为命名函数？

Posted 2023-03-15

【中文标题】如何在基于 lambda 演算的系统中将 beta 归约还原为命名函数？

【英文标题】：How to revert beta-reductions to named functions in a lambda calculus-based system?

【发布时间】：2021-09-21 19:18:06

【问题描述】：

好吧，假设我在教堂编码中有一组功能定义（带有语法树）：

true : λx -> λy -> x
false : λx -> λy -> y

给定定义 λx -> λy -> y，很清楚如何返回命名定义，应用与 alpha 等价的匹配就足够了。

α true λx -> λy -> y = false
α false λx -> λy -> y = true

但请考虑以下示例：

0 : λf λz -> x
succ : λn λf λx -> f (n f x)
3 : succ (succ (succ 0)))

因此，当 3 遭受 beta 减少时，它将展开为某种定义，例如：

3_unfolded : (λf -> (λx -> (f (f (f x))))) : (A -> A) -> A -> A

您可以看到术语很容易变大，当然，由于术语的大小，这不是表示纯数据的好方法。所以，我想知道是否有一种算法能够在经过评估后有效地重新命名每个定义。它们3_unfolded会再次变成(succ(succ(succ(succ 0))))，通过给出自然教会编码的定义集(0，并且只有succ)。

我知道有一些副作用，比如模棱两可的表示，但让我们忽略它（例如，如果您扩展 succ 的相同定义并重命名为 succ_2）。

【问题讨论】：

“给出定义 λx -> λy -> x，很清楚如何返回命名的定义”您能否展示一下（包括在您的问题中），以便清楚您的意思通过那个。你的意思是，检测它实际上是true？如果是这样，问题就变成了，你用什么 Haskell 术语来代表你的“λx -> λy -> x”实体？

我无法理解目标。您不能检查标准形式是否包含教堂数字并将其替换为所需的等价物吗？相反，目标是否更普遍？如果是这样，你应该从精确的形式化开始。

Beta 等价性无法确定。

...我也不认为 3 在 lambda 演算的通常语义下计算为 3_unfolded。为此，您必须在活页夹下进行评估，而这...通常不会完成。从根本上来说这并没有什么坏处，它只是让程序员更难编写一个可靠地终止的程序。

这就像试图通过它的输出来恢复一个程序。当然，您总是可以将输出推入“打印”语句并宣布胜利，但当然有无数程序产生相同的输出。你想要最短的吗？ （不可能）最人性化的一个？ （您如何定义？）

【参考方案1】：

这本质上是beta-equivalence的问题，一般是不可判定的；它也不一定会产生 usable 输出，即使它可以产生 something，例如有一些限制，包括强标准化。因此我认为你最好的策略是启发式的，因为默认情况下，减少会破坏信息。解决方案是保留您关心的信息，或避免需要已丢失的信息。例如：

将术语的记忆表示与它们的 LC 表示分离，尤其是在您关心效率和可用性的情况下。例如，您可以将 Church 数字存储和打印为 Natural，同时仍允许根据需要将其转换为函数。我觉得这是最实用的技术角度。

保留有关每个术语出处的信息，并将其用作提示来重构命名术语。例如，如果您知道某个术语是由给定的 beta-reduction 产生的，您可以 beta-expand/alpha-match 以可能重新发现 succ 等函数的应用。这在简单的情况下可能会有所帮助，但我希望它会在非平凡的程序中失效。

不要将其视为算法问题，而应将其视为可用性设计问题，并专注于识别有用信息并清晰呈现的方法。例如，搜索 最大 匹配的函数体，它也是 最具体的，例如一个术语可能同时匹配λx. x（身份）和λf. λx. f x（函数应用程序），但后者更具体，甚至更具体地它可以是一个数字（λs. λz. s z = 1）；如果有多种可能性，请提出最有可能的少数。

当您遇到任意程序无法确定的问题时，值得记住的是，人类编写非常非任意程序。因此，启发式解决方案在实践中非常有效。

【讨论】：

我认为第一种方法最适合我。在大多数情况下，启发式方法会很好，但是，相信本地解决方案可能在未来对我来说是个问题。在积极标准化的情况下，保留信息也过于复杂，并且可能会浪费内存。我将避免 beta 等效问题。谢谢你的回答乔恩，很清楚。