module plfa.part2.Confluence where

简介

在这一章我们将证明 β-归约是合流的（Confluent） （又被称作 Church-Rosser 性质）： 如果有从任一项 L 至两个不同项 M₁ 和 M₂ 的归约序列， 那么一定存在从这两个项至某个相同项 N 的归约序列。 如图：

    L
   / \
  /   \
 /     \
M₁      M₂
 \     /
  \   /
   \ /
    N

其中向下的线是 -↠ 的实例。

合流性（Confluence）也在许多 λ-演算外的重写系统中被研究， 并且如何在满足菱形性质（Diamond Property）， 一种合流性的单步版本的重写系统中证明合流性是广为人知的。 令 ⇛ 为一个关系。⇛ 具有菱形性质， 如果对于任何 L ⇛ M₁ 和 L ⇛ M₂ 都存在 N ， 使得 M₁ ⇛ N 和 M₂ ⇛ N。 这只是上图的另一个例子，此处向下的线代表 ⇛。 如果我们将 ⇛ 的自反传递闭包写作 ⇛*， 那么可以立即从菱形性质推出 ⇛* 的合流性。

不幸的是 λ-演算的归约并不满足菱形性质。这是一个反例：

(λ x. x x)((λ x. x) a) —→ (λ x. x x) a
(λ x. x x)((λ x. x) a) —→ ((λ x. x) a) ((λ x. x) a)

两个项都可以归约至 a a，但第二项需要两步来完成，而不是一步。

为了回避这个问题，我们将定义一个辅助归约关系， 称为平行归约（Parallel Reduction） ， 它可以同时执行许多归约并因此满足菱形性质。 更进一步地，我们将证明在两个项间存在平行归约序列当且仅当这两个项间存在 β-归约序列。 因此，我们可以将 β-归约序列合流性的证明约化为平行归约合流性的证明。

导入

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Function.Base using (_∘_)
open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
  renaming (_,_ to ⟨_,_⟩)
open import plfa.part2.Substitution using (Rename; Subst)
open import plfa.part2.Untyped
  using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; begin_; _—→⟨_⟩_; _—↠⟨_⟩_; _∎;
  abs-cong; appL-cong; appR-cong; —↠-trans;
  _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
  rename; ext; exts; Z; S_; subst; subst-zero; Context)

平行归约

平行归约关系被定义如下。

infix 2 _⇛_

data _⇛_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

  pvar : ∀{Γ A}{x : Γ ∋ A}
      ---------
    → (` x) ⇛ (` x)

  pabs : ∀{Γ}{N N′ : Γ , ★ ⊢ ★}
    → N ⇛ N′
      ----------
    → ƛ N ⇛ ƛ N′

  papp : ∀{Γ}{L L′ M M′ : Γ ⊢ ★}
    → L ⇛ L′
    → M ⇛ M′
      -----------------
    → L · M ⇛ L′ · M′

  pbeta : ∀{Γ}{N N′  : Γ , ★ ⊢ ★}{M M′ : Γ ⊢ ★}
    → N ⇛ N′
    → M ⇛ M′
      -----------------------
    → (ƛ N) · M  ⇛  N′ [ M′ ]

前三种规则是同时归约每个部分的合同性。 最后一个规则平行地归约一个 λ-项和另一个项，接着是一步 β-归约。

我们注意到 pabs、papp 和 pbeta 规则同时对它们的所有子表达式执行归约。 此外，pabs 规则类似于 ζ 规则，pbeta 类似于 β 规则。

平行归约是自反的。

