5

在 lambda 演算中，如果一个项具有范式，则常规降阶策略总是会产生它。

我只是想知道如何严格证明上述命题？

4

1 回答 1

4

您提到的结果是所谓的标准化定理的推论，指出对于任何简化序列 M-> N 在相同的术语 M 和 N 之间存在另一个“标准”，您可以在其中以最左边的最外层顺序执行 redexes。证明不是那么简单，文献中有几种不同的方法。我在下面添加了一个简短的参考书目。

Kashima 最近的证明5（另见1）具有不使用残差概念和基于纯归纳技术的优点。它对形式化2也有好处，但除非你对这个主题没有信心，否则它并不是特别有指导意义。

标准化背后的总体思路如下。假设有两个 redexes R 和 S，其中 S 相对于 R 位于最左边的最外面的位置，并考虑以下归约：

                R      S
             M  ->  P  ->  N

然后，您可以开始触发 S，但通过这种方式，您可能会复制（或删除）redex R。这些 redex，本质上是触发 S 后 R 的剩余部分，称为残差，通常表示为 R /S（读取：S 之后的 R 的残差）。所以，基本的引理是

             R S = S (R/S)

为了将它用于标准化，我们需要将 R 推广到任意序列 ρ（我们可以假设它是标准的，在 S 的最左边最外面的位置没有 redex）。仍然是真的

         (*) ρS = S (ρ/S)

但不那么明显的是 (ρ/S) 的标准化。为此，让我们观察 ρ 是在触发 S = C[\xM N] 之前执行的，这基本上将术语分为三个不连贯的区域：上下文 C、M 和 N。这导致 ρ 在三个连续的区域中重新分配序列：

           ρ1   inside M
           ρ2   inside N
           ρ3   inside C

（请记住，没有 redex 位于 S 的最左侧最外面的位置）。唯一可以复制（或删除）的部分是 ρ2，并且残差 ρ2-0 ... ρ2-k 很容易根据 S 的发射产生的 k 个 N 副本的不同位置排序。所以

   S ρ1 ρ2-0 ... ρ2-k ρ_3

是 (*) 的标准版本。

基本参考书目。

1 A.Asperti，JJ。征收。lambda-calculus 中的使用成本。LICS 2013。

3 HP Barendregt。Lambda 微积分，北荷兰（1984 年）。

4 G.Gonthier，JJ。宾夕法尼亚州利维。梅丽丝。一个抽象的标准化定理。LICS '92。

2 F.圭迪。为 Matita 定理证明器形式化的纯 Lambda 微积分中的标准化和汇合。形式化推理杂志 5(1):1-25, 2012。

5 R.鹿岛。λ演算中标准化定理的证明。技术报告 C-145，东京工业大学，2000 年。

[6] JW。克洛普。组合还原系统。博士论文，CWI，阿姆斯特丹，1980。

[7] G.米奇克。λ演算的标准化定理。Z. Math.Logik。格伦德拉格。数学，25:29–31, 1979

[8] M.高桥. λ演算的并行减少。信息与计算 118，第 120-127 页，1995。

[9] H. Xi，标准化的上限和应用。Symboloc Logic 杂志 64，第 291-303 页，1999。

于 2017-02-02T13:32:45.503 回答