lambda-calculus - lambda 演算，正规阶，正规形式，

Question

在 lambda 演算中，如果一个项具有范式，则正常的降阶策略将始终产生它。

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

Answer 1

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

Kashima 最近的证明 5 (另请参阅 1 )的优点是不使用残差概念并且基于纯粹的归纳技术。也有利于形式化2 ，但除非你对这个主题还没有信心，否则它不是特别有指导意义。

标准化背后的一般思想如下。
假设有两个还原 R 和 S，其中 S 相对于 R 位于最左边的最外侧位置，并考虑以下归约:

                R      S
             M  ->  P  ->  N

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

             R S = S (R/S)

为了将其用于标准化，我们需要将 R 推广到任意序列 ρ(我们可以假设它是标准的，在最左边的最外层位置 w.r.t. 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

是 (*) 的标准版本。

基础书目。

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

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

4 G.Gonthier，JJ。利维，PA。梅利斯。 An abstract standardisation theorem . LICS '92。

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

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

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

[7] G.Mitschke。 lambda 演算的标准化定理。
Z. Math.Logik。格鲁拉格。数学，25:29–31，1979

[8] M.Takahashi。 lambda 演算的平行归约。
信息与计算 118，第 120-127 页，1995 年。

[9] 奚海， Upper bounds for standardizations and an application .符号逻辑杂志 64，第 291-303 页，1999 年。