c21*_*c21 5 lambda-calculus evaluation-strategy
在lambda演算中,如果一个术语具有正常形式,则正常的降阶策略将始终产生它.
我只是想知道如何严格证明上述命题？
您提到的结果是所谓标准化定理的推论，该定理指出，对于任何归约序列 M->N，相同项 M 和 N 之间存在另一个“标准”序列，其中您以最左边最外层的顺序执行 redexes。证明并不是那么简单，文献中有几种不同的方法。我在下面添加了一个简短的参考书目。
\n\nKashima 5最近的证明（另见1）具有不使用残差概念并且基于纯归纳技术的优点。这也有利于形式化2，但除非您对这个主题还没有信心，否则它并不是特别有指导意义。
\n\n标准化背后的总体思路如下。\n假设有两个 redexes R 和 S，其中 S 相对于 R 位于最左边最外面的位置，并考虑以下归约：
\n\n R S\n M -> P -> N\n然后，您可以开始触发 S，但通过这种方式，您可以复制（或擦除）redex R。这些 redex 本质上是触发 S 后 R 剩余的部分，称为残差，通常表示为 R /S（读作：S 之后 R 的残差）。\n所以，基本引理是
\n\n R S = S (R/S)\n为了将其用于标准化，我们需要将 R 概括为任意序列 \xcf\x81 （我们可以假设它是标准的，在 S 的最左边最外层位置没有 redex）。这仍然是事实
\n\n (*) \xcf\x81S = S (\xcf\x81/S)\n但不太明显的是 (\xcf\x81/S) 的标准化。为此，\n让我们观察 \xcf\x81 在触发 S = C[\\xM N] 之前执行，这\n本质上将术语分割为三个不相连的区域：上下文 C、M 和 N。\n这导致将 \xcf\x81 重新分区为三个连续序列：
\n\n \xcf\x811 inside M\n \xcf\x812 inside N\n \xcf\x813 inside C\n（请记住，S 的最左边最外位置没有 redex）。\n唯一可以复制（或擦除）的部分是 \xcf\x812，而残差\n\xcf\x812-0 ... \xcf\x812 -k 很容易根据由 S 的发射创建的 N 的 k 个副本的不同位置来排序。所以
\n\n S \xcf\x811 \xcf\x812-0 ... \xcf\x812-k \xcf\x81_3\n是 (*) 的标准版本。
\n\n基本参考书目。
\n\n1 A.阿斯佩尔蒂，JJ。征收。lambda 演算的使用成本。LICS 2013。
\n\n3 HP 巴伦德雷特。Lambda 微积分，北荷兰 (1984)。
\n\n4 G.Gonthier，JJ。宾夕法尼亚州利维。梅利斯。抽象标准化定理。LICS \xe2\x80\x9992。
\n\n2 F.吉迪。纯 Lambda 微积分的标准化和汇合 \n针对 Matita 定理证明器进行形式化。形式化推理杂志\n5(1):1\xe2\x80\x9325，2012。
\n\n5 R.鹿岛。lambda 演算中标准化定理的证明。\n技术报告 C-145，东京工业大学，2000 年。
\n\n[6] JW. 克洛普。组合减速系统。博士论文，CWI，\n阿姆斯特丹，1980 年。
\n\n[7]G.米奇克。lambda 演算的标准化定理。\nZ. 数学逻辑。根德滞后。数学，25:29\xe2\x80\x9331，1979
\n\n[8] M.高桥。lambda 演算的并行约简。\n信息与计算 118，第 120-127 页，1995 年。
\n\n[9] H. Xi，标准化上限和应用。《符号逻辑杂志》64，第 291-303 页，1999 年。
\n| 归档时间： |
|
| 查看次数： |
280 次 |
| 最近记录： |