私はラムダ計算を研究しており、最近チャーチ・ロッサーの定理を見ました。この定理は、ラムダ計算の項に縮約規則を適用する場合、縮約が選択される順序は最終的な結果に違いをもたらさないと述べています (wiki から)。しかし、これは値による呼び出しの削減や通常の順序の削減と矛盾していると思います。たとえば、ラムダ項 λz.(λx.x) y は、通常の次数簡約規則に従うと、λz.z に簡約できます。ただし、値による呼び出しの削減は λ 抽象化内での削減を禁止するため、値による呼び出しの削減を使用する場合、それ以上削減することはできません。したがって、項項 λz.(λx.x) y は、異なるルールを使用して同じ結果に評価することはできません。これは、チャーチ・ロッサーの定理と矛盾しているようです。ここで何が問題なのですか？助けてください。どうもありがとうございました!
1 に答える
0
あなたはチャーチ・ロッサーの定理について不正確だと思います。それが混乱の原因です。
私が理解している限り（そして、「関数型プログラミング言語の実装」を手元に置いてこれを書いています）、定理は次のように述べています。
2 つのラムダ式 E と F が任意の縮約シーケンスによって相互変換可能である場合、式 G が存在し、E と F の両方を G に縮約できます。
このことから、1 つの式が2 つの異なる正規形を持つことはできません(ただし、正規形はまったく存在しない可能性があります)。ただし、2 つの削減命令が与えられた場合、一方は通常の形式になり、他方は発散する可能性があります。
さて、あなたの場合、E = \z.zは通常の形式であり、F = \z.((\x.x) z)*はそれに還元できます。ここで言える唯一のことは、 をF以外に減らすことはできないということですがE、どれだけ減らす必要があるかについては何も言われていません。
定理には別の部分もあり、正規形が存在する場合、正規の順序でそれが見つかるというものです。繰り返しますが、値による呼び出しと名前による呼び出しは通常の順序とは異なる結果になる可能性があるため、観察に矛盾はありません。
*後者は意味をなさないため、これは の代わりに意味したと思います\z.((\x.x) y)。
于 2015-11-23T22:44:00.007 に答える