par-refl : ∀{Γ A}{M : Γ ⊢ A} → M ⇛ M
par-refl {Γ} {A} {` x} = pvar
par-refl {Γ} {★} {ƛ N} = pabs par-refl
par-refl {Γ} {★} {L · M} = papp par-refl par-refl

我们定义平行归约序列如下。

infix  2 _⇛*_
infixr 2 _⇛⟨_⟩_
infix  3 _∎

data _⇛*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
      --------
    → M ⇛* M

  _⇛⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
    → L ⇛ M
    → M ⇛* N
      ---------
    → L ⇛* N

练习 par-diamond-eg（实践）

回顾上文中菱形性质的反例，证明在这种情况下平行归约具有菱形性质。

-- 请将代码写在此处

平行归约与归约间等价性

此处我们证明对于任何 M 和 N，M ⇛* N 当且仅当 M —↠ N。 必要性的证明非常容易，我们开始于说明若 M —→ N，则 M ⇛ N。 该证明通过对归约 M —→ N 进行归纳。

beta-par : ∀{Γ A}{M N : Γ ⊢ A}
  → M —→ N
    ------
  → M ⇛ N
beta-par {Γ} {★} {L · M} (ξ₁ r) = papp (beta-par {M = L} r) par-refl
beta-par {Γ} {★} {L · M} (ξ₂ r) = papp par-refl (beta-par {M = M} r)
beta-par {Γ} {★} {(ƛ N) · M} β = pbeta par-refl par-refl
beta-par {Γ} {★} {ƛ N} (ζ r) = pabs (beta-par r)

证明了该引理后我们便可完成必要性的证明， 即 M —↠ N 蕴含 M ⇛* N。该证明是对 M —↠ N 归约序列的简单归纳。

betas-pars : ∀{Γ A} {M N : Γ ⊢ A}
  → M —↠ N
    ------
  → M ⇛* N
betas-pars {Γ} {A} {M₁} {.M₁} (M₁ ∎) = M₁ ∎
betas-pars {Γ} {A} {.L} {N} (L —→⟨ b ⟩ bs) =
   L ⇛⟨ beta-par b ⟩ betas-pars bs

现在考虑命题的充分性，即 M ⇛* N 蕴含 M —↠ N。 充分性的证明有一点不同，因为它不是 M ⇛ N 蕴含 M —→ N 的情形。 毕竟 M ⇛ N 执行了许多归约， 所以我们应当证明 M ⇛ N 蕴含 M —↠ N。

par-betas : ∀{Γ A}{M N : Γ ⊢ A}
  → M ⇛ N
    ------
  → M —↠ N
par-betas {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) ∎
par-betas {Γ} {★} {ƛ N} (pabs p) = abs-cong (par-betas p)
par-betas {Γ} {★} {L · M} (papp {L = L}{L′}{M}{M′} p₁ p₂) =
    begin
    L · M   —↠⟨ appL-cong{M = M} (par-betas p₁) ⟩
    L′ · M  —↠⟨ appR-cong (par-betas p₂) ⟩
    L′ · M′
    ∎
par-betas {Γ} {★} {(ƛ N) · M} (pbeta{N′ = N′}{M′ = M′} p₁ p₂) =
    begin
    (ƛ N) · M                    —↠⟨ appL-cong{M = M} (abs-cong (par-betas p₁)) ⟩
    (ƛ N′) · M                   —↠⟨ appR-cong{L = ƛ N′} (par-betas p₂)  ⟩
    (ƛ N′) · M′                  —→⟨ β ⟩
     N′ [ M′ ]
    ∎

该证明通过对 M ⇛ N 进行归纳。

  • 假定 x ⇛ x。我们立刻有 x —↠ x。

  • 假定 ƛ N ⇛ ƛ N′ 因为 N ⇛ N′。根据归纳假设我们有 N —↠ N′。 我们得出 ƛ N —↠ ƛ N′ 因为 —↠ 具有合同性。

  • 假定 L · M ⇛ L′ · M′ 因为 L ⇛ L′ 和 M ⇛ M′。 根据归纳假设，我们有 L —↠ L′ 和 M —↠ M′。 所以有 L · M —↠ L′ · M 以及 L′ · M —↠ L′ · M′ 因为 —↠ 具有合同性。

  • 假定 (ƛ N) · M ⇛ N′ [ M′ ] 因为 N ⇛ N′ 和 M ⇛ M′。 根据类似的原因，我们有 (ƛ N) · M —↠ (ƛ N′) · M′， 接着应用 β-归约我们得到 (ƛ N′) · M′ —→ N′ [ M′ ]。

证明了该引理后我们便可通过对 M ⇛* N 的一步简单归纳完成 M ⇛* N 蕴含 M —↠ N 的证明。

pars-betas : ∀{Γ A} {M N : Γ ⊢ A}
  → M ⇛* N
    ------
  → M —↠ N
pars-betas (M₁ ∎) = M₁ ∎
pars-betas (L ⇛⟨ p ⟩ ps) = —↠-trans (par-betas p) (pars-betas ps)

平行归约的替换引理

我们的下一个目标是对平行归约证明菱形性质。 为了完成该证明，我们还需证明替换遵从平行归约。 也就是说，如果有 N ⇛ N′ 和 M ⇛ M′，那么 N [ M ] ⇛ N′ [ M′ ]。 我们不能直接通过归纳证明它，所以我们将其推广为： 如果 N ⇛ N′ 并且替换 σ 逐点（Pointwise）平行归约至 τ， 则 subst σ N ⇛ subst τ N′。 我们将代换的逐点平行归约定义如下：

par-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
par-subst {Γ}{Δ} σ σ′ = ∀{A}{x : Γ ∋ A} → σ x ⇛ σ′ x

In the type of par-subst we make use of the shorthand Subst Γ Δ for the type of a substitution. Similarly, we shall make use of Rename Γ Δ for the type of a renaming. Both are defined in Chapter Substitution and have the following meaning.

_ : ∀(Γ Δ : Context) → Set₁
_ = λ Γ Δ →   Rename Γ Δ ≡ ∀{A} → Γ ∋ A → Δ ∋ A

_ : ∀(Γ Δ : Context) → Set₁
_ = λ Γ Δ →   Subst Γ Δ ≡ ∀{A} → Γ ∋ A → Δ ⊢ A

因为替换依赖于扩展函数 exts，而其又依赖于 rename， 我们开始于被称为 par-rename 的替换引理的一种版本，该引理专门用于重命名。 par-rename 依赖于重命名和替换可以相互交换的事实， 这是一个我们在 Substitution 章节引入并在此处重申的引理。

rename-subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{ρ : Rename Γ Δ }
    → (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ])
rename-subst-commute {N = N} = plfa.part2.Substitution.rename-subst-commute {N = N}

现在证明 par-rename 引理。

par-rename : ∀{Γ Δ A} {ρ : Rename Γ Δ} {M M′ : Γ ⊢ A}
  → M ⇛ M′
    ------------------------
  → rename ρ M ⇛ rename ρ M′
par-rename pvar = pvar
par-rename (pabs p) = pabs (par-rename p)
par-rename (papp p₁ p₂) = papp (par-rename p₁) (par-rename p₂)
par-rename {Γ}{Δ}{A}{ρ} (pbeta{Γ}{N}{N′}{M}{M′} p₁ p₂)
    with pbeta (par-rename{ρ = ext ρ} p₁) (par-rename{ρ = ρ} p₂)
... | G rewrite rename-subst-commute{Γ}{Δ}{N′}{M′}{ρ} = G

证明通过对 M ⇛ M′ 进行归纳来完成。前三种情况很简单， 所以我们只考虑最后一种，即 pbeta。

  • 假定 (ƛ N) · M ⇛ N′ [ M′ ] 因为 N ⇛ N′ 和 M ⇛ M′。 根据归纳假设，我们有 rename (ext ρ) N ⇛ rename (ext ρ) N′ 和 rename ρ M ⇛ rename ρ M′。 所以根据 pbeta 我们有 (ƛ rename (ext ρ) N) · (rename ρ M) ⇛ (rename (ext ρ) N) [ rename ρ M ]。 然而，为了得出结论我们需要平行归约至 rename ρ (N [ M ])。 值得庆幸的是，重命名和归约可以相互交换。

有了 par-rename 引理，很容易证明扩展替换保留了逐点平行归约关系。

par-subst-exts : ∀{Γ Δ} {σ τ : Subst Γ Δ}
  → par-subst σ τ
    ------------------------------------------
  → ∀{B} → par-subst (exts σ {B = B}) (exts τ)
par-subst-exts s {x = Z} = pvar
par-subst-exts s {x = S x} = par-rename s

为了证明替换遵从平行归约关系，我们需要证明的下一个引理如下文所示， 它声称同时归约可以与单步归约相交换。 我们从 Substitution 章节导入这个引理， 并重申如下。

subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ }
  → subst (exts σ) N [ subst σ M ] ≡ subst σ (N [ M ])
subst-commute {N = N} = plfa.part2.Substitution.subst-commute {N = N}

我们准备好去证明替换遵从平行归约。

subst-par : ∀{Γ Δ A} {σ τ : Subst Γ Δ} {M M′ : Γ ⊢ A}
  → par-subst σ τ  →  M ⇛ M′
    --------------------------
  → subst σ M ⇛ subst τ M′
subst-par {Γ} {Δ} {A} {σ} {τ} {` x} s pvar = s
subst-par {Γ} {Δ} {A} {σ} {τ} {ƛ N} s (pabs p) =
  pabs (subst-par {σ = exts σ} {τ = exts τ}
        (λ {A}{x} → par-subst-exts s {x = x}) p)
