michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

updated Confluence

Browse source
This commit is contained in:
wadler 2019-05-08 16:39:06 -03:00
parent 6fc3e4a920
commit 84aa286783
1 changed files with 187 additions and 144 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

331
extra/extra/Confluence.lagda
View file

@ -9,11 +9,10 @@ open import extra.Substitution
open import extra.LambdaReduction
open import plfa.Denotational using (Rename)
open import plfa.Soundness using (Subst)
open import plfa.Untyped
renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to commence_; _∎ to _fini)
open import plfa.Untyped hiding (_—→_; _—↠_; begin_; _∎)
-- renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to commence_; _∎ to _fini)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Function using (_∘_)
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
renaming (_,_ to ⟨_,_⟩)
@ -22,20 +21,37 @@ open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; p
## Introduction
In this chapter we prove that beta reduction is _confluent_. That is,
if there is a reduction sequence from any term `M` to two different
terms `N` and `N'`, then there exist reduction sequences from those
two terms to some common term `L`.
if there is a reduction sequence from any term `L` to two different
terms `M₁` and `M₂`, then there exist reduction sequences from those
two terms to some common term `N`. In pictures:
L
/ \
/ \
/ \
M₁ M₂
\ /
\ /
\ /
N
where downward lines are instances of `—↠`.
Confluence is studied in many other kinds of rewrite systems besides
the lambda calculus, and it is well known how to prove confluence in
rewrite systems that enjoy the _diamond property_, a single-step
version of confluence. Let `⇒` be a relation. Then `⇒` has the
diamond property if `M ⇒ N` and `M ⇒ N'`, then there exists an `L`
such that `N ⇒ L` and `N' ⇒ L`. Let `⇒*` stand for sequences of `⇒`
reductions. The proof of confluence requires one easy lemma, that if
`M ⇒ N` and `M ⇒* N'`, then there exists an `L` such that `N ⇒* L` and
`N' ⇒ L. With this lemma in hand, confluence is proved by induction
on the reduction sequence `M ⇒* N`.
version of confluence. Let `⇛` be a relation. Then `⇛` has the
diamond property if whenever `L ⇛ M₁` and `L ⇛ M₂`, then there exists
an `N` such that `M₁ ⇛ N` and `M₂ ⇛ N`. This is just an instance of
the same picture above, where downward lines are now instance of `⇛`.
If we write `⇛*` for the reflexive and transitive closure of `⇛`, then
confluence of `⇛*` follows immediately from the diamon property.
<!-- Let `⇛*` stand for sequences of `⇛` reductions.
The proof of confluence requires one easy lemma, that if
`M ⇛ N` and `M ⇛* N'`, then there exists an `L` such that `N ⇛* L` and
`N' ⇛ L. With this lemma in hand, confluence is proved by induction
on the reduction sequence `M ⇛* N`. -->
Unfortunately, reduction in the lambda calculus does not satisfy the
diamond property. Here is a counter example.
@ -60,29 +76,34 @@ corollary to confluence for parallel reduction.
The parallel reduction relation is defined as follows.
\begin{code}
infix 2 _⇒_
infix 2 _⇛_
data _⇒_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
data _⇛_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
pvar : ∀{Γ A}{x : Γ ∋ A}
---------
→ (` x) ⇒ (` x)
→ (` x) ⇛ (` x)
pabs : ∀{Γ}{N N' : Γ , ★ ⊢ ★}
→ N ⇒ N'
→ N ⇛ N'
----------
→ ƛ N ⇒ ƛ N'
→ ƛ N ⇛ ƛ N'
papp : ∀{Γ}{L L' M M' : Γ ⊢ ★}
→ L ⇒ L' → M ⇒ M'
→ L ⇛ L'
→ M ⇛ M'
-----------------
→ L · M ⇒ L' · M'
→ L · M ⇛ L' · M'
pbeta : ∀{Γ}{N N' : Γ , ★ ⊢ ★}{M M' : Γ ⊢ ★}
→ N ⇒ N' → M ⇒ M'
→ N ⇛ N'
→ M ⇛ M'
-----------------------
→ (ƛ N) · M ⇒ N' [ M' ]
→ (ƛ N) · M ⇛ N' [ M' ]
\end{code}
The first three rules are congruences that reduce each of their
parts simultaneously. The last rule reduces a lambda term and
term in parallel followed by a beta step.
We remark that the `pabs`, `papp`, and `pbeta` rules perform reduction
on all their subexpressions simultaneously. Also, the `pabs` rule is
@ -91,51 +112,43 @@ akin to the `ζ` rule and `pbeta` is akin to `β`.
Parallel reduction is reflexive.
\begin{code}
par-refl : ∀{Γ A}{M : Γ ⊢ A} → M ⇒ M
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
\end{code}
We define the sequences of parallel reduction as follows.
\begin{code}
infix 2 _⇒*_
infix 1 init_
infixr 2 _⇒⟨_⟩_
infix 3 _□
infix 2 _⇛*_
infixr 2 _⇛⟨_⟩_
infix 3 _∎
data _⇒*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
data _⇛*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
_□ : ∀ {Γ A} (M : Γ ⊢ A)
_∎ : ∀ {Γ A} (M : Γ ⊢ A)
--------
→ M ⇒* M
→ M ⇛* M
_⇒⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L ⇒ M
→ M ⇒* N
_⇛⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L ⇛ M
→ M ⇛* N
---------
→ L ⇒* N
init_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
→ M ⇒* N
------
→ M ⇒* N
init M⇒*N = M⇒*N
→ L ⇛* N
\end{code}
## Equivalence between parallel reduction and reduction
Here we prove that for any `M` and `N`, `M ⇒* N` if and only if `M —↠ N`.
Here we prove that for any `M` and `N`, `M ⇛* N` if and only if `M —↠ N`.
The only-if direction is particularly easy. We start by showing
that if `M —→ N`, then `M ⇒ N`. The proof is by induction on
that if `M —→ N`, then `M ⇛ N`. The proof is by induction on
the reduction `M —→ N`.
\begin{code}
beta-par : ∀{Γ A}{M N : Γ ⊢ A}
→ M —→ N
------
→ 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
@ -143,27 +156,27 @@ beta-par {Γ} {★} {ƛ N} (ζ r) = pabs (beta-par r)
\end{code}
With this lemma in hand we complete the only-if direction,
that `M —↠ N` implies `M ⇒* N`. The proof is a straightforward
that `M —↠ N` implies `M ⇛* N`. The proof is a straightforward
induction on the reduction sequence `M —↠ N`.
\begin{code}
betas-pars : ∀{Γ A} {M N : Γ ⊢ A}
→ M —↠ N
------
→ M ⇒* N
betas-pars {Γ} {A} {M₁} {.M₁} (M₁ []) = M₁ □
→ M ⇛* N
betas-pars {Γ} {A} {M₁} {.M₁} (M₁ []) = M₁ ∎
betas-pars {Γ} {A} {.L} {N} (L —→⟨ b ⟩ bs) =
L ⇒⟨ beta-par b ⟩ betas-pars bs
L ⇛⟨ beta-par b ⟩ betas-pars bs
\end{code}
Now for the other direction, that `M ⇒* N` implies `M —↠ N`. The
Now for the other direction, that `M ⇛* N` implies `M —↠ N`. The
proof of this direction is a bit different because it's not the case
that `M ⇒ N` implies `M —→ N`. After all, `M ⇒ N` performs many
reductions. So instead we shall prove that `M ⇒ N` implies `M —↠ N`.
that `M ⇛ N` implies `M —→ N`. After all, `M ⇛ N` performs many
reductions. So instead we shall prove that `M ⇛ N` implies `M —↠ N`.
\begin{code}
par-betas : ∀{Γ A}{M N : Γ ⊢ A}
→ M ⇒ N
→ M ⇛ N
------
→ M —↠ N
par-betas {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) []
@ -181,36 +194,36 @@ par-betas {Γ} {★} {(ƛ N) · M} (pbeta{N' = N'}{M' = M'} p₁ p₂) =
—↠-trans (—↠-trans a b) c
\end{code}
The proof is by induction on `M ⇒ N`.
The proof is by induction on `M ⇛ N`.
* Suppose `x ⇒ x`. We immediately have `x —↠ x`.
* Suppose `x ⇛ x`. We immediately have `x —↠ x`.
* Suppose `ƛ N ⇒ ƛ N'` because `N ⇒ N'`. By the induction hypothesis
* Suppose `ƛ N ⇛ ƛ N'` because `N ⇛ N'`. By the induction hypothesis
we have `N —↠ N'`. We conclude that `ƛ N —↠ ƛ N'` because
`—↠` is a congruence.
* Suppose `L · M ⇒ L' · M'` because `L ⇒ L'` and `M ⇒ M'`.
* Suppose `L · M ⇛ L' · M'` because `L ⇛ L'` and `M ⇛ M'`.
By the induction hypothesis, we have `L —↠ L'` and `M —↠ M'`.
So `L · M —↠ L' · M` and then `L' · M —↠ L' · M'`
because `—↠` is a congruence. We conclude using the transitity
of `—↠`.
* Suppose `(ƛ N) · M ⇒ N' [ M' ]` because `N ⇒ N'` and `M ⇒ M'`.
* Suppose `(ƛ N) · M ⇛ N' [ M' ]` because `N ⇛ N'` and `M ⇛ M'`.
By similar reasoning, we have
`(ƛ N) · M —↠ (ƛ N') · M'`.
Of course, `(ƛ N') · M' —→ N' [ M' ]`, so we can conclude
using the transitivity of `—↠`.
With this lemma in handle, we complete the proof that `M ⇒* N` implies
`M —↠ N` with a simple induction on `M ⇒* N`.
With this lemma in handle, we complete the proof that `M ⇛* N` implies
`M —↠ N` with a simple induction on `M ⇛* N`.
\begin{code}
pars-betas : ∀{Γ A} {M N : Γ ⊢ A}
→ M ⇒* N
→ M ⇛* N
------
→ M —↠ N
pars-betas (M₁ □) = M₁ []
pars-betas (L ⇒⟨ p ⟩ ps) = —↠-trans (par-betas p) (pars-betas ps)
pars-betas (M₁ ∎) = M₁ []
pars-betas (L ⇛⟨ p ⟩ ps) = —↠-trans (par-betas p) (pars-betas ps)
\end{code}
@ -219,16 +232,16 @@ pars-betas (L ⇒⟨ p ⟩ ps) = —↠-trans (par-betas p) (pars-betas ps)
Our next goal is the prove the diamond property for parallel
reduction. But to do that, we need to prove that substitution
respects parallel reduction. That is, if
`N ⇒ N'` and `M ⇒ M'`, then `N [ M ] ⇒ N' [ M' ]`.
`N ⇛ N'` and `M ⇛ M'`, then `N [ M ] ⇛ N' [ M' ]`.
We cannot prove this directly by induction, so we
generalize it to: if `N ⇒ N'` and
generalize it to: if `N ⇛ N'` and
the substitution `σ` pointwise parallel reduces to `τ`,
then `subst σ N ⇒ subst τ N'`. We define the notion
then `subst σ N ⇛ subst τ N'`. We define the notion
of pointwise parallel reduction as follows.
\begin{code}
par-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
par-subst {Γ}{Δ} σ₁ σ₂ = ∀{A}{x : Γ ∋ A} → σ₁ x ⇒ σ₂ x
par-subst {Γ}{Δ} σ σ′ = ∀{A}{x : Γ ∋ A} → σ x ⇛ σ′ x
\end{code}
Because substitution depends on the extension function `exts`, which
@ -237,9 +250,9 @@ substitution lemma specialized to renamings.
\begin{code}
par-rename : ∀{Γ Δ A} {ρ : Rename Γ Δ} {M M' : Γ ⊢ A}
→ M ⇒ M'
→ M ⇛ M'
------------------------
→ rename ρ M ⇒ rename ρ 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₂)
@ -248,15 +261,15 @@ par-rename {Γ}{Δ}{A}{ρ} (pbeta{Γ}{N}{N'}{M}{M'} p₁ p₂)
... | G rewrite rename-subst-commute{Γ}{Δ}{N'}{M'}{ρ} = G
\end{code}
The proof is by induction on `M ⇒ M'`. The first four cases
The proof is by induction on `M ⇛ M'`. The first four cases
are straightforward so we just consider the last one for `pbeta`.
* Suppose `(ƛ N) · M ⇒ N' [ M' ]` because `N ⇒ N'` and `M ⇒ M'`.
* Suppose `(ƛ N) · M ⇛ N' [ M' ]` because `N ⇛ N'` and `M ⇛ M'`.
By the induction hypothesis, we have
`rename (ext ρ) N ⇒ rename (ext ρ) N'` and
`rename ρ M ⇒ rename ρ M'`.
`rename (ext ρ) N ⇛ rename (ext ρ) N'` and
`rename ρ M ⇛ rename ρ M'`.
So by `pbeta` we have
`(ƛ rename (ext ρ) N) · (rename ρ M) ⇒ (rename (ext ρ) N) [ rename ρ M ]`.
`(ƛ rename (ext ρ) N) · (rename ρ M) ⇛ (rename (ext ρ) N) [ rename ρ M ]`.
However, to conclude we instead need parallel reduction to
`rename ρ (N [ M ])`. But thankfully, renaming and substitution
commute with one another, that is,
@ -280,9 +293,9 @@ parallel reduction.
\begin{code}
subst-par : ∀{Γ Δ A} {σ τ : Subst Γ Δ} {M M' : Γ ⊢ A}
→ par-subst σ τ → M ⇒ M'
→ par-subst σ τ → M ⇛ M'
--------------------------
→ subst σ M ⇒ subst τ M'
→ subst σ M ⇛ subst τ M'
subst-par {Γ} {Δ} {A} {σ} {τ} {` x} s pvar = s
subst-par {Γ} {Δ} {★} {σ} {τ} {ƛ N} s (pabs p) =
pabs (subst-par {σ = exts σ} {τ = exts τ}
@ -291,33 +304,33 @@ 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 {A}{x}) p₁)
(subst-par (λ {A}{x} → s{A}{x}) p₂)
(λ{A}{x} → par-subst-exts s{A}{x}) p₁)
(subst-par (λ{A}{x} → s{A}{x}) p₂)
... | G rewrite subst-commute{N = N'}{M = M'}{σ = τ} =
G
\end{code}
We proceed by induction on `M ⇒ M'`.
We proceed by induction on `M ⇛ M'`.
* Suppose `x ⇒ x`. We conclude that `σ x ⇒ τ x` using
* Suppose `x ⇛ x`. We conclude that `σ x ⇛ τ x` using
the premise `par-subst σ τ`.
* Suppose `ƛ N ⇒ ƛ N'` because `N ⇒ N'`.
* Suppose `ƛ N ⇛ ƛ N'` because `N ⇛ N'`.
To use the induction hypothesis, we need `par-subst (exts σ) (exts τ)`,
which we obtain by `par-subst-exts`.
So then we have `subst (exts σ) N ⇒ subst (exts τ) N'`
So then we have `subst (exts σ) N ⇛ subst (exts τ) N'`
and conclude by rule `pabs`.
* Suppose `L · M ⇒ L' · M'` because `L ⇒ L'` and `M ⇒ M'`.
* Suppose `L · M ⇛ L' · M'` because `L ⇛ L'` and `M ⇛ M'`.
By the induction hypothesis we have
`subst σ L ⇒ subst τ L'` and `subst σ M ⇒ subst τ M'`, so
`subst σ L ⇛ subst τ L'` and `subst σ M ⇛ subst τ M'`, so
we conclude by rule `papp`.
* Suppose `(ƛ N) · M ⇒ N' [ M' ]` because `N ⇒ N'` and `M ⇒ M'`.
* Suppose `(ƛ N) · M ⇛ N' [ M' ]` because `N ⇛ N'` and `M ⇛ M'`.
Again we obtain `par-subst (exts σ) (exts τ)` by `par-subst-exts`.
So by the induction hypothesis, we have
`subst (exts σ) N ⇒ subst (exts τ) N'` and
`subst σ M ⇒ subst τ M'`. So by rule `pbeta`, we have parallel reduction
`subst (exts σ) N ⇛ subst (exts τ) N'` and
`subst σ M ⇛ subst τ M'`. So by rule `pbeta`, we have parallel reduction
to `subst (exts τ) N' [ subst τ M' ]`.
Substitution commutes with itself in the following sense.
For any σ, N, and M, we have
@ -327,12 +340,12 @@ We proceed by induction on `M ⇒ M'`.
So we have parallel reduction to `subst τ (N' [ M' ])`.
Of course, if `M ⇒ M'`, then `subst-zero M` pointwise parallel reduces
Of course, if `M ⇛ M'`, then `subst-zero M` pointwise parallel reduces
to `subst-zero M'`.
\begin{code}
par-subst-zero : ∀{Γ}{A}{M M' : Γ ⊢ A}
→ M ⇒ M'
→ 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
@ -343,9 +356,10 @@ respects parallel reduction.
\begin{code}
sub-par : ∀{Γ A B} {N N' : Γ , A ⊢ B} {M M' : Γ ⊢ A}
→ N ⇒ N' → M ⇒ M'
→ N ⇛ N'
→ M ⇛ M'
--------------------------
→ N [ M ] ⇒ N' [ M' ]
→ N [ M ] ⇛ N' [ M' ]
sub-par pn pm = subst-par (par-subst-zero pm) pn
\end{code}
@ -354,13 +368,15 @@ sub-par pn pm = subst-par (par-subst-zero pm) pn
The heart of this proof is made of stone, or rather, of diamond! We
show that parallel reduction satisfies the diamond property: that if
`M ⇒ N` and `M ⇒ N'`, then `N ⇒ L` and `N' ⇒ L` for some `L`. The
proof is relatively easy; it is parallel reduction's raison d'etre.
`M ⇛ N` and `M ⇛ N'`, then `N ⇛ L` and `N' ⇛ L` for some `L`. The
proof is relatively easy; it is parallel reduction's _raison d'etre_.
\begin{code}
par-diamond : ∀{Γ A} {M N N' : Γ ⊢ A}
→ M ⇒ N → M ⇒ N'
→ Σ[ L ∈ Γ ⊢ A ] (N ⇒ L) × (N' ⇒ L)
→ M ⇛ N
→ M ⇛ N'
---------------------------------
→ Σ[ L ∈ Γ ⊢ A ] (N ⇛ L) × (N' ⇛ L)
par-diamond (pvar{x = x}) pvar = ⟨ ` x , ⟨ pvar , pvar ⟩ ⟩
par-diamond (pabs p1) (pabs p2)
with par-diamond p1 p2
@ -395,42 +411,42 @@ par-diamond {Γ}{A} (pbeta p1 p3) (pbeta p2 p4)
The proof is by induction on both premises.
* Suppose `x ⇒ x` and `x ⇒ x`.
We choose `L = x` and immediately have `x ⇒ x` and `x ⇒ x`.
* Suppose `x ⇛ x` and `x ⇛ x`.
We choose `L = x` and immediately have `x ⇛ x` and `x ⇛ x`.
* Suppose `ƛ N ⇒ ƛ N'` and `ƛ N ⇒ ƛ N''`.
* Suppose `ƛ N ⇛ ƛ N'` and `ƛ N ⇛ ƛ N''`.
By the induction hypothesis, there exists `L'` such that
`N' ⇒ L'` and `N'' ⇒ L'`. We choose `L = ƛ L'` and
by `pabs` conclude that `ƛ N' ⇒ ƛ L'` and `ƛ N'' ⇒ ƛ L'.
`N' ⇛ L'` and `N'' ⇛ L'`. We choose `L = ƛ L'` and
by `pabs` conclude that `ƛ N' ⇛ ƛ L'` and `ƛ N'' ⇛ ƛ L'.
* Suppose that `L · M ⇒ L₁ · M₁` and `L · M ⇒ L₂ · M₂`.
* Suppose that `L · M ⇛ L₁ · M₁` and `L · M ⇛ L₂ · M₂`.
By the induction hypothesis we have
`L₁ ⇒ L₃` and `L₂ ⇒ L₃` for some `L₃`.
`L₁ ⇛ L₃` and `L₂ ⇛ L₃` for some `L₃`.
Likewise, we have
`M₁ ⇒ M₃` and `M₂ ⇒ M₃` for some `M₃`.
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = L₃ · M₃` and conclude with two uses of `papp`.
* Suppose that `(ƛ N) · M ⇒ (ƛ N₁) · M₁` and `(ƛ N) · M ⇒ N₂ [ M₂ ]`
* Suppose that `(ƛ N) · M ⇛ (ƛ N₁) · M₁` and `(ƛ N) · M ⇛ N₂ [ M₂ ]`
By the induction hypothesis we have
`N₁ ⇒ N₃` and `N₂ ⇒ N₃` for some `N₃`.
`N₁ ⇛ N₃` and `N₂ ⇛ N₃` for some `N₃`.
Likewise, we have
`M₁ ⇒ M₃` and `M₂ ⇒ M₃` for some `M₃`.
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = N₃ [ M₃ ]`.
We have `(ƛ N₁) · M₁ ⇒ N₃ [ M₃ ]` by rule `pbeta`
and conclude that `N₂ [ M₂ ] ⇒ N₃ [ M₃ ]` because
We have `(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]` by rule `pbeta`
and conclude that `N₂ [ M₂ ] ⇛ N₃ [ M₃ ]` because
substitution respects parallel reduction.
* Suppose that `(ƛ N) · M ⇒ N₁ [ M₁ ]` and `(ƛ N) · M ⇒ (ƛ N₂) · M₂`.
* Suppose that `(ƛ N) · M ⇛ N₁ [ M₁ ]` and `(ƛ N) · M ⇛ (ƛ N₂) · M₂`.
The proof of this case is the mirror image of the last one.
* Suppose that `(ƛ N) · M ⇒ N₁ [ M₁ ]` and `(ƛ N) · M ⇒ N₂ [ M₂ ]`.
* Suppose that `(ƛ N) · M ⇛ N₁ [ M₁ ]` and `(ƛ N) · M ⇛ N₂ [ M₂ ]`.
By the induction hypothesis we have
`N₁ ⇒ N₃` and `N₂ ⇒ N₃` for some `N₃`.
`N₁ ⇛ N₃` and `N₂ ⇛ N₃` for some `N₃`.
Likewise, we have
`M₁ ⇒ M₃` and `M₂ ⇒ M₃` for some `M₃`.
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = N₃ [ M₃ ]`.
We have both `(ƛ N₁) · M₁ ⇒ N₃ [ M₃ ]`
and `(ƛ N₂) · M₂ ⇒ N₃ [ M₃ ]`
We have both `(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]`
and `(ƛ N₂) · M₂ ⇛ N₃ [ M₃ ]`
by rule `pbeta`
@ -439,59 +455,86 @@ The proof is by induction on both premises.
As promised at the beginning, the proof that parallel reduction is
confluent is easy now that we know it satisfies the diamond property.
We just need one more lemma which states that
if `M ⇒ N` and `M ⇒* N'`, then
`N ⇒* L` and `N' ⇒ L` for some `L`.
The proof is a straightforward induction on `M ⇒* N'`,
if `M ⇛ N` and `M ⇛* N'`, then
`N ⇛* L` and `N' ⇛ L` for some `L`.
The proof is a straightforward induction on `M ⇛* N'`,
using the diamond property in the induction step.
\begin{code}
par-confR : ∀{Γ A} {M N N' : Γ ⊢ A}
→ M ⇒ N → M ⇒* N'
→ Σ[ L ∈ Γ ⊢ A ] (N ⇒* L) × (N' ⇒ L)
par-confR{Γ}{A}{M}{N}{N'} mn (M □) = ⟨ N , ⟨ N □ , mn ⟩ ⟩
par-confR{Γ}{A}{M}{N}{N'} mn (_⇒⟨_⟩_ M {M'} mm' mn')
par-confR : ∀{Γ A} {L M₁ M₂ : Γ ⊢ A}
→ L ⇛ M₁
→ L ⇛* M₂
-----------------------------------
→ Σ[ N ∈ Γ ⊢ A ] (M₁ ⇛* N) × (M₂ ⇛ N)
par-confR{Γ}{A}{M}{N}{N'} mn (M ∎) = ⟨ N , ⟨ N ∎ , mn ⟩ ⟩
par-confR{Γ}{A}{M}{N}{N'} mn (_⇛⟨_⟩_ M {M'} mm' mn')
with par-diamond mn mm'
... | ⟨ L , ⟨ nl , m'l ⟩ ⟩
with par-confR m'l mn'
... | ⟨ L' , ⟨ ll' , n'l' ⟩ ⟩ =
⟨ L' , ⟨ (N ⇒⟨ nl ⟩ ll') , n'l' ⟩ ⟩
⟨ L' , ⟨ (N ⇛⟨ nl ⟩ ll') , n'l' ⟩ ⟩
\end{code}
The proof of confluence for parallel reduction is now proved by
induction on the sequence `M ⇒* N`, using the above lemma in the
induction on the sequence `M ⇛* N`, using the above lemma in the
induction step.
\begin{code}
par-confluence : ∀{Γ A} {M N N' : Γ ⊢ A}
→ M ⇒* N → M ⇒* N'
→ Σ[ L ∈ Γ ⊢ A ] (N ⇒* L) × (N' ⇒* L)
par-confluence {Γ}{A}{M}{N}{N'} (M □) m→n' = ⟨ N' , ⟨ m→n' , N' □ ⟩ ⟩
par-confluence {Γ}{A}{M}{N}{N'} (_⇒⟨_⟩_ M {M'} m→m' m'→n) m→n'
with par-confR m→m' m→n'
... | ⟨ L , ⟨ m'→l , n'→l ⟩ ⟩
with par-confluence m'→n m'→l
... | ⟨ L' , ⟨ n→l' , l→l' ⟩ ⟩ =
⟨ L' , ⟨ n→l' , (N' ⇒⟨ n'→l ⟩ l→l') ⟩ ⟩
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 par-confR 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′) ⟩ ⟩
\end{code}
The step case may be illustrated as follows:
L
/ \
1 *
/ \
M₁ (a) M₂
/ \ /
* * 1
/ \ /
M₁′(b) N
\ /
* *
\ /
N′
where downward lines are instances of `⇛` or `⇛*`, depending on how
they are marked. Here `(a)` holds by `par-confR` and `(b)` holds by
induction.
## Proof of confluence for reduction
Confluence of reduction is a corollary of confluence for parallel
reduction. From
`M —↠ N` and `M —↠ N'` we have
`M ⇒* N` and `M ⇒* N'` by `betas-pars`.
`L —↠ M₁` and `L —↠ M₂` we have
`L ⇛* M₁` and `L ⇛* M₂` by `betas-pars`.
Then by confluence we obtain some `L` such that
`N ⇒* L` and `N' ⇒* L`, from which we conclude that
`N —↠ L` and `N' —↠ L` by `pars-betas`.
`M₁ ⇛* N` and `M₂ ⇛* N`, from which we conclude that
`M₁ —↠ N` and `M₂ —↠ N` by `pars-betas`.
\begin{code}
confluence : ∀{Γ A} {M N N' : Γ ⊢ A}
→ M —↠ N → M —↠ N'
→ Σ[ L ∈ Γ ⊢ A ] (N —↠ L) × (N' —↠ L)
confluence m→n m→n'
with par-confluence (betas-pars m→n) (betas-pars m→n')
... | ⟨ L , ⟨ n→l , n'→l ⟩ ⟩ =
⟨ L , ⟨ pars-betas n→l , pars-betas n'→l ⟩ ⟩
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 ⟩ ⟩
\end{code}