チャーチ＝ロッサーの定理

ラムダ計算において、チャーチ・ロッサーの定理は、項に還元規則を適用する際、還元を選択する順序は最終的な結果に影響を与えないことを述べている。

より正確には、同じ項に適用できる 2 つの異なる還元または還元のシーケンスがある場合、追加の還元の (おそらく空の) シーケンスを適用することによって、両方の結果から到達可能な項が存在する。^{[ 1 ]}この定理は 1936 年にアロンゾ・チャーチとJ. バークレー・ロッサーによって証明され、彼らにちなんで名付けられました。

この定理は、隣の図で象徴的に表されます。項a がbとc の両方に還元できる場合、 bとcの両方に還元できる別の項d ( bまたはcのいずれかに等しい可能性がある)が存在しなければなりません。ラムダ計算を抽象的な書き換えシステムと見なすと、チャーチ・ロッサーの定理は、ラムダ計算の還元規則が合流的であることを述べています。この定理の結果として、ラムダ計算の項は最大で 1 つの正規形を持ち、与えられた正規化可能な項の「正規形」を参照することが正当化されます。

1936年、アロンゾ・チャーチとJ・バークレー・ロッサーは、 λI計算（抽象化された変数はすべて項の本体に現れる必要がある）におけるβ還元についてこの定理が成り立つことを証明した。証明方法は「展開の有限性」として知られており、標準化定理などの追加的な帰結がある。標準化定理は、還元を左から右に実行して正規形（存在する場合）に到達できる方法に関連している。純粋な型なしラムダ計算の結果は、1965年にDE・シュレーアーによって証明された。^{[ 2 ]}

純粋型なしラムダ計算において、チャーチ・ロッサーの定理が適用される還元の一種はβ還元であり、その形式の部分項は${\displaystyle (\lambda xt)s}$置換によって契約が締結される${\displaystyle t[x:=s]}$、 どこ${\displaystyle t,s}$は 2 つのラムダ式です。β 縮小は次のように表されます。${\displaystyle \rightarrow _{\beta }}$そしてその反射的、推移的閉鎖は${\displaystyle \twoheadrightarrow _{\beta }}$すると、チャーチ・ロッサーの定理は次のようになる。^{[ 3 ]}

$\displaystyle \forall M,N_{1},N_{2}\in \Lambda$ :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{かつ}}\ M\twoheadrightarrow _{\beta }N_{2}\ {\text{ならば}}\ \exists X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{かつ}}\ N_{2}\twoheadrightarrow _{\beta }X}

この性質の結果として、2 つの項が等しくなります${\displaystyle \lambda \beta }$共通項に還元する必要がある: ^{[ 4 ]}

${\displaystyle \forall M,N\in \Lambda$ :{\text{if}}\ \lambda \beta \vdash M=N\ {\text{then}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{and}}\ N\twoheadrightarrow _{\beta }X}

この定理はη還元にも適用され、その部分項は${\displaystyle \lambda x.Sx}$に置き換えられます${\displaystyle S}$これは、2つの還元規則の和集合であるβη還元にも適用される。

チャーチ・ロッサーの定理は、単純型付きラムダ計算、高度な型システムを持つ多くの計算体系、ゴードン・プロトキンのベータ値計算など、ラムダ計算の多くの変種にも当てはまります。プロトキンはまた、チャーチ・ロッサーの定理を用いて、関数型プログラムの評価（遅延評価と即時評価の両方）が、プログラムから値（ラムダ項のサブセット）への関数であることを証明しました。

古い研究論文では、書き換えシステムが合流性を持つ場合、それはチャーチ・ロッサーである、またはチャーチ・ロッサー特性を持つと言われます。

• Alama, Jesse (2017). Zalta, Edward N. (編).スタンフォード哲学百科事典(2017年秋 版). スタンフォード大学形而上学研究室.
• Church, Alonzo ; Rosser, J. Barkley (1936 年 5 月)、「変換のいくつかの性質」(PDF)、アメリカ数学会紀要、39 (3): 472–482、doi : 10.2307/1989762、JSTOR 1989762 。
• Barendregt, Hendrik Pieter (1984) 『ラムダ計算：その構文と意味論』、論理学と数学の基礎に関する研究、第 103巻（改訂 版）、North Holland、アムステルダム、ISBN 0-444-87508-52004年8月23日にオリジナルからアーカイブされました訂正​​