Lambda演算、正则序、正则形式。

Question

在λ演算中，如果一个术语具有正规式，则正则序规约策略将始终产生它。

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

- c21

---

我认为你指的是Church-Rosser定理。 - nicolas

Answer 1

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

Kashima最近的证明5（也请参见1）具有不使用残差概念并基于纯归纳技术的优点。它也适用于形式化2，但除非您已经对该主题有信心，否则它并不特别有启发性。

标准化背后的一般思想如下。 假设有两个redexes R和S，其中S相对于R处于最左最外位置，并考虑以下缩减：

                R      S
             M  ->  P  ->  N

然后，你可以开始使用S来触发，但这样可能会复制（或删除）红块R。这些红块，在触发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

（记住在S中没有任何红式位于最左外位置。） 唯一可能复制（或擦除）的部分是ρ2，而剩余量ρ2-0 … ρ2-k根据S触发创建k个N的不同位置很容易排序，因此

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

这是(*）的标准版本。

基础参考书目。

1 A.Asperti, JJ. Levy. lambda演算中使用的成本。LICS 2013。

3 H. P. Barendregt. Lambda演算，North-Holland（1984年）。

4 G.Gonthier, JJ.Levy, PA.Mellies. 一个抽象的标准化定理. LICS '92.

2 F.Guidi. 为Matita定理证明器形式化的纯lambda演算中的标准化和合流. 《形式化推理杂志》5(1)：1-25，2012年。

5 R.Kashima. Lambda演算中标准化定理的证明. Technical Report C-145, 东京工业大学, 2000年.

[6] JW. Klop. 组合约简系统. 博士论文, 荷兰国家计算机与网络研究所, 阿姆斯特丹, 1980年.

[7] G.Mitschke. Lambda演算的标准化定理. 数学逻辑基础杂志, 第25卷, 第29至31页, 1979年.

[8] M.Takahashi. Lambda演算中的并行约简. 信息与计算, 第118卷, 第120至127页, 1995年.

[9] H. Xi, 标准化的上界及其应用. 符号逻辑杂志, 第64卷, 第291至303页, 1999年.

- Andrea Asperti