lambda演算，规范序，规范形式，

Question

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

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

Answer 1

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

鹿岛5 (另见1)最近的证明具有不使用残差概念和基于纯归纳技术的优势。它对形式化2也很有帮助，但是除非您对这个主题还不是很有信心，否则它不是特别有指导意义。

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

                R      S
             M  ->  P  ->  N

然后，你可以开始发射S，但通过这种方式，你可以复制(或擦除) redex R。这些redex本质上是在发射S之后R的剩余部分，称为残差，通常表示为R/S (读取:R在S之后的残差)。所以，基本的引理是

             R S = S (R/S)

为了使用它进行标准化，我们需要将R推广到任意序列ρ(我们可以假设它是标准的，在最左边最外面的位置w.r.t.没有redex。s)。这仍然是真的

         (*) ρ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.so创建的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。兰姆达微积分，北荷兰(1984)。

4 G.Gonthier，JJ.宾夕法尼亚州列维梅利。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.Kashima.A proof of the standardization theorem in lambda-calculus。技术报告C-145，东京工业大学，2000。

6 JW。克洛普。组合约简系统。PhD论文，CWI，阿姆斯特丹，1980年。

7 G.Mitschke。λ演算的标准化定理。Z. Math.Logik。Grundlag。数学，25:29-31,1979

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

9 H. Xi，Upper bounds for standardizations and an application。《符号逻辑杂志》64，第291-303页，1999年。