0

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

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 0)))，通过给出自然教堂编码的定义集（0，并且只有 succ）。

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

4

1 回答 1

2

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

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

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

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

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

于 2021-07-12T20:44:42.930 回答