lambda演算，正规顺序，正规形式，

Question

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

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

Answer 1

您提到的结果是所谓的标准化定理的推论，它指出对于任何简化序列 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[\x.M N] 之前执行的，即 本质上将术语拆分为三个不相关的区域：上下文 C、M 和 N。 这导致 ρ 在三个连续序列中重新分配：

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

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

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

是 (*) 的标准版本。

基本参考书目。

1A.Asperti，JJ。征收。 The cost of usage in the lambda-calculus。 LICS 2013。

3 H. P. Barendregt。 Lambda 微积分，北荷兰 (1984)。

4G.Gonthier, JJ。宾夕法尼亚州利维。梅丽丝。 An abstract standardisation theorem。 LICS '92。

2F.Guidi。 Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover。形式化推理杂志 5(1):1-25, 2012.

5R.Kashima。 A proof of the standardization theorem in lambda-calculus。 技术报告 C-145，东京工业大学，2000 年。

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

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

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

[9] H. Xi, Upper bounds for standardizations and an application. Symboloc Logic 64 杂志，第 291-303 页，1999 年。