subst-par {Γ} {Δ} {★} {σ} {τ} {L · M} s (papp p₁ p₂) =
  papp (subst-par s p₁) (subst-par s p₂)
subst-par {Γ} {Δ} {★} {σ} {τ} {(ƛ N) · M} s (pbeta{N′ = N′}{M′ = M′} p₁ p₂)
    with pbeta (subst-par{σ = exts σ}{τ = exts τ}{M = N}
                        (λ{A}{x} → par-subst-exts s {x = x}) p₁)
               (subst-par {σ = σ} s p₂)
... | G rewrite subst-commute{N = N′}{M = M′}{σ = τ} = G

我们通过对 M ⇛ M′ 归纳来证明。

  • 假定 x ⇛ x。我们使用前提 par-subst σ τ 来得出 σ x ⇛ τ x。

  • 假定 ƛ N ⇛ ƛ N′ 因为 N ⇛ N′。 为了使用归纳假设，我们需要 par-subst (exts σ) (exts τ)， 它通过 par-subst-exts 得出。 所以我们有 subst (exts σ) N ⇛ subst (exts τ) N′ 并且通过规则 pabs 来完成证明。

  • 假定 L · M ⇛ L′ · M′ 因为 L ⇛ L′ 和 M ⇛ M′。 根据归纳假设我们有 subst σ L ⇛ subst τ L′ 和 subst σ M ⇛ subst τ M′， 所以我们通过规则 papp 来完成证明。

  • 假定 (ƛ N) · M ⇛ N′ [ M′ ] 因为 N ⇛ N′ 和 M ⇛ M′。 同样我们根据 par-subst-exts 来得到 par-subst (exts σ) (exts τ)。 所以根据归纳假设，我们有 subst (exts σ) N ⇛ subst (exts τ) N′ 和 subst σ M ⇛ subst τ M′。 接着根据 pbeta 规则，我们平行归约至 subst (exts τ) N′ [ subst τ M′ ]。 替换在以下意义中与自身交换： 对于任意 σ、 N 和 M， 我们有

      (subst (exts σ) N) [ subst σ M ] ≡ subst σ (N [ M ])

    所以我们平行归约得到 subst τ (N′ [ M′ ])。

