Church-Rosser の合流定理

• λ式 e からβ簡約をくりかえしてλ式 e' が得られるとき，e→→e' と書く．

定理 e→→e₁，e→→e₂ ならば，λ式 e₃ が存在して，e₁→→e₃，e₂→→e₃ となる．

• 以下これを証明する．

補題1 λ式 e の redex 集合 A と redex σ に対し，θ_A(e) の redex 集合 C と，θ_σ(e) の redex 集合 B が存在して，
θ_C(θ_A(e) ) = θ_B(θ_σ(e) )．

• 補題1の証明
  • A₁ = A∩σ↓, A₂ = A - A₁ とおく.
  • σ∈A の場合．
    θ_σ(e) の redex 集合 B₁⊂σ↓ が存在して，θ_A1(e) = θ_B1θ_σ(e).
    B = B₁∪ A₂ とおくと，
    θ_Bθ_σ(e) = θ_A2θ_B1θ_σ(e) = θ_A2θ_A1(e) = θ_A(e).

• • σ∉A の場合．
    θ_σ(e) の redex 集合 B₁⊂σ↓ が存在して，θ_σθ_A1(e) = θ_B1θ_σ(e).
    θ_A(e) の redex 集合 C が存在して， θ_Cθ_A(e) = θ _C θ_A2θ_A1 (e) = θ_A2θ_σθ_A1 (e)
    B = B₁∪ A₂ とおくと，
    θ_Bθ_σ(e) = θ_A2θ_B1θ_σ(e) = θ_A2θ_σθ_A1 (e) = θ_Cθ_A(e). //

• 補題1より次が従う．

補題2 e→→e'，A を e の redex 集合とすると，e' の redex 集合 B が存在して，θ_A(e)→→θ_B(e')．

• 補題2より定理が従う．qed.

http://www.cs.cornell.edu/~kozen/papers/ChurchRosser.pdf