显然，若 M ⇛ M′，则 subst-zero M 逐点平行归约至 subst-zero M′。

par-subst-zero : ∀{Γ}{A}{M M′ : Γ ⊢ A}
       → M ⇛ M′
       → par-subst (subst-zero M) (subst-zero M′)
par-subst-zero {M} {M′} p {A} {Z} = p
par-subst-zero {M} {M′} p {A} {S x} = pvar

我们以所期望的推论来结束本节，即替换遵从平行归约。

sub-par : ∀{Γ A B} {N N′ : Γ , A ⊢ B} {M M′ : Γ ⊢ A}
  → N ⇛ N′
  → M ⇛ M′
    --------------------------
  → N [ M ] ⇛ N′ [ M′ ]
sub-par pn pm = subst-par (par-subst-zero pm) pn

平行归约满足菱形性质

合流性证明的核心是石头制成的，更确切地说，是钻石！ 【译注：在英文中 diamond 一词既指钻石，又指菱形。】 我们将证明平行归约满足菱形性质，即若有 M ⇛ N 和 M ⇛ N′， 那么对某个 L 有 N ⇛ L 和 N′ ⇛ L。 典型的证明通过对 M ⇛ N 和 M ⇛ N′ 归纳来完成， 因此每一个可能的对都会在执行足够多次平行 β-归约后产生一个证明 L。

其中向下的线是 ⇛ 的实例。因此我们称其为三角性质（Triangle Property）。

_⁺ : ∀ {Γ A}
  → Γ ⊢ A → Γ ⊢ A
(` x) ⁺       =  ` x
(ƛ M) ⁺       = ƛ (M ⁺)
((ƛ N) · M) ⁺ = N ⁺ [ M ⁺ ]
(L · M) ⁺     = L ⁺ · (M ⁺)

par-triangle : ∀ {Γ A} {M N : Γ ⊢ A}
  → M ⇛ N
    -------
  → N ⇛ M ⁺
par-triangle pvar          = pvar
par-triangle (pabs p)      = pabs (par-triangle p)
par-triangle (pbeta p1 p2) = sub-par (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = ƛ _ } (pabs p1) p2) =
  pbeta (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = ` _}   p1 p2) = papp (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = _ · _} p1 p2) = papp (par-triangle p1) (par-triangle p2)

三角性质的证明通过对 M ⇛ N 归纳来完成。

  • 假定 x ⇛ x。显然 x ⁺ = x，所以 x ⇛ x ⁺。

  • 假定 ƛ M ⇛ ƛ N。根据归纳假设我们有 N ⇛ M ⁺， 并且根据定义我们有 (λ M) ⁺ = λ (M ⁺)，所以我们得出 λ N ⇛ λ(M ⁺)。

  • 假定 (λ N) · M ⇛ N′ [ M′ ]。根据归纳假设我们有 N′ ⇛ N ⁺ 和 M′ ⇛ M ⁺。 因为替换遵从平行归约，于是得到 N′ [ M′ ] ⇛ N ⁺ [ M ⁺ ]， 而右侧即为 ((λ N) · M) ⁺，因此有 N′ [ M′ ] ⇛ ((λ N) · M) ⁺。

  • 假定 (λ L) · M ⇛ (λ L′) · M′。 根据归纳假设我们有 L′ ⇛ L ⁺ 和 M′ ⇛ M ⁺； 根据定义有 ((λ L) · M) ⁺ = L ⁺ [ M ⁺ ]。 接着得出 (λ L′) · M′ ⇛ L ⁺ [ M ⁺ ]。

  • 假定 x · M ⇛ x · M′。 根据归纳假设我们有 M′ ⇛ M ⁺ 和 x ⇛ x ⁺，因此 x · M′ ⇛ x · M ⁺。 剩余的情况可以以相同方式证明，所以我们忽略它。 （由于 Agda 目前没有办法在检查右侧之前为我们扩展 _⁺ 定义中的 catch-all 模式，我们必须明确地写下剩余的情况。）

菱形性质接着通过将菱形折半成两个三角形得出。

    M
   /|\
  / | \
 /  |  \
N   2   N′
 \  |  /
  \ | /
   \|/
    M⁺

也就是说，菱形性质通过在两侧应用具有相同合流项 M ⁺的三角性质而证明。

par-diamond : ∀{Γ A} {M N N′ : Γ ⊢ A}
  → M ⇛ N
  → M ⇛ N′
    ---------------------------------
  → Σ[ L ∈ Γ ⊢ A ] (N ⇛ L) × (N′ ⇛ L)
par-diamond {M = M} p1 p2 = ⟨ M ⁺ , ⟨ par-triangle p1 , par-triangle p2 ⟩ ⟩

不过，在存在三角性质的情况下，该步骤是可选的。

练习（实践）

  • 通过对 M ⇛ N 和 M ⇛ N′ 归纳直接证明菱形性质 par-diamond。

  • 作图表示 par-diamond 的直接证明中的六种情况。 图应当包含节点和有向边，其中节点用项标记，边代表平行归约。

平行归约合流性的证明

像在开始承诺的那样，平行归约合流性的证明现在十分简单， 因为我们知道它满足三角性质。 我们只需证明带状引理（Strip Lemma），它声称若有 M ⇛ N 和 M ⇛* N′， 则对于某个 L 有 N ⇛* L 和 N′ ⇛ L。 下图解释了带状引理：

    M
   / \
  1   *
 /     \
N       N′
 \     /
  *   1
   \ /
    L

此处向下的线是 ⇛ 或 ⇛* 的实例，取决于它们如何被标记。

带状引理的证明是对 M ⇛* N′ 的简单归纳，并在归纳步骤使用三角性质。

strip : ∀{Γ A} {M N N′ : Γ ⊢ A}
  → M ⇛ N
  → M ⇛* N′
    ------------------------------------
  → Σ[ L ∈ Γ ⊢ A ] (N ⇛* L)  ×  (N′ ⇛ L)
strip{Γ}{A}{M}{N}{N′} mn (M ∎) = ⟨ N , ⟨ N ∎ , mn ⟩ ⟩
strip{Γ}{A}{M}{N}{N′} mn (M ⇛⟨ mm' ⟩ m'n')
  with strip (par-triangle mm') m'n'
... | ⟨ L , ⟨ ll' , n'l' ⟩ ⟩ = ⟨ L , ⟨ N ⇛⟨ par-triangle mn ⟩ ll' , n'l' ⟩ ⟩

平行归约合流性的证明现在通过对序列 M ⇛* N 归纳来完成，并在归纳步骤使用上述引理。

par-confluence : ∀{Γ A} {L M₁ M₂ : Γ ⊢ A}
  → L ⇛* M₁
  → L ⇛* M₂
    ------------------------------------
  → Σ[ N ∈ Γ ⊢ A ] (M₁ ⇛* N) × (M₂ ⇛* N)
par-confluence {Γ}{A}{L}{.L}{N} (L ∎) L⇛*N = ⟨ N , ⟨ L⇛*N , N ∎ ⟩ ⟩
par-confluence {Γ}{A}{L}{M₁′}{M₂} (L ⇛⟨ L⇛M₁ ⟩ M₁⇛*M₁′) L⇛*M₂
    with strip L⇛M₁ L⇛*M₂
... | ⟨ N , ⟨ M₁⇛*N , M₂⇛N ⟩ ⟩
      with par-confluence M₁⇛*M₁′ M₁⇛*N
...   | ⟨ N′ , ⟨ M₁′⇛*N′ , N⇛*N′ ⟩ ⟩ =
        ⟨ N′ , ⟨ M₁′⇛*N′ , (M₂ ⇛⟨ M₂⇛N ⟩ N⇛*N′) ⟩ ⟩

归纳步骤可以如下图解释：

        L
       / \
      1   *
     /     \
    M₁ (a)  M₂
   / \     /
  *   *   1
 /     \ /
M₁′(b)  N
 \     /
  *   *
   \ /
    N′

此处向下的线是 ⇛ 或 ⇛* 的实例，取决于它们如何被标记。 此处 (a) 根据 strip 而成立，(b) 根据归纳假设而成立。

归约合流性的证明

归约的合流性是平行归约合流性的一个推论。 从 L —↠ M₁ 和 L —↠ M₂ 根据 betas-pars 我们有 L ⇛* M₁ 和 L ⇛* M₂。 接着根据合流性我们得到对于某个 L 有 M₁ ⇛* N 和 M₂ ⇛* N。 因此我们根据 pars-betas 得出 M₁ —↠ N 和 M₂ —↠ N。

confluence : ∀{Γ A} {L M₁ M₂ : Γ ⊢ A}
  → L —↠ M₁
  → L —↠ M₂
    -----------------------------------
  → Σ[ N ∈ Γ ⊢ A ] (M₁ —↠ N) × (M₂ —↠ N)
confluence L↠M₁ L↠M₂
    with par-confluence (betas-pars L↠M₁) (betas-pars L↠M₂)
... | ⟨ N , ⟨ M₁⇛N , M₂⇛N ⟩ ⟩ =
      ⟨ N , ⟨ pars-betas M₁⇛N , pars-betas M₂⇛N ⟩ ⟩

注记

总而言之，这种机械化的合流性证明基于几个来源。 subst-par 引理是 Schäfer, Tebbi, and Smolka (2015) 的「强替换性（Strong Substitutivity）」 引理。 par-triangle、strip 和 par-confluence 的证明基于 Takahashi (1995) 完全发展的概念，以及 Pfenning (1992) 关于 Church-Rosser 定理的技术报告。 此外，我们询问了 Nipkow 和 Berghofer 在 Isabelle 中的机械化， 它基于 Nipkow (1996) 的早期论文。

Unicode

本章中使用了以下 Unicode：

⇛  U+21DB  RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
⁺  U+207A  SUPERSCRIPT PLUS SIGN   (\^+)
Nipkow, Tobias. 1996. “More Church-Rosser Proofs (in Isabelle/HOL).” In Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, 733–47. CADE-13. Berlin, Heidelberg: Springer-Verlag.
Pfenning, Frank. 1992. “A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework.” CMU-CS-92-186. Carnegie Mellon University; Carnegie Mellon University.
Schäfer, Steven, Tobias Tebbi, and Gert Smolka. 2015. “Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions.” In Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6, 359–74. Springer.
Takahashi, M. 1995. “Parallel Reductions in λ-Calculus.” Information and Computation 118 (1): 120–27. https://doi.org/https://doi.org/10.1006/inco.1995.1057.