diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md index 51ee73809..b9c30b999 100644 --- a/src/1Lab/HIT/Truncation.lagda.md +++ b/src/1Lab/HIT/Truncation.lagda.md @@ -106,8 +106,11 @@ whenever it is a family of propositions, by providing a case for → (x : ∥ A ∥) → P ∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop) -∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A -∥-∥-proj {ap = ap} = ∥-∥-rec ap λ x → x +∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A +∥-∥-proj ap = ∥-∥-rec ap λ x → x + +∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A +∥-∥-proj! {ap = ap} = ∥-∥-proj ap ``` --> diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md index d11f23185..b5598e396 100644 --- a/src/Cat/Univalent/Rezk/Universal.lagda.md +++ b/src/Cat/Univalent/Rezk/Universal.lagda.md @@ -86,7 +86,7 @@ eso→pre-faithful → is-eso H → (γ δ : F => G) → (∀ b → γ .η (H .F₀ b) ≡ δ .η (H .F₀ b)) → γ ≡ δ eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p = - Nat-path λ b → ∥-∥-proj {ap = C.Hom-set _ _ _ _} do + Nat-path λ b → ∥-∥-proj (C.Hom-set _ _ _ _) do (b′ , m) ← h-eso b ∥_∥.inc $ γ .η b ≡⟨ C.intror (F-map-iso F m .invl) ⟩ @@ -191,7 +191,7 @@ this file in Agda and poke around the proof. ```agda lemma : (a : A.Ob) (f : H.₀ a B.≅ b) → γ.η a ≡ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to) - lemma a f = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do + lemma a f = ∥-∥-proj (C.Hom-set _ _ _ _) do (k , p) ← H-full (h.from B.∘ B.to f) (k⁻¹ , q) ← H-full (B.from f B.∘ h.to) ∥_∥.inc $ @@ -216,7 +216,7 @@ over $b$ is a proposition. T-prop : ∀ b → is-prop (T b) T-prop b (g , coh) (g′ , coh′) = Σ-prop-path (λ x → Π-is-hlevel² 1 λ _ _ → C.Hom-set _ _ _ _) $ - ∥-∥-proj {ap = C.Hom-set _ _ _ _} do + ∥-∥-proj (C.Hom-set _ _ _ _) do (a₀ , h) ← H-eso b pure $ C.iso→epic (F-map-iso F h) _ _ (C.iso→monic (F-map-iso G (h B.Iso⁻¹)) _ _ @@ -236,7 +236,7 @@ $(a,h)$ pair. ∥_∥.inc (Mk.g b a₀ h , Mk.lemma b a₀ h) mkT : ∀ b → T b - mkT b = ∥-∥-proj {ap = T-prop b} (mkT′ b (H-eso b)) + mkT b = ∥-∥-proj (T-prop b) (mkT′ b (H-eso b)) ``` Another calculation shows that, since $H$ is full, given any pair of @@ -260,7 +260,7 @@ the transformation we're defining, too. module h = B._≅_ h naturality : _ - naturality = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do + naturality = ∥-∥-proj (C.Hom-set _ _ _ _) do (k , p) ← H-full (h′.from B.∘ f B.∘ h.to) pure $ C.pullr (C.pullr (F.weave (sym (B.pushl p ∙ ap₂ B._∘_ refl (B.cancelr h.invl))))) @@ -281,8 +281,8 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful. δ : F => G δ .η b = mkT b .fst δ .is-natural b b′ f = ∥-∥-elim₂ - {P = λ α β → ∥-∥-proj {ap = T-prop b′} (mkT′ b′ α) .fst C.∘ F.₁ f - ≡ G.₁ f C.∘ ∥-∥-proj {ap = T-prop b} (mkT′ b β) .fst} + {P = λ α β → ∥-∥-proj (T-prop b′) (mkT′ b′ α) .fst C.∘ F.₁ f + ≡ G.₁ f C.∘ ∥-∥-proj (T-prop b) (mkT′ b β) .fst} (λ _ _ → C.Hom-set _ _ _ _) (λ (a′ , h′) (a , h) → naturality f a a′ h h′) (H-eso b′) (H-eso b) @@ -290,7 +290,7 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful. full {x = x} {y = y} γ = pure (δ _ _ γ , Nat-path p) where p : ∀ b → δ _ _ γ .η (H.₀ b) ≡ γ .η b p b = subst - (λ e → ∥-∥-proj {ap = T-prop _ _ γ (H.₀ b)} (mkT′ _ _ γ (H.₀ b) e) .fst + (λ e → ∥-∥-proj (T-prop _ _ γ (H.₀ b)) (mkT′ _ _ γ (H.₀ b) e) .fst ≡ γ .η b) (squash (inc (b , B.id-iso)) (H-eso (H.₀ b))) (C.eliml (y .F-id) ∙ C.elimr (x .F-id)) @@ -377,7 +377,7 @@ candidate over it. + +```agda +module Data.Rel.Base where +``` + +# Relations + +A **relation** between types $A$ and $B$ consists of a family of types +indexed by $A$ and $B$. + +```agda +Rel : ∀ {a b} → Type a → Type b → (ℓ : Level) → Type _ +Rel A B ℓ = A → B → Type ℓ +``` + + + +We say that a relation is **propositional** if $R(x,y)$ is a proposition +for every $x$ and $y$. + +```agda +is-prop-rel : Rel A B ℓ → Type _ +is-prop-rel R = ∀ {x y} → is-prop (R x y) +``` + +## Operations on Propositional Relations + +We can take the union of two propositional relations by taking the +pointwise truncated +coproduct. + +```agda +_∪r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _ +R ∪r S = λ x y → ∥ R x y ⊎ S x y ∥ +``` + +Likewise, intersection can be defined by taking the pointwise product +of the two relations. + +```agda +_∩r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _ +R ∩r S = λ x y → R x y × S x y +``` + +We can compose two propositional relations by requiring the (mere) +existence of a common endpoint. + +```agda +_∘r_ : Rel B C ℓ → Rel A B ℓ' → Rel A C _ +R ∘r S = λ x y → ∃[ z ∈ _ ] (S x z × R z y) +``` + +Every relation between $A$ and $B$ can be flipped to get a relation +between $B$ and $A$. + +```agda +flipr : Rel A B ℓ → Rel B A ℓ +flipr R = λ x y → R y x +``` + +## Relationships between Relations + +We say that a relation $R$ is contained in another relation $S$ +if $R(x,y)$ implies $S(x,y)$ for every $x$ and $y$. + +```agda +_⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _ +R ⊆r S = ∀ {x y} → R x y → S x y + +_≃r_ : Rel A B ℓ → Rel A B ℓ' → Type _ +R ≃r S = ∀ {x y} → R x y ≃ S x y +``` + +```agda +⊆r-trans : R ⊆r S → S ⊆r T → R ⊆r T +⊆r-trans p q Rxy = q (p Rxy) +``` + + +Equality of propositional relations can be characterised in terms +of containment. + +```agda +prop-rel-ext + : is-prop-rel R → is-prop-rel S + → R ⊆r S → S ⊆r R → R ≡ S +prop-rel-ext R-prop S-prop R⊆S S⊆R = + funext λ x → funext λ y → ua (prop-ext R-prop S-prop R⊆S S⊆R) +``` + +## Properties of Relations + +A relation is **reflexive** if every element is related to itself. + +```agda +is-reflexive : Rel A A ℓ → Type _ +is-reflexive R = ∀ x → R x x +``` + +A relation is **symmetric** if every $R(x,y)$ implies that $R(y,x)$. + +```agda +is-symmetric : Rel A A ℓ → Type _ +is-symmetric R = ∀ {x y} → R x y → R y x +``` + +A relation is **transitive** if $R(x,y)$ and $R(y,z)$ implies that +$R(x,z)$. + +```agda +is-transitive : Rel A A ℓ → Type _ +is-transitive R = ∀ {x y z} → R x y → R y z → R x z +``` diff --git a/src/Data/Rel/Closure.agda b/src/Data/Rel/Closure.agda new file mode 100644 index 000000000..5a88290de --- /dev/null +++ b/src/Data/Rel/Closure.agda @@ -0,0 +1,12 @@ +-- This module doesn't have any text! That's because it's simply a bunch +-- of convenient re-exports for working with closures of relations + +module Data.Rel.Closure where + +open import Data.Rel.Base public +open import Data.Rel.Closure.Base public +open import Data.Rel.Closure.Reflexive public +open import Data.Rel.Closure.Symmetric public +open import Data.Rel.Closure.Transitive public +open import Data.Rel.Closure.ReflexiveTransitive public +open import Data.Rel.Closure.ReflexiveSymmetricTransitive public diff --git a/src/Data/Rel/Closure/Base.lagda.md b/src/Data/Rel/Closure/Base.lagda.md new file mode 100644 index 000000000..7079261a8 --- /dev/null +++ b/src/Data/Rel/Closure/Base.lagda.md @@ -0,0 +1,80 @@ + + +```agda +module Data.Rel.Closure.Base where +``` + + + +# Closures of relations + +A **closure operator** $-^{+}$ on relations takes a relation $R$ on a type +$A$ to a new relation $R^{+}$ on $A$, where $R^{+}$ is the smallest +relation containing $R$ that satisfies some property. + +Intuitively, the closure of a relation should enjoy the following properties: +- If $R \subseteq S$, then $R^{+} \subseteq S^{+}$. +- $R \subseteq R^{+}$ +- $(R^{+})^{+} \subseteq R^{+}$, as closing $R$ under a property twice shouldn't + add any more elements. + +This ends up forming a [monad], though we do not define a closure operator as +such due to annoying size restrictions. + +[monad]: Cat.Diagram.Monad.html + +```agda +record is-rel-closure + (K : ∀ {ℓ ℓ'} {A : Type ℓ} → Rel A A ℓ' → Rel A A (ℓ ⊔ ℓ')) + : Typeω where + field + monotone : R ⊆r S → K R ⊆r K S + extensive : R ⊆r K R + closed : K (K R) ⊆r K R + has-prop : is-prop-rel (K R) +``` + +Closure, monotonicity, and extensivity combine to give idempotence +of the closure operator. + +```agda + idempotent : K (K R) ≡ K R + idempotent = + prop-rel-ext has-prop has-prop + closed + (monotone extensive) +``` + +We can also derive an extension operator using the normal formulation +for monads. + +```agda + extend : S ⊆r K R → K S ⊆r K R + extend p kr = closed (monotone p kr) +``` + +We can leverage this to see that if $R \subseteq S \subseteq K R$, then +$K R = K S$. + +```agda + ⊆+⊆-clo→≃ : S ⊆r R → R ⊆r K S → K R ≃r K S + ⊆+⊆-clo→≃ p q = + prop-ext has-prop has-prop (extend q) (monotone p) +``` diff --git a/src/Data/Rel/Closure/Reflexive.lagda.md b/src/Data/Rel/Closure/Reflexive.lagda.md new file mode 100644 index 000000000..aeb042332 --- /dev/null +++ b/src/Data/Rel/Closure/Reflexive.lagda.md @@ -0,0 +1,146 @@ + + +```agda +module Data.Rel.Closure.Reflexive where +``` + + + +# Reflexive Closure + +The reflexive [closure] of a [relation] $R$ is the smallest reflexive +relation $R^{=}$ that contains $R$. + +[relation]: Data.Rel.Base.html +[closure]: Data.Rel.Closure.html + +```agda +data Refl {A : Type ℓ} (R : Rel A A ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where + reflexive : Refl R x x + [_] : ∀ {y} → R x y → Refl R x y + trunc : ∀ {y} → is-prop (Refl R x y) +``` + + + +The recursion principle for the reflexive closure of a relation witnesses +the aforementioned universal property: it is the smallest reflexive +relation containing $R$. + +```agda +Refl-rec + : (S : A → A → Type ℓ) + → (∀ {x y} → R x y → S x y) + → (∀ x → S x x) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl R x y → S x y +Refl-rec {R = R} S prel prefl pprop r+ = go r+ where + go : ∀ {x y} → Refl R x y → S x y + go reflexive = prefl _ + go [ r ] = prel r + go (trunc r+ r+' i) = pprop (go r+) (go r+') i +``` + + + + +## As a closure operator + +As the name suggests, the reflexive closure of a relation forms a closure +operator. + +```agda +refl-clo-mono : R ⊆r S → Refl R ⊆r Refl S +refl-clo-mono {S = S} p = + Refl-rec (Refl S) (λ r → [ p r ]) (λ _ → reflexive) trunc + +refl-clo-closed : Refl (Refl R) ⊆r Refl R +refl-clo-closed {R = R} = Refl-rec (Refl R) id (λ _ → reflexive) trunc + +refl-closure : is-rel-closure Refl +refl-closure .is-rel-closure.monotone = refl-clo-mono +refl-closure .is-rel-closure.extensive = [_] +refl-closure .is-rel-closure.closed = refl-clo-closed +refl-closure .is-rel-closure.has-prop = trunc +``` + +## Properties + +If the original relation is symmetric or transitive, then so is the +reflexive closure. + +```agda +refl-clo-symmetric + : is-symmetric R + → is-symmetric (Refl R) +refl-clo-symmetric {R = R} is-sym = + Refl-rec (λ x y → Refl R y x) + (λ r → [ is-sym r ]) + (λ _ → reflexive) + trunc + +refl-clo-transitive : is-transitive R → is-transitive (Refl R) +refl-clo-transitive {R = R} is-trans = + Refl-rec₂ (λ x _ z → Refl R x z) + (λ x~*y y~*z → [ is-trans x~*y y~*z ]) + [_] + [_] + (λ _ → reflexive) + trunc +``` diff --git a/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md new file mode 100644 index 000000000..a5507ee7a --- /dev/null +++ b/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md @@ -0,0 +1,164 @@ + + +```agda +module Data.Rel.Closure.ReflexiveSymmetricTransitive where +``` + + + +# Reflexive-Symmetric-Transitive Closure + +Finally, the reflexive-symmetric-transitive closure of a relation $R$ is +the smallest reflexive, symmetric, and transitive relation +$R^{\leftrightarrow*}$ that contains $R$. + +```agda +data Refl-sym-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where + [_] : ∀ {y} → R x y → Refl-sym-trans R x y + reflexive : Refl-sym-trans R x x + symmetric : ∀ {y} → Refl-sym-trans R y x → Refl-sym-trans R x y + transitive : ∀ {y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → Refl-sym-trans R x z + trunc : ∀ {y} → is-prop (Refl-sym-trans R x y) +``` + + + +Yet again, the recursion principle for the reflexive, symmetric, +transitive closure witnesses it's universal property; it is the smallest +reflexive, symmetric, transitive relation containing $R$. + +```agda +Refl-sym-trans-rec + : (S : A → A → Type ℓ) + → (∀ {x y} → (r : R x y) → S x y) + → (∀ {x} → S x x) + → (∀ {x y} → S x y → S y x) + → (∀ {x y z} → S x y → S y z → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl-sym-trans R x y → S x y +Refl-sym-trans-rec {R = R} S prel prefl psym ptrans pprop r+ = go r+ where + go : ∀ {x y} → Refl-sym-trans R x y → S x y + go [ r ] = prel r + go reflexive = prefl + go (symmetric r) = psym (go r) + go (transitive r+ s+) = ptrans (go r+) (go s+) + go (trunc r+ r+' i) = pprop (go r+) (go r+') i +``` + +We also define an alternative recursion principle for inducting down +the length of the chain of relations. + +```agda +Refl-sym-trans-rec-chain + : (S : A → A → Type ℓ) + → (∀ {x} → S x x) + → (∀ {x y z} → R x y → Refl-sym-trans R y z → S y z → S x z) + → (∀ {x y z} → R y x → Refl-sym-trans R y z → S y z → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl-sym-trans R x y → S x y +Refl-sym-trans-rec-chain {R = R} S pnil pstep pinv pprop r+ = go r+ reflexive pnil where + go : ∀ {x y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → S y z → S x z + go-sym : ∀ {x y z} → Refl-sym-trans R y x → Refl-sym-trans R y z → S y z → S x z + + go [ x→y ] y→*z acc = pstep x→y y→*z acc + go reflexive y→*z acc = acc + go (symmetric y→*x) y→*z acc = go-sym y→*x y→*z acc + go (transitive x→*x' x'→*y) y→*z acc = + go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc) + go (trunc x→*y x→*y' i) y→*z acc = + pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i + + go-sym [ y→x ] y→*z acc = pinv y→x y→*z acc + go-sym reflexive y→*z acc = acc + go-sym (symmetric x→*y) y→*z acc = go x→*y y→*z acc + go-sym (transitive y→*y' y'→*x) y→*z acc = + go-sym y'→*x (transitive (symmetric y→*y') y→*z) (go-sym y→*y' y→*z acc) + go-sym (trunc y→*x y→*x' i) y→*z acc = + pprop (go-sym y→*x y→*z acc) (go-sym y→*x' y→*z acc) i +``` + +## As a closure operator + +```agda +refl-sym-trans-clo-mono : R ⊆r S → Refl-sym-trans R ⊆r Refl-sym-trans S +refl-sym-trans-clo-mono {S = S} p = + Refl-sym-trans-rec (Refl-sym-trans S) + (λ r → [ p r ]) + reflexive + symmetric + transitive + trunc + +refl-sym-trans-clo-closed : Refl-sym-trans (Refl-sym-trans R) ⊆r Refl-sym-trans R +refl-sym-trans-clo-closed {R = R} = + Refl-sym-trans-rec (Refl-sym-trans R) + id + reflexive + symmetric + transitive + trunc + +refl-sym-trans-closure : is-rel-closure Refl-sym-trans +refl-sym-trans-closure .is-rel-closure.monotone = refl-sym-trans-clo-mono +refl-sym-trans-closure .is-rel-closure.extensive = [_] +refl-sym-trans-closure .is-rel-closure.closed = refl-sym-trans-clo-closed +refl-sym-trans-closure .is-rel-closure.has-prop = trunc +``` + +## Properties + +The reflexive-transitive closure embeds into the reflexive symmetric +transitive closure. + +```agda +refl-trans⊆refl-sym-trans + : Refl-trans R ⊆r Refl-sym-trans R +refl-trans⊆refl-sym-trans = + Refl-trans-rec (Refl-sym-trans _) [_] reflexive transitive trunc +``` diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md new file mode 100644 index 000000000..468c4f179 --- /dev/null +++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md @@ -0,0 +1,334 @@ + + +```agda +module Data.Rel.Closure.ReflexiveTransitive where +``` + + + +# Reflexive-Transitive Closure + +The reflexive-transitive [closure] of a [relation] $R$ is the smallest +reflexive and transitive relation $R^{*}$ that contains $R$. + +[relation]: Data.Rel.Base.html +[closure]: Data.Rel.Closure.html + +```agda +data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where + [_] : ∀ {y} → R x y → Refl-trans R x y + reflexive : Refl-trans R x x + transitive : ∀ {y z} → Refl-trans R x y → Refl-trans R y z → Refl-trans R x z + trunc : ∀ {y} → is-prop (Refl-trans R x y) +``` + + + +Following the general theme, the recursion principle for the reflexive +transitive closure witnesses it's universal property; it is the smallest +reflexive and transitive relation containing $R$. + +```agda +Refl-trans-rec + : (S : A → A → Type ℓ) + → (∀ {x y} → (r : R x y) → S x y) + → (∀ {x} → S x x) + → (∀ {x y z} → S x y → S y z → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl-trans R x y → S x y +Refl-trans-rec {R = R} S prel prefl ptrans pprop r+ = go r+ where + go : ∀ {x y} → Refl-trans R x y → S x y + go [ r ] = prel r + go reflexive = prefl + go (transitive r+ s+) = ptrans (go r+) (go s+) + go (trunc r+ r+' i) = pprop (go r+) (go r+') i +``` + +We also provide a recursion principle that inducts down the length of the +chain of relations. + +```agda +Refl-trans-rec-chain + : (S : A → A → Type ℓ) + → (∀ {x} → S x x) + → (∀ {x y z} → R x y → Refl-trans R y z → S y z → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl-trans R x y → S x y +Refl-trans-rec-chain {R = R} S pnil pstep pprop r+ = go r+ reflexive pnil where + go : ∀ {x y z} → Refl-trans R x y → Refl-trans R y z → S y z → S x z + go [ x→y ] y→*z acc = pstep x→y y→*z acc + go reflexive y→*z acc = acc + go (transitive x→*x' x'→*y) y→*z acc = + go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc) + go (trunc x→*y x→*y' i) y→*z acc = + pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i +``` + +It's useful to be able to perform induction in the reverse direction, so +we also provide a recursion principle for doing so. + +```agda +Refl-trans-rec-chain-bwd + : (S : A → A → Type ℓ) + → (∀ {x} → S x x) + → (∀ {x y z} → Refl-trans R x y → R y z → S x y → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Refl-trans R x y → S x y +Refl-trans-rec-chain-bwd {R = R} S pnil pstep pprop {x = x} r+ = + Refl-trans-rec-chain (λ y z → Refl-trans R x y → S x y → S x z) + (λ _ Sxx' → Sxx') + (λ {x'} {y} {z} x'→y y→*z ih x→*x' Sxx' → + ih (transitive x→*x' [ x'→y ]) (pstep x→*x' x'→y Sxx')) + (Π-is-hlevel 1 λ _ → Π-is-hlevel 1 λ _ → pprop) + r+ reflexive pnil +``` + + +We also provide an eliminator for inspecting forks. + +```agda +Refl-trans-case-fork + : (S : A → A → A → Type ℓ) + → (∀ {a y} → Refl-trans R' a y → S a a y) + → (∀ {a x} → Refl-trans R a x → S a x a) + → (∀ {a x y x' y'} + → R a x' → Refl-trans R x' x + → R' a y' → Refl-trans R' y' y + → S a x y) + → (∀ {a x y} → is-prop (S a x y)) + → ∀ {a x y} → Refl-trans R a x → Refl-trans R' a y → S a x y +Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y = + Refl-trans-rec-chain (λ a x → Refl-trans R' a y → S a x y) + refll + (λ {a} {a'} {x} a→a' a'→*x _ a→*y → + Refl-trans-rec-chain + (λ a y → R a a' → Refl-trans R a' x → S a x y) + (λ a→a' a'→*x → reflr (transitive [ a→a' ] a'→*x)) + (λ a→a' a'→*y _ a→a'' a''→*x → fork a→a'' a''→*x a→a' a'→*y) + (Π-is-hlevel 1 (λ _ → Π-is-hlevel 1 λ _ → prop)) + a→*y a→a' a'→*x) + (Π-is-hlevel 1 (λ _ → prop)) + a→*x a→*y +``` + +Similarly, we provide an eliminator for inspecting wedges. + +```agda +Refl-trans-case-wedge + : (S : A → A → A → Type ℓ) + → (∀ {z} → S z z z) + → (∀ {x y y' z} → R' y y' → Refl-trans R' y' z → S x y z) + → (∀ {x x' y z} → R x x' → Refl-trans R x' z → S x y z) + → (∀ {x y z} → is-prop (S x y z)) + → ∀ {x y z} → Refl-trans R x z → Refl-trans R' y z → S x y z +Refl-trans-case-wedge {R' = R'} {R = R} S refl2 wedgel wedger prop {x} {y} {z} x→*z y→*z = + Refl-trans-rec-chain (λ x z → Refl-trans R' y z → S x y z) + (λ y→*z → Refl-trans-rec-chain (λ y z → S z y z) + refl2 + (λ y→y' y'→*z _ → wedgel y→y' y'→*z) + prop + y→*z) + (λ x→x' x'→z _ _ → wedger x→x' x'→z) + (Π-is-hlevel 1 λ _ → prop) + x→*z y→*z +``` + + +## As a closure operator + +```agda +refl-trans-clo-mono : R ⊆r S → Refl-trans R ⊆r Refl-trans S +refl-trans-clo-mono {S = S} p = + Refl-trans-rec (Refl-trans S) + (λ r → [ p r ]) + reflexive + transitive + trunc + +refl-trans-clo-closed : Refl-trans (Refl-trans R) ⊆r Refl-trans R +refl-trans-clo-closed {R = R} = + Refl-trans-rec (Refl-trans R) + id + reflexive + transitive + trunc + +refl-trans-closure : is-rel-closure Refl-trans +refl-trans-closure .is-rel-closure.monotone = refl-trans-clo-mono +refl-trans-closure .is-rel-closure.extensive = [_] +refl-trans-closure .is-rel-closure.closed = refl-trans-clo-closed +refl-trans-closure .is-rel-closure.has-prop = trunc +``` + +## Properties + +If the underlying relation is symmetric, then so is the +reflexive-transitive closure. + +```agda +refl-trans-clo-symmetric : is-symmetric R → is-symmetric (Refl-trans R) +refl-trans-clo-symmetric {R = R} is-sym r+ = + Refl-trans-rec (λ x y → Refl-trans R y x) + (λ r → [ is-sym r ]) + reflexive + (λ r+ s+ → transitive s+ r+) + trunc + r+ +``` + +The reflexive closure and the transitive closure are contained in +the reflexive transitive closure. + +```agda +refl-clo⊆refl-trans-clo : Refl R ⊆r Refl-trans R +refl-clo⊆refl-trans-clo {R = R} = + Refl-rec (Refl-trans R) [_] (λ _ → reflexive) hlevel! + +trans-clo⊆refl-trans-clo : Trans R ⊆r Refl-trans R +trans-clo⊆refl-trans-clo {R = R} = + Trans-rec (Refl-trans R) [_] transitive hlevel! +``` + + +Note that the reflexive-transitive closure is equivalent to taking +the reflexive closure of the transitive closure. + +```agda +refl-clo-trans-clo⊆refl-trans-clo : Refl (Trans R) ⊆r Refl-trans R +refl-clo-trans-clo⊆refl-trans-clo {R = R} = + Refl-rec (Refl-trans R) + trans-clo⊆refl-trans-clo + (λ _ → reflexive) + hlevel! + +refl-trans-clo⊆refl-clo-trans-clo : Refl-trans R ⊆r Refl (Trans R) +refl-trans-clo⊆refl-clo-trans-clo {R = R} = + Refl-trans-rec (Refl (Trans R)) + (λ x~y → [ [ x~y ] ]) + reflexive + (refl-clo-transitive transitive) + hlevel! + +refl-clo-trans-clo≡refl-trans-clo : Refl (Trans R) ≡ Refl-trans R +refl-clo-trans-clo≡refl-trans-clo {R = R} = + prop-rel-ext trunc trunc + refl-clo-trans-clo⊆refl-trans-clo + refl-trans-clo⊆refl-clo-trans-clo +``` + +The same can be said for the transitive closure of the reflexive closure. + +```agda +trans-clo-refl-clo⊆refl-trans-clo : Trans (Refl R) ⊆r Refl-trans R +trans-clo-refl-clo⊆refl-trans-clo {R = R} = + Trans-rec (Refl-trans R) + refl-clo⊆refl-trans-clo + transitive + hlevel! + +refl-trans-clo⊆trans-clo-refl-clo : Refl-trans R ⊆r Trans (Refl R) +refl-trans-clo⊆trans-clo-refl-clo {R = R} = + Refl-trans-rec (Trans (Refl R)) + (λ x~y → [ [ x~y ] ]) + [ reflexive ] + transitive + hlevel! + +trans-clo-refl-clo≡refl-trans-clo : Trans (Refl R) ≡ Refl-trans R +trans-clo-refl-clo≡refl-trans-clo {R = R} = + prop-rel-ext trunc trunc + trans-clo-refl-clo⊆refl-trans-clo + refl-trans-clo⊆trans-clo-refl-clo +``` + +The reflexive-transitive closures of $R$ and $S$ are contained in the +transitive closure of $R \cup S$. + +```agda +refl-trans-clo-inl : Refl-trans R ⊆r Refl-trans (R ∪r S) +refl-trans-clo-inl = + refl-trans-clo-mono (λ r → inc (inl r)) + +refl-trans-clo-inr : Refl-trans S ⊆r Refl-trans (R ∪r S) +refl-trans-clo-inr = + refl-trans-clo-mono (λ s → inc (inr s)) +``` + + +The union of $R$ and $S$ is contained within $S^{*} \circ R^{*}$. + +```agda +union⊆comp-trans-clo + : (R ∪r S) ⊆r (Refl-trans S ∘r Refl-trans R) +union⊆comp-trans-clo {x = x} {y = y} = + ∥-∥-map + (⊎-rec + (λ x↝₁y → y , ([ x↝₁y ] , reflexive)) + (λ x↝₂y → x , reflexive , [ x↝₂y ])) +``` + +The composition of the reflexive-transitive closures of $R$ and $S$ is +contained within the reflexive-transitive closure of their union. + +```agda +comp-trans-clo⊆trans-clo-union + : (Refl-trans S ∘r Refl-trans R) ⊆r Refl-trans (R ∪r S) +comp-trans-clo⊆trans-clo-union {x = x} {y = y} = + ∥-∥-rec trunc + (λ { (w , x↝₁w , w↝₂y) → + transitive (refl-trans-clo-inl x↝₁w) (refl-trans-clo-inr w↝₂y) }) +``` + +Therefore, the reflexive-transitive closure of the $R \cup S$ +the reflexive-transitive closure of $S^{*} \circ R^{*}$. + +```agda +refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo + : Refl-trans (Refl-trans S ∘r Refl-trans R) ≃r Refl-trans (R ∪r S) +refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo = + is-rel-closure.⊆+⊆-clo→≃ refl-trans-closure + union⊆comp-trans-clo + comp-trans-clo⊆trans-clo-union +``` diff --git a/src/Data/Rel/Closure/Symmetric.lagda.md b/src/Data/Rel/Closure/Symmetric.lagda.md new file mode 100644 index 000000000..e6fa10a36 --- /dev/null +++ b/src/Data/Rel/Closure/Symmetric.lagda.md @@ -0,0 +1,189 @@ + + + +```agda +module Data.Rel.Closure.Symmetric where +``` + + + +# Symmetric Closure + +The symmetric [closure] of a [relation] $R$ is the smallest symmetric +relation $R^{\leftrightarrow}$ that contains $R$. + +[closure]: Data.Rel.Closure.html +[relation]: Data.Rel.Base.html + +```agda +data Sym {A : Type ℓ} (R : A → A → Type ℓ') (x y : A) : Type (ℓ ⊔ ℓ') where + symmetric : Sym R y x → Sym R x y + [_] : R x y → Sym R x y + trunc : is-prop (Sym R x y) +``` + + + +Like the [reflexive closure], the recursion principle for the symmetric +closure witnesses it's universal property; it is the smallest symmetric +relation containing $R$. + +[reflexive closure]: Data.Rel.Closure.Reflexive.html + +```agda +Sym-rec + : (S : A → A → Type ℓ) + → (∀ {x y} → R x y → S x y) + → (∀ {x y} → S x y → S y x) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Sym R x y → S x y +Sym-rec {R = R} S prel psym pprop r+ = go r+ where + go : ∀ {x y} → Sym R x y → S x y + go (symmetric r) = psym (go r) + go [ r ] = prel r + go (trunc r+ r+' i) = pprop (go r+) (go r+') i +``` + +## As a closure operator + +It is straightforward to show that the symmetric closure is a closure +operator. + +```agda +sym-clo-mono : R ⊆r S → Sym R ⊆r Sym S +sym-clo-mono {S = S} p = + Sym-rec (Sym S) (λ r → [ p r ]) symmetric trunc + +sym-clo-closed : Sym (Sym R) ⊆r Sym R +sym-clo-closed {R = R} = + Sym-rec (Sym R) id symmetric trunc + +sym-closure : is-rel-closure Sym +sym-closure .is-rel-closure.monotone = sym-clo-mono +sym-closure .is-rel-closure.extensive = [_] +sym-closure .is-rel-closure.closed = sym-clo-closed +sym-closure .is-rel-closure.has-prop = trunc +``` + + +## Properties + +If two elements $x$ and $y$ are related in the symmetric closure, then +either $R x y$ or $R y x$ in the original relation. + +```agda +sym-clo-rel + : ∀ {x y} → Sym R x y → ∥ (R x y) ⊎ (R y x) ∥ +sym-clo-rel {R = R} = + Sym-rec (λ x y → ∥ (R x y) ⊎ (R y x) ∥) + (λ r → inc (inl r)) + (∥-∥-map (⊎-rec inr inl)) + squash +``` + +If the original relation is reflexive, then so is the symmetric closure. + +```agda +sym-clo-reflexive : is-reflexive R → is-reflexive (Sym R) +sym-clo-reflexive is-refl x = [ is-refl x ] +``` + +Note that this is *not* true for transitivity! To see why, consider an +irreflexive transitive relation on a type with at least related 2 +elements $R x y$ . If the symmetric closure of this relation was +transitive, we'd be able to create a loop $R^{\leftrightarrow} x x$ in +the symmetric closure by composing the relations $R^{\leftrightarrow} x +y$ and $R^{\leftrightarrow} y x$. However, if two elements are related +in the symmetric closure, then they must be related in the original +relation, which leads directly to a contradiction, as the original +relation is irreflexive. + +For simplicity, we show this for the strict ordering on the natural +numbers. + +```agda +private + ¬sym-clo-transitive + : ¬ (is-transitive (Sym Nat._<_)) + ¬sym-clo-transitive sym-clo-trans = + ∥-∥-rec! (⊎-rec (Nat.<-irrefl refl) (Nat.<-irrefl refl)) + (sym-clo-rel (sym-clo-trans [ 0<1 ] (symmetric [ 0<1 ]))) + where + 0<1 : 0 Nat.< 1 + 0<1 = Nat.s≤s Nat.0≤x +``` + +As a corollary, we can see that the transitive closure of the symmetric closure +is not the same as the symmetric closure of the transitive closure. + +However, the reflexive closure of the symmetric closure is equal to the +symmetric closure of the reflexive closure. + +```agda +sym-clo-refl-clo⊆refl-clo-sym-clo : Sym (Refl R) ⊆r Refl (Sym R) +sym-clo-refl-clo⊆refl-clo-sym-clo {R = R} = + Sym-rec (Refl (Sym R)) + (Refl-rec (Refl (Sym R)) + (λ x~y → [ [ x~y ] ]) + (λ _ → reflexive) + hlevel!) + (Refl-rec (flipr (Refl (Sym R))) + (λ y~x → [ symmetric y~x ] ) + (λ _ → reflexive) + hlevel!) + hlevel! + +refl-clo-sym-clo⊆sym-clo-refl-clo : Refl (Sym R) ⊆r Sym (Refl R) +refl-clo-sym-clo⊆sym-clo-refl-clo {R = R} = + Refl-rec (Sym (Refl R)) + (Sym-rec (Sym (Refl R)) + (λ x~y → [ [ x~y ] ]) + symmetric + hlevel!) + (λ _ → [ reflexive ]) + hlevel! + +refl-clo-sym-clo≡sym-clo-refl-clo : Refl (Sym R) ≡ Sym (Refl R) +refl-clo-sym-clo≡sym-clo-refl-clo = + prop-rel-ext trunc trunc + refl-clo-sym-clo⊆sym-clo-refl-clo + sym-clo-refl-clo⊆refl-clo-sym-clo +``` diff --git a/src/Data/Rel/Closure/Transitive.lagda.md b/src/Data/Rel/Closure/Transitive.lagda.md new file mode 100644 index 000000000..2b1f52c80 --- /dev/null +++ b/src/Data/Rel/Closure/Transitive.lagda.md @@ -0,0 +1,113 @@ + + +```agda +module Data.Rel.Closure.Transitive where +``` + + + +# Transitive Closure + +The transitive [closure] of a [relation] $R$ is the smallest transitive +relation $R^{+}$ that contains $R$. + +[relation]: Data.Rel.Base.html +[closure]: Data.Rel.Closure.html + +```agda +data Trans {A : Type ℓ} (_~_ : Rel A A ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where + [_] : x ~ z → Trans _~_ x z + transitive : ∀ {y} → Trans _~_ x y → Trans _~_ y z → Trans _~_ x z + trunc : is-prop (Trans _~_ x z) +``` + + + +The recursion principle for the transitive closure witnesses it's +universal property; it is the smallest transitive relation containing $R$. + +```agda +Trans-rec + : (S : A → A → Type ℓ) + → (∀ {x y} → (r : R x y) → S x y) + → (∀ {x y z} → S x y → S y z → S x z) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → Trans R x y → S x y +Trans-rec {R = R} S prel ptrans pprop r+ = go r+ where + go : ∀ {x y} → Trans R x y → S x y + go [ r ] = prel r + go (transitive r+ s+) = ptrans (go r+) (go s+) + go (trunc r+ r+' i) = pprop (go r+) (go r+') i +``` + +## As a closure operator + +```agda +trans-clo-mono : R ⊆r S → Trans R ⊆r Trans S +trans-clo-mono {S = S} p = + Trans-rec (Trans S) (λ r → [ p r ]) transitive trunc + +trans-clo-closed : Trans (Trans R) ⊆r Trans R +trans-clo-closed {R = R} = + Trans-rec (Trans R) id transitive trunc + +trans-closure : is-rel-closure Trans +trans-closure .is-rel-closure.monotone = trans-clo-mono +trans-closure .is-rel-closure.extensive = [_] +trans-closure .is-rel-closure.closed = trans-clo-closed +trans-closure .is-rel-closure.has-prop = trunc +``` + +## Properties + +If the original relation is reflexive or symmetric, then so is the +transitive closure. + +```agda +trans-clo-reflexive : is-reflexive R → is-reflexive (Trans R) +trans-clo-reflexive is-refl x = [ is-refl x ] + +trans-clo-symmetric : is-symmetric R → is-symmetric (Trans R) +trans-clo-symmetric {R = R} is-sym r+ = + Trans-rec (λ x y → Trans R y x) + (λ r → [ is-sym r ]) + (λ r+ s+ → transitive s+ r+) + trunc + r+ +``` diff --git a/src/Data/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md index e8fbae44f..9d192662c 100644 --- a/src/Data/Set/Material.lagda.md +++ b/src/Data/Set/Material.lagda.md @@ -285,8 +285,8 @@ Presentation-is-prop {ℓ} {A} f P1 P2 = done where eqv : ∀ x → fibre g x ≃ fibre h x eqv x = prop-ext (gm x) (hm x) - (λ fib → ∥-∥-proj {ap = hm x} (v' .fst x (u' .snd x (inc fib)))) - (λ fib → ∥-∥-proj {ap = gm x} (u' .fst x (v' .snd x (inc fib)))) + (λ fib → ∥-∥-proj (hm x) (v' .fst x (u' .snd x (inc fib)))) + (λ fib → ∥-∥-proj (gm x) (u' .fst x (v' .snd x (inc fib)))) ``` This pointwise equivalence between fibres extends to an equivalence @@ -386,7 +386,7 @@ module Members {ℓ} (X : V ℓ) where memb : ∀ {x} → x ∈ₛ X ≃ fibre elem x memb {x = x} = prop-ext (is-member _ X .is-tr) (embeds _) - (λ a → ∥-∥-proj {ap = embeds _} (subst (x ∈ₛ_) presents a)) + (λ a → ∥-∥-proj (embeds _) (subst (x ∈ₛ_) presents a)) (λ a → subst (x ∈ₛ_) (sym presents) (inc a)) module memb {x} = Equiv (memb {x}) diff --git a/src/Data/Sum/Base.lagda.md b/src/Data/Sum/Base.lagda.md index dd21cf6fa..42efc3e6c 100644 --- a/src/Data/Sum/Base.lagda.md +++ b/src/Data/Sum/Base.lagda.md @@ -45,10 +45,26 @@ One of the most important things about sum types is the following property: given two functions `A → C` and `B → C`, we can construct a function `A ⊎ B → C`. + + ```agda +⊎-rec : (A → C) → (B → C) → (A ⊎ B) → C +⊎-rec f g (inl x) = f x +⊎-rec f g (inr x) = g x + [_,_] : (A → C) → (B → C) → (A ⊎ B) → C -[ f , g ] (inl x) = f x -[ f , g ] (inr x) = g x +[_,_] = ⊎-rec +{-# INLINE [_,_] #-} ``` Furthermore, this function is "universal" in the following sense: if we diff --git a/src/Order/Semilattice/Free.lagda.md b/src/Order/Semilattice/Free.lagda.md index 688d38e46..66fd54ef8 100644 --- a/src/Order/Semilattice/Free.lagda.md +++ b/src/Order/Semilattice/Free.lagda.md @@ -194,7 +194,7 @@ $K$-finiteness condition, but it will be very useful! .glb≤fam i → K-fin-lt {P , P-fin} {ηₛₗ (cover i .fst)} λ j i=j → subst (λ e → ∣ P e ∣) (out! i=j) (cover i .snd) - .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj do + .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj! do (idx , path) ← surj (i , i∈p) pure (K-fin-lt′ {lb′} {ηₛₗ (cover idx .fst)} (wit idx) i (inc (ap fst path))) ``` @@ -267,7 +267,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where pres .pres-⋆ (A , af) (B , bf) = ap fst $ glb-unique y.po (go.ε′ (_∪_ x (A , af) (B , bf) .fst) (_∪_ x (A , af) (B , bf) .snd)) $ _ , λ where - .glb≤fam (x , w) → ∥-∥-proj $ w >>= λ where + .glb≤fam (x , w) → ∥-∥-proj! $ w >>= λ where (inl w) → pure $ g1 .fst y.∩ g2 .fst y.≤⟨ y.∩≤l ⟩ g1 .fst y.≤⟨ g1.glb≤fam (x , w) ⟩ @@ -287,7 +287,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where make-free-slat .commutes {y = y} f = funext λ x → sym y.∩-idr where module y = Semilattice y make-free-slat .unique {x = x} {y = y} {f = f} {g = g} w = - Homomorphism-path λ arg → ∥-∥-proj {ap = y.has-is-set _ _} do + Homomorphism-path λ arg → ∥-∥-proj (y.has-is-set _ _) do (card , diagram , glb) ← K-reduce x arg let path : arg ≡ KA.⋂ λ i → ηₛₗ x (diagram i) diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md new file mode 100644 index 000000000..6d38ea9a8 --- /dev/null +++ b/src/Rewriting/Base.lagda.md @@ -0,0 +1,269 @@ + + +```agda +module Rewriting.Base where +``` + + + +# Abstract Rewriting Systems + +Many problems in computer science can be phrased in terms of +**term rewriting systems**. Concretely, these are given by a collection +of terms in some language, along with a collection of rules that describe +how we can simplify terms. As an example, the untyped $\lambda$-calculus +can be naturally presented as a term rewriting system, where only +reduction rule is $\beta$-reduction. More abstractly, a rewriting system +on a type $A$ is simply a [relation] $\to$ on $A$ which encodes the +rewriting rules. Sequences of rewrites are then described using the +[reflexive transitive closure] of $\to$. + +[relation]: Data.Rel.Base.html +[reflexive transitive closure]: Data.Rel.Closure.ReflexiveTransitive.html + +## Basic Concepts + +Let $R$ and $S$ be a pair of relations on $A$. We say that +2 elements $x$ and $y$ are **joinable** by $R$ and $S$ if there +exists some $z$ such that $R(x,z)$ and $S(y,z)$. + +```agda +is-joinable + : ∀ {ℓa ℓr ℓs} {A : Type ℓa} + → (R : Rel A A ℓr) (S : Rel A A ℓs) + → A → A → Type _ +is-joinable {A = A} R S x y = ∃[ z ∈ A ] (R x z × S y z) +``` + +This is equivalent to the composite of $S^{-1}$ and $R$, but this is +less intuitive to think about. + +```agda +private + ∘≡joinable + : ∀ {R : Rel A A ℓ} {S : Rel A A ℓ'} {x y : A} + → (flipr S ∘r R) x y ≡ is-joinable R S x y + ∘≡joinable = refl +``` + +If $P \subseteq R$ and $Q \subseteq S$, then $R$ and $S$ are joinable +if $P$ and $Q$ are. + +```agda +joinable-⊆ + : P ⊆r R → Q ⊆r S + → ∀ x y → is-joinable P Q x y → is-joinable R S x y +joinable-⊆ P⊆R Q⊆S x y = ∥-∥-map λ where + (z , p , q) → z , P⊆R p , Q⊆S q +``` + + +Let $P$, $Q$, $R$ and $S$ all be relations on $A$. We say that $P$ and +$Q$ are resolvable by $R$ and $S$ if for all $x,y,z : A$, $P(x,y)$ and +$Q(x,z)$ implies that $y$ and $z$ are joinable by $R$ and $S$. + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z \\ + & {\exists! w} + \arrow["R"', dashed, from=2-1, to=3-2] + \arrow["S", dashed, from=2-3, to=3-2] + \arrow["P"', from=1-2, to=2-1] + \arrow["Q", from=1-2, to=2-3] +\end{tikzcd} +~~~ + +```agda +is-resolvable + : ∀ {ℓa ℓp ℓq ℓr ℓs} {A : Type ℓa} + → (P : Rel A A ℓp) → (Q : Rel A A ℓq) + → (R : Rel A A ℓr) → (S : Rel A A ℓs) + → Type _ +is-resolvable {A = A} P Q R S = + ∀ {x y z} → P x y → Q x z → is-joinable R S y z +``` + +This condition is equivalent to $Q \circ P^{-1} \subseteq S^{-1} \circ R$, +but the latter version is much more confusing to think about. + +```agda +private + ←∘→⊆→∘←≃resolvable + : ∀ {ℓa ℓp ℓq ℓr ℓs} {A : Type ℓa} + → {P : Rel A A ℓp} {Q : Rel A A ℓq} + → {R : Rel A A ℓr} {S : Rel A A ℓs} + → ((Q ∘r flipr P) ⊆r (flipr S ∘r R)) ≃ is-resolvable P Q R S + ←∘→⊆→∘←≃resolvable = + prop-ext! + (λ sub p q → sub (pure (_ , p , q))) + (λ diamond q∘p → do + x , p , q ← q∘p + diamond p q) +``` + +We also have the following useful lemma characterizing resolvability +of subrelations. + +```agda +resolvable-⊆ + : P' ⊆r P → Q' ⊆r Q + → R ⊆r R' → S ⊆r S' + → is-resolvable P Q R S → is-resolvable P' Q' R' S' +resolvable-⊆ p q r s sq {x = x} {y = y} x↝y x↝z = + joinable-⊆ r s x y (sq (p x↝y) (q x↝z)) +``` + +## Normal Forms + +Let $R$ be an abstract rewriting relation on a type $A$. We say +that an element $x : A$ is a **normal form** if it cannot be reduced +by $R$. + +```agda +is-normal-form : (R : Rel A A ℓ) → A → Type _ +is-normal-form {A = A} R x = ¬ Σ[ y ∈ A ] R x y +``` + +This allows us to give a restricted form of elimination for the +reflexive-transitive closure when the domain is a normal form. + +```agda +Refl-trans-rec-normal-form + : (S : A → A → Type ℓ) + → (∀ {x} → S x x) + → (∀ {x y} → is-prop (S x y)) + → ∀ {x y} → is-normal-form R x → Refl-trans R x y → S x y +Refl-trans-rec-normal-form {R = R} S srefl sprop x-nf x↝y = + Refl-trans-rec-chain + (λ x y → is-normal-form R x → S x y) + (λ _ → srefl) + (λ x↝y _ _ x-nf → absurd (x-nf (_ , x↝y))) + (Π-is-hlevel 1 λ _ → sprop) + x↝y x-nf +``` + + +If if $A$ is a set, $x : A$ is a normal form, and $x \to^{*} y$, then +$x = y$. + +```agda +normal-form+reduces→path + : ∀ {R : Rel A A ℓ} {x y} + → is-set A + → is-normal-form R x + → Refl-trans R x y + → x ≡ y +normal-form+reduces→path A-set = + Refl-trans-rec-normal-form _≡_ refl (A-set _ _) +``` + +As a corollary, if $x$ and $y$ are normal forms such that +$x \to^{*} z \leftarrow^{*} y$, then $x = y$. + +```agda +normal-forms+wedge→path + : ∀ {R : Rel A A ℓ} {x y z} + → is-set A + → is-normal-form R x → is-normal-form R y + → Refl-trans R x z → Refl-trans R y z + → x ≡ y +normal-forms+wedge→path set x-nf y-nf x↝z y↝z = + normal-form+reduces→path set x-nf x↝z + ∙ (sym $ normal-form+reduces→path set y-nf y↝z) +``` + + + + +If $x$ is a normal form, and $x \to^{*} z$ and $y \to^{*} z$, then +$y$ must reduce to $x$. + +```agda +normal-form+reduces→reduces + : ∀ {R : Rel A A ℓ} {x y z} + → is-normal-form R x + → Refl-trans R x z → Refl-trans R y z + → Refl-trans R y x +normal-form+reduces→reduces {R = R} {y = y} x-nf x↝z y↝z = + Refl-trans-rec-normal-form + (λ x z → Refl-trans R y z → Refl-trans R y x) + id + hlevel! + x-nf x↝z y↝z +``` + +A normal form of $x : A$ is another $y : A$ such that $y$ is a normal form +and $R^{*}(x,y)$. Note that this is untruncated; uniqueness of normal forms +shall be derived from other properties of $R$. + +```agda +record Normal-form {A : Type ℓ} (R : Rel A A ℓ') (x : A) : Type (ℓ ⊔ ℓ') where + constructor normal-form + no-eta-equality + field + nf : A + reduces : Refl-trans R x nf + has-normal-form : is-normal-form R nf + +open Normal-form +``` + +If $A$ is a set, then the type of normal forms is also a set. + +```agda +private unquoteDecl eqv = declare-record-iso eqv (quote Normal-form) + +Normal-form-is-hlevel + : ∀ {R : A → A → Type ℓ} {x} + → (n : Nat) → is-hlevel A (2 + n) → is-hlevel (Normal-form R x) (2 + n) +Normal-form-is-hlevel n A-set = + Iso→is-hlevel (2 + n) eqv (Σ-is-hlevel (2 + n) A-set hlevel!) +``` + + diff --git a/src/Rewriting/Commute.lagda.md b/src/Rewriting/Commute.lagda.md new file mode 100644 index 000000000..12cb63bd6 --- /dev/null +++ b/src/Rewriting/Commute.lagda.md @@ -0,0 +1,362 @@ + + +```agda +module Rewriting.Commute where +``` + + + +# Commuting Rewrite Systems + +Let $R$ and $S$ be a pair of [abstract rewrite systems] on a +type $A$. We say that $R$ **commutes** with $S$ if $R^{*}$ and +$S^{*}$ are resolvable by $S^{*}$ and $R^{*}$, as in the following +diagram. + +[abstract rewrite systems]: Rewriting.Base.html + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z \\ + & {\exists w} + \arrow["{S^*}"', dashed, from=2-1, to=3-2] + \arrow["{R^*}", dashed, from=2-3, to=3-2] + \arrow["{R^*}"', from=1-2, to=2-1] + \arrow["{S^*}", from=1-2, to=2-3] +\end{tikzcd} +~~~ + +```agda +commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _ +commutes-with R S = + is-resolvable + (Refl-trans R) (Refl-trans S) + (Refl-trans S) (Refl-trans R) +``` + +Intuitively, this condition ensures that applying a sequences of rewrites +from $R$ and $S$ don't let us diverge; we can always reconcile the two +by performing rewrites from $S$ and $R$, resp. This generalizes +[confluence], which states that a relation commutes with itself. + +[confluence]: Rewriting.Confluent.html + +This condition can be somewhat difficult to work with, so we introduce +an intermediate notion of **semi-commutation**, where one of the reflexive +transitive closures has been removed. + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z \\ + & {\exists w} + \arrow["{S^*}"', dashed, from=2-1, to=3-2] + \arrow["{R^*}", dashed, from=2-3, to=3-2] + \arrow["{R^*}"', from=1-2, to=2-1] + \arrow["S", from=1-2, to=2-3] +\end{tikzcd} +~~~ + +```agda +semi-commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _ +semi-commutes-with R S = + is-resolvable + (Refl-trans R) S + (Refl-trans S) (Refl-trans R) +``` + +Commutativity obviously implies semi-commutativity. + +```agda +commutes→semi-commutes : commutes-with R S → semi-commutes-with R S +commutes→semi-commutes comm x↝₁*y1 x↝₂y2 = + comm x↝₁*y1 [ x↝₂y2 ] +``` + +Furthermore, semi-commutativity implies commutativity. We begin with +the following situation: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1} && \bullet + \arrow["{R^*}"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow[dashed, from=3-1, to=3-3] + \arrow[dashed, from=1-3, to=3-3] +\end{tikzcd} +~~~ + +We then proceed by induction on the $S^*$. If it is an empty sequence of +rewrites, then we are done. If it is non-empty, then we have the following +situation: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2'} && {y_2} \\ + \\ + {y_1} &&&& \bullet + \arrow["{R^*}"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{S^*}", from=1-3, to=1-5] + \arrow[dashed, from=1-5, to=3-5] + \arrow[dashed, from=3-1, to=3-5] +\end{tikzcd} +~~~ + +We can apply semi-commutativity to fill in the left-hand square, as +in the following diagram. + +~~~{.quiver} +\begin{tikzcd} + x && {y_2'} && {y_2} \\ + \\ + {y_1} && {z'} && \bullet + \arrow["{R^*}"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow[dashed, from=1-5, to=3-5] + \arrow["{S^*}", from=1-3, to=1-5] + \arrow["{S^*}"', from=3-1, to=3-3] + \arrow["{R^*}", from=1-3, to=3-3] + \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] + \arrow[dashed, from=3-3, to=3-5] +\end{tikzcd} +~~~ + +Finally, we can use our induction hypothesis to fill in the right-hand +square, completing the proof. + +~~~{.quiver} +\begin{tikzcd} + x && {y_2'} && {y_2} \\ + \\ + {y_1} && {z'} && z + \arrow["{R^*}"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^*}", from=1-5, to=3-5] + \arrow["{S^*}", from=1-3, to=1-5] + \arrow["{S^*}"', from=3-1, to=3-3] + \arrow["{R^*}", from=1-3, to=3-3] + \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] + \arrow["{S^*}"', from=3-3, to=3-5] + \arrow["{I.H.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-3, to=3-5] +\end{tikzcd} +~~~ + +```agda +semi-commutes→commutes : semi-commutes-with R S → commutes-with R S +semi-commutes→commutes {R = R} {S = S} semi-comm x↝₁*y1 x↝₂*y2 = + Refl-trans-rec-chain + (λ x y2 → + ∀ y1 → Refl-trans R x y1 + → is-joinable (Refl-trans S) (Refl-trans R) y1 y2) + (λ y1 x↝₁*y1 → pure (y1 , reflexive , x↝₁*y1)) + (λ {x} {y2'} {y2} x↝₂y2' y2'↝₂*y2 ih y1 x↝₁*y1 → do + z' , y1↝₂*z' , y2'↝₁*z' ← semi-comm x↝₁*y1 x↝₂y2' + z , z'↝₂*z , y2↝₁*z ← ih z' y2'↝₁*z' + pure (z , transitive y1↝₂*z' z'↝₂*z , y2↝₁*z)) + hlevel! + x↝₂*y2 _ x↝₁*y1 +``` + +## Strong Commutativity + +Semi-commutativity is a useful notion when performing purely +rewrite-theoretic proofs, but it is still difficult to show, as it +is a global property rather than a local one. For this reason, we +introduce the notion of **strong commutativity**, which allows us +to resolve diamonds of the following form: + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z \\ + & {\exists w} + \arrow["R"', from=1-2, to=2-1] + \arrow["{S^{=}}"', dashed, from=2-1, to=3-2] + \arrow["{R^{*}}", dashed, from=2-3, to=3-2] + \arrow["S", from=1-2, to=2-3] +\end{tikzcd} +~~~ + +```agda +strongly-commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _ +strongly-commutes-with R S = + is-resolvable + R S + (Refl S) (Refl-trans R) +``` + +This property is generally easier to show, as it only involves resolving +one reduction step on either side, instead of an arbitrarily long chain. + +As the name suggests, strong commutativity is a stronger condition +than commutativity. We will prove this by showing that strong +commutativity implies semi-commutativity. + +Recall that semi-commutativity involves resolving a diagram of the +following shape: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1} && \bullet + \arrow["{R^{*}}"', from=1-1, to=3-1] + \arrow["{S^{=}}"', dashed, from=3-1, to=3-3] + \arrow["{R^{*}}", dashed, from=1-3, to=3-3] + \arrow["S", from=1-1, to=1-3] +\end{tikzcd} +~~~ + +We proceed by induction on the $R^{*}$; if it is an empty path, then +we are done. If it is non-empty, then we have the following situation: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1'} \\ + \\ + {y_1} && \bullet + \arrow["R"', from=1-1, to=3-1] + \arrow["{R^{*}}", dashed, from=1-3, to=5-3] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=5-1] + \arrow[dashed, from=5-1, to=5-3] +\end{tikzcd} +~~~ + +We can then apply strong commutativity to fill the upper square. + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1'} && {z'} \\ + \\ + {y_1} && \bullet + \arrow["R"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=5-1] + \arrow["{R{*}}", from=1-3, to=3-3] + \arrow["{S^{=}}"', from=3-1, to=3-3] + \arrow[dashed, from=3-3, to=5-3] + \arrow[dashed, from=5-1, to=5-3] + \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] +\end{tikzcd} +~~~ + +We now perform induction on the $S^{=}$. If it is the reflexive path, +then we have the following situation: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1'} \\ + \\ + {y_1} + \arrow["R"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=5-1] + \arrow["{R^{*}}", from=1-3, to=3-1] +\end{tikzcd} +~~~ + +Thus, we can use $y_1$ as our resolution. + +If the $S^{=}$ is not the empty path, then we have the following +diagram: + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1'} && {z'} \\ + \\ + {y_1} && \bullet + \arrow["R"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=5-1] + \arrow[dashed, from=5-1, to=5-3] + \arrow["{R{*}}", from=1-3, to=3-3] + \arrow["S"', from=3-1, to=3-3] + \arrow[dashed, from=3-3, to=5-3] + \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] +\end{tikzcd} +~~~ + +We can use our induction hypothesis to fill in the lower square, +completing the proof. + +~~~{.quiver} +\begin{tikzcd} + x && {y_2} \\ + \\ + {y_1'} && {z'} \\ + \\ + {y_1} && \bullet + \arrow["R"', from=1-1, to=3-1] + \arrow["S", from=1-1, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=5-1] + \arrow["{S^{*}}"', from=5-1, to=5-3] + \arrow["{R{*}}", from=1-3, to=3-3] + \arrow["S"', from=3-1, to=3-3] + \arrow["{R^{*}}", from=3-3, to=5-3] + \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] + \arrow["{I.H}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=3-1, to=5-3] +\end{tikzcd} +~~~ + +```agda +strongly-commutes→semi-commutes + : strongly-commutes-with R S → semi-commutes-with R S +strongly-commutes→semi-commutes {R = R} {S = S} strong-comm x↝₁*y1 x↝₂y2 = + Refl-trans-rec-chain + (λ x y1 → ∀ y2 → S x y2 → is-joinable (Refl-trans S) (Refl-trans R) y1 y2) + (λ {x} y2 x↝₂y2 → pure (y2 , [ x↝₂y2 ] , reflexive)) + (λ {x} {y1'} {y1} x↝₁y1' y1'↝₁*y1 ih y2 x↝₂y2 → do + z' , y1'↝₂=z , y2↝₁*z ← strong-comm x↝₁y1' x↝₂y2 + Refl-rec + (λ y1' z' + → Refl-trans R y2 z' → Refl-trans R y1' y1 + → (∀ y2 → S y1' y2 → is-joinable (Refl-trans S) (Refl-trans R) y1 y2) + → is-joinable (Refl-trans S) (Refl-trans R) y1 y2) + (λ {y1'} {z'} y1'↝₂z y2↝₁*z' y1'↝₁*y1 ih → do + z , y1↝₂*z , z'↝₁*z ← ih z' y1'↝₂z + pure (z , y1↝₂*z , transitive y2↝₁*z' z'↝₁*z)) + (λ y1' y2↝₁*y1' y1'↝₁*y1 _ → + pure (y1 , reflexive , transitive y2↝₁*y1' y1'↝₁*y1)) + hlevel! + y1'↝₂=z y2↝₁*z y1'↝₁*y1 ih) + hlevel! + x↝₁*y1 _ x↝₂y2 +``` + +Strong commutativity implies commutativity, as semi-commutativity +is equivalent to commutativity. + +```agda +strongly-commutes→commutes + : strongly-commutes-with R S → commutes-with R S +strongly-commutes→commutes strong-comm = + semi-commutes→commutes $ strongly-commutes→semi-commutes strong-comm +``` diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md new file mode 100644 index 000000000..b8b580f0a --- /dev/null +++ b/src/Rewriting/Confluent.lagda.md @@ -0,0 +1,896 @@ + + +```agda +module Rewriting.Confluent where +``` + +# Confluent Rewriting Systems + + + +Recall that [rewriting systems] may be non-deterministic, as multiple +rewrite rules can apply to a term $t$. This means that multiple +strategies of applying the rules may lead to different answers, which is +quite problematic if we want to use the rewriting system to simplify +expressions. It would be useful if we could prove *some* property of the +relation that would guarantee that this situation does not occur. + +[rewriting systems]: Rewriting.Base.html + +This leads us to the notion of **confluence**. We say a relation $\to$ +is confluent if for all pairs of reduction chains $a \to^{*} x$ +and $a \to^{*} y$, there exists some $z$ such that $x \to^{*} z$ +and $y \to^{*} z$, as in the following diagram. + +~~~{.quiver} +\begin{tikzcd} + a && y \\ + \\ + x && {\exists z} + \arrow["{*}"{description}, from=1-1, to=3-1] + \arrow["{*}"{description}, dashed, from=3-1, to=3-3] + \arrow["{*}"{description}, dashed, from=1-3, to=3-3] + \arrow["{*}"{description}, from=1-1, to=1-3] +\end{tikzcd} +~~~ + +```agda +is-confluent : (A → A → Type ℓ) → Type _ +is-confluent {A = A} R = + commutes-with R R +``` + +Note that this does *not* mean that all rewriting sequences terminate +regardless of strategy. For instance, consider the following rewriting +system: + +~~~{.quiver} +\begin{tikzcd} + \bullet & \bullet & \bullet & \cdots \\ + \\ + \bullet + \arrow[from=1-1, to=3-1] + \arrow[from=1-2, to=3-1] + \arrow[from=1-3, to=3-1] + \arrow[from=1-2, to=1-3] + \arrow[from=1-1, to=1-2] + \arrow[from=1-4, to=3-1] + \arrow[from=1-3, to=1-4] +\end{tikzcd} +~~~ + +There is an infinitely long sequence of rewrites extending to the right, +so a bad strategy will never terminate. However, we can always reconcile +diverging paths by rewriting to the term at the bottom of the diagram. + + + +Before getting into the more complicated properties of confluence, +we should get some minor lemmas out of the way. First, if $R^{*}$ +is equivalent to $S^{*}$ and $R^{*}$ is confluent, then so is $S^{*}$. +This follows directly from properties of resolutions. + +```agda +refl-trans-clo-equiv+confluent→confluent + : Refl-trans R ≃r Refl-trans S + → is-confluent R → is-confluent S +refl-trans-clo-equiv+confluent→confluent eqv R-conf {x} {y} {z} = + resolvable-⊆ + (Equiv.from (eqv {x} {y})) (Equiv.from (eqv {x} {z})) + (Equiv.to eqv) (Equiv.to eqv) + R-conf {x} {y} {z} +``` + +If a rewrite system on a set is confluent, then every element of $A$ +has at most one normal form. + +To show this, assume that $y$ and $z$ are both normal forms of $x$. +This gives us the following fork: + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z + \arrow["{*}"', from=1-2, to=2-1] + \arrow["{*}", from=1-2, to=2-3] +\end{tikzcd} +~~~ + +We can apply confluence to obtain a wedge $y \to^{*} w \leftarrow^{*} z$. + +~~~{.quiver} +\begin{tikzcd} + & x \\ + y && z \\ + & w + \arrow["{*}"', from=1-2, to=2-1] + \arrow["{*}", from=1-2, to=2-3] + \arrow["{*}"', from=2-1, to=3-2] + \arrow["{*}", from=2-3, to=3-2] + \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-2, to=3-2] +\end{tikzcd} +~~~ + +Both $y$ and $z$ are normal forms, so this gives us a pair of paths $y = w$ and +$z = w$, which completes the proof. + +```agda +confluent→unique-normal-forms + : ∀ {R : Rel A A ℓ} + → is-set A + → is-confluent R + → ∀ x → is-prop (Normal-form R x) +confluent→unique-normal-forms {R = R} A-set conf x y-nf z-nf = + ∥-∥-rec (Normal-form-is-hlevel 0 A-set y-nf z-nf) + (λ where + (w , y↝w , z↝w) → + Normal-form-path y-nf z-nf + (normal-forms+wedge→path A-set + (y-nf .has-normal-form) (z-nf .has-normal-form) + y↝w z↝w)) + (conf (y-nf .reduces) (z-nf .reduces)) +``` + + + +If $\to$ is a confluent relation and $x \to^{*} w \leftarrow^{*} y$, +then $y$ has a normal form if and only if $x$ does. + +To see this, note that we have the following pair of reductions +out of $x$: + +~~~{.quiver} +\begin{tikzcd} + x && w && y \\ + \\ + {x \downarrow} + \arrow["{*}", from=1-1, to=1-3] + \arrow["{*}"', from=1-1, to=3-1] + \arrow["{*}"', from=1-5, to=1-3] +\end{tikzcd} +~~~ + +We can use confluence to fill in the left-hand square: + +~~~{.quiver} +\begin{tikzcd} + x && w && y \\ + \\ + {x \downarrow} && {w'} + \arrow["{*}", from=1-1, to=1-3] + \arrow["{*}"', from=1-1, to=3-1] + \arrow["{*}"', from=1-5, to=1-3] + \arrow[from=1-3, to=3-3] + \arrow[from=3-1, to=3-3] + \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3] +\end{tikzcd} +~~~ + +Note that $x \downarrow$ and $y$ both reduce to the same value; this +means that $y$ reduces to $x \downarrow$, as $x \downarrow$ is a normal +form. + +```agda +confluent+wedge+normal-form→normal-form + : ∀ {x y w} + → is-confluent R + → Refl-trans R x w → Refl-trans R y w + → Normal-form R x → Normal-form R y +confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .nf = + x↓ .nf +confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .reduces = + ∥-∥-rec! + (λ where + (w' , x↓↝w' , w↝w') → + normal-form+reduces→reduces (x↓ .has-normal-form) + x↓↝w' (transitive y↝w w↝w')) + (conf (x↓ .reduces) x↝w) +confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .has-normal-form = + x↓ .has-normal-form +``` + +## The Church-Rosser Property + +A rewriting system $\to$ yields an equivalence relation on terms via +the [reflexive symmetric transitive closure] of $\to$. This leads to +a variant of confluence known as the **Church-Rosser Property**, which +requires a $z$ for every pair of equivalent terms $x$ and $y$ such that +$x \to^{*} z$ and $y \to^{*} z$. + +[reflexive symmetric transitive closure]: Data.Rel.Closure.ReflexiveSymmetricTransitive.html + +~~~{.quiver} +\begin{tikzcd} + x && y \\ + & z + \arrow["{*}"{description}, dashed, from=1-1, to=2-2] + \arrow["{*}"{description}, dashed, from=1-3, to=2-2] + \arrow["{*}"{description}, tail reversed, from=1-1, to=1-3] +\end{tikzcd} +~~~ + +```agda +has-church-rosser : (A → A → Type ℓ) → Type _ +has-church-rosser {A = A} R = + ∀ {x y} → Refl-sym-trans R x y + → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z) +``` + +At first glance, this seems like a stronger condition than confluence, +as Church-Rosser also gives us diamonds of the following shape: + +~~~{.quiver} +\begin{tikzcd} + a && y \\ + \\ + x && {\exists z} + \arrow["{*}"{description}, from=3-1, to=1-1] + \arrow["{*}"{description}', dashed, from=3-1, to=3-3] + \arrow["{*}"{description}, dashed, from=1-3, to=3-3] + \arrow["{*}"{description}, from=1-3, to=1-1] +\end{tikzcd} +~~~ + +Somewhat surprisingly, it turns out that the two conditions are equivalent! +Showing that Church-Rosser implies confluence is rather easy: if we +have two reduction sequences $a \to^{*} x$ and $a \to^{*} y$, +we can invert one side to get an equivalence in the reflexive symmetric +transitive closure, and then invoke Church-Rosser to get the desired +pair of reductions. + +```agda +church-rosser→confluent : has-church-rosser R → is-confluent R +church-rosser→confluent church-rosser a→*x a→*y = + church-rosser $ + transitive + (symmetric (refl-trans⊆refl-sym-trans a→*x)) + (refl-trans⊆refl-sym-trans a→*y) +``` + +The converse is much more tricky, and requires introducing an intermediate +notion of **semi-confluence**, which yields solutions to diamonds of the +following form. + +~~~{.quiver} +\begin{tikzcd} + a && y \\ + \\ + x && {\exists z} + \arrow["{*}"{description}, from=1-1, to=3-1] + \arrow["{*}"{description}', dashed, from=3-1, to=3-3] + \arrow["{*}"{description}, dashed, from=1-3, to=3-3] + \arrow[from=1-1, to=1-3] +\end{tikzcd} +~~~ + +```agda +is-semi-confluent : (A → A → Type ℓ) → Type _ +is-semi-confluent {A = A} R = + semi-commutes-with R R +``` + +Confluence obviously implies semi-confluence. + +```agda +confluent→semiconfluent : is-confluent R → is-semi-confluent R +confluent→semiconfluent conf a→*x a→y = conf a→*x [ a→y ] +``` + +Furthermore, semi-confluence implies Church-Rosser. Let $\to$ be a +semi-confluent rewriting system, and let $x \leftrightarrow^{*} y$ be a +pair of convertible elements. We proceed by inducting over the reduction +chain $x \leftrightarrow^{*} y$. If the chain is empty, then we can +form the trivial diamond, and we are done. + +If we have a reduction chain $x \to x' \leftrightarrow^{*} y$, then +can perform induction on the $x' \leftrightarrow^{*} y$ to obtain +a $v$ with $x' \to^{*} v$ and $y \to^{*} v$, as in the following diagram. + +~~~{.quiver} +\begin{tikzcd} + x && {x'} && y \\ + \\ + && v + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, from=1-5, to=3-3] + \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5] + \arrow[from=1-1, to=1-3] +\end{tikzcd} +~~~ + +Let's re-arrange the diagram a bit, adding in a trivial reduction +of $v$ to $v$. + +~~~{.quiver} +\begin{tikzcd} + {x'} && x && {x'} && y \\ + \\ + && v && v + \arrow["{*}"{description}, from=1-5, to=3-5] + \arrow["{*}"{description}, from=1-7, to=3-5] + \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7] + \arrow[from=1-3, to=1-5] + \arrow[from=1-3, to=1-1] + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, from=3-5, to=3-3] +\end{tikzcd} +~~~ + +We can then apply semi-confluence to the pair $x \to x'$ and $x \to^{*} v$ +to get some $w$ with reductions $x' \to^{*} w$ and $v \to^{*} w$. + +~~~{.quiver} +\begin{tikzcd} + {x'} && x && {x'} && y \\ + \\ + w && v && v + \arrow["{*}"{description}, from=1-5, to=3-5] + \arrow["{*}"{description}, from=1-7, to=3-5] + \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7] + \arrow[from=1-3, to=1-5] + \arrow[from=1-3, to=1-1] + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, from=3-5, to=3-3] + \arrow["{*}"{description}, from=3-3, to=3-1] + \arrow["{*}"{description}, from=1-1, to=3-1] +\end{tikzcd} +~~~ + +This yields a pair of reductions $x \to^{*} w$ and $y \to^{*} w$, +completing this case. + +~~~{.quiver} +\begin{tikzcd} + {x'} && x && {x'} && y \\ + \\ + w && v && v + \arrow["{*}"{description}, from=1-5, to=3-5] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-7, to=3-5] + \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7] + \arrow[from=1-3, to=1-5] + \arrow[color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1] + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=3-3] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-3, to=3-1] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=3-1] +\end{tikzcd} +~~~ + +Finally, suppose we have a reduction chain $x' \to x \leftrightarrow^{*} y$. +We can perform induction on the $x \leftrightarrow^{*} y$ to obtain +a $v$ with $x \to^{*} v$ and $y \to^{*} v$, as in the following diagram. + +~~~{.quiver} +\begin{tikzcd} + x && {x'} && y \\ + \\ + && v + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, from=1-5, to=3-3] + \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5] + \arrow[from=1-3, to=1-1] +\end{tikzcd} +~~~ + +We can then apply semi-confluence to the reduction pair $x \to x'$ and +$x \to^{*} v$, yielding the following diagram. + +~~~{.quiver} +\begin{tikzcd} + x && {x'} && y \\ + \\ + w && v + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, from=1-5, to=3-3] + \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5] + \arrow[from=1-3, to=1-1] + \arrow["{*}"{description}, from=1-1, to=3-1] + \arrow["{*}"{description}, from=3-3, to=3-1] +\end{tikzcd} +~~~ + +We can then chase some arrows to determine that we have constructed +a pair of reductions $x \to^{*} w$ and $y \to^{*} w$, completing the proof. + +~~~{.quiver} +\begin{tikzcd} + x && {x'} && y \\ + \\ + w && v + \arrow["{*}"{description}, from=1-3, to=3-3] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-5, to=3-3] + \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5] + \arrow[color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=3-1] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-3, to=3-1] +\end{tikzcd} +~~~ + +```agda +semiconfluent→church-rosser : is-semi-confluent R → has-church-rosser R +semiconfluent→church-rosser {R = R} semiconf x↔y = + Refl-sym-trans-rec-chain + (λ x y → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z)) + (inc (_ , reflexive , reflexive)) + (λ {x} {x'} {y} x→x' _ x'→*v*←y → do + v , x'→*v , y→*v ← x'→*v*←y + w , v→*w , x'→*w ← semiconf (transitive [ x→x' ] x'→*v) x→x' + pure (w , transitive [ x→x' ] x'→*w , transitive y→*v v→*w)) + (λ {x} {x'} {y} x'→x _ x'→*v*←y → do + v , x'→*v , y→*v ← x'→*v*←y + w , v→*w , x→*w ← semiconf x'→*v x'→x + pure (w , x→*w , transitive y→*v v→*w)) + squash + x↔y +``` + +We can use these 3 proofs to show that confluence, Church-Rosser, and +semi-confluence are equivalent. + +```agda +semiconfluent→confluent : is-semi-confluent R → is-confluent R +semiconfluent→confluent conf = + church-rosser→confluent (semiconfluent→church-rosser conf) + +confluent→church-rosser : is-confluent R → has-church-rosser R +confluent→church-rosser conf = + semiconfluent→church-rosser (confluent→semiconfluent conf) + +church-rosser→semiconfluent : has-church-rosser R → is-semi-confluent R +church-rosser→semiconfluent church-rosser = + confluent→semiconfluent (church-rosser→confluent church-rosser) +``` + +This theorem has some very useful consequences; first, if $R$ is +confluent and $x$ and $y$ are convertible, then $x$ reduces to $y$ +if $y$ is in normal form. + +To see this, note that Church-rosser implies that gives us a $w$ such +that $x \to^{*} w$ and $y \to^{*} w$. We can then perform induction +on the $y \to^{*} w$; if it is empty, then we have $y = w$, and thus +$x \to^{*} y$. If it is non-empty, then we have a contradiction, as +$y$ is a normal form. + +```agda +confluent+convertible→reduces-to-normal-form + : ∀ {x y} + → is-confluent R + → Refl-sym-trans R x y + → is-normal-form R y + → Refl-trans R x y +confluent+convertible→reduces-to-normal-form {R = R} {x = x} {y = y} conf x↔y y-nf = + ∥-∥-rec! + (λ where + (w , x↝w , y↝w) → + Refl-trans-rec-chain + (λ y w → is-normal-form R y → Refl-trans R x w → Refl-trans R x y) + (λ _ x↝y → x↝y) + (λ y↝z _ _ y-nf _ → absurd (y-nf (_ , y↝z))) + hlevel! + y↝w y-nf x↝w) + (confluent→church-rosser conf x↔y) +``` + +Furthermore, if $R$ is a confluent relation on a set, and $x y : A$ +are convertible normal forms, then $x = y$. This follows from +`normal-forms+wedge→path`{.Agda} and confluence. + +```agda +confluent+convertible→unique-normal-form + : ∀ {R : Rel A A ℓ} {x y} + → is-set A + → is-confluent R + → Refl-sym-trans R x y + → is-normal-form R x → is-normal-form R y + → x ≡ y +confluent+convertible→unique-normal-form set conf x↔y x-nf y-nf = + ∥-∥-rec (set _ _) + (λ where + (w , x↝w , y↝w) → + normal-forms+wedge→path set x-nf y-nf x↝w y↝w) + (confluent→church-rosser conf x↔y) +``` + +We can also show that if $R$ is a confluent relation on a set, and +$x$ and $y$ are convertible, then the their types of normal forms are +equivalent. + +```agda +confluent+convertible→normal-form-equiv + : ∀ {R : Rel A A ℓ} {x y} + → is-set A + → is-confluent R + → Refl-sym-trans R x y + → Normal-form R x ≃ Normal-form R y +confluent+convertible→normal-form-equiv {R = R} {x = x} {y = y} set conf x↔y = + ∥-∥-rec! + (λ where + (w , x↝w , y↝w) → + prop-ext! + (confluent+wedge+normal-form→normal-form conf x↝w y↝w) + (confluent+wedge+normal-form→normal-form conf y↝w x↝w)) + (confluent→church-rosser conf x↔y) + where + instance + _ : ∀ {x} {n} → H-Level (Normal-form R x) (suc n) + _ = H-Level-confluent-normal-form set conf +``` + +## Local Confluence and Newman's Lemma + +Proving confluence can be difficult, as it requires looking at +forks of arbitrary depth. It is much easier to only consider single-step +forks, which leads to a notion of **local confluence**. + +```agda +is-locally-confluent : (A → A → Type ℓ) → Type _ +is-locally-confluent {A = A} R = + ∀ {a x y} → R a x → R a y + → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z) +``` + +Note that local confluence is a weaker property than confluence. As +a concrete example, consider the following rewrite system: + +~~~{.quiver} +\begin{tikzcd} + w & x && y & z \\ + \\ + \\ + && {} + \arrow[curve={height=-12pt}, from=1-2, to=1-4] + \arrow[curve={height=-12pt}, from=1-4, to=1-2] + \arrow[from=1-2, to=1-1] + \arrow[from=1-4, to=1-5] +\end{tikzcd} +~~~ + +There are two single-step forks in this system: +$w \leftarrow x \rightarrow y$ and $x \leftarrow y \to z$. Both of +these are locally confluent: We can reduce both to $w$ for the first fork, +and $z$ for the second. However, it is *not* confluent: there is a fork +$w \leftarrow^{*} x \to^{*} z$ that cannot be reconciled. + +However, if the rewrite system is [strongly normalising], then local +confluence implies confluence. + +[strongly normalising]: Rewriting.StronglyNormalising.html + +Let $\to$ be a strongly normalising, locally confluent rewriting system. +Consider some fork $x \leftarrow^{*} a \to^{*} y$. As $\to$ is strongly +normalizing, we can perform well-founded induction, attempting to +produce a common reduct for both sides of the fork. + +If either side of tthe fork is a zero-length chain, then we can use the +trivial joins $a \to{*} x \leftarrow^{*} a$ and $a \to{*} y +\leftarrow^{*} a$, resp. If both chains are non-trivial, we end up with +the following diagram: + +~~~{.quiver} +\begin{tikzcd} + && a \\ + & {x'} && {y'} \\ + x &&&& y + \arrow[from=1-3, to=2-2] + \arrow[from=1-3, to=2-4] + \arrow["{*}"{description}, from=2-2, to=3-1] + \arrow["{*}"{description}, from=2-4, to=3-5] +\end{tikzcd} +~~~ + +We can then apply local confluence to $a \to x'$ and $a \to y'$. + +~~~{.quiver} +\begin{tikzcd} + && a \\ + & {x'} && {y'} \\ + x && u && y + \arrow[from=1-3, to=2-2] + \arrow[from=1-3, to=2-4] + \arrow["{*}"{description}, from=2-2, to=3-1] + \arrow["{*}"{description}, from=2-4, to=3-5] + \arrow["{*}"{description}, from=2-2, to=3-3] + \arrow["{*}"{description}, from=2-4, to=3-3] +\end{tikzcd} +~~~ + +Next, we can recurse on $x' \to^{*} x$ and $x' \to^{*} u$. + +~~~{.quiver .tall-2} +\begin{tikzcd} + && a \\ + & {x'} && {y'} \\ + x && u && y \\ + & v + \arrow[from=1-3, to=2-2] + \arrow[from=1-3, to=2-4] + \arrow["{*}"{description}, from=2-2, to=3-1] + \arrow["{*}"{description}, from=2-4, to=3-5] + \arrow["{*}"{description}, from=2-2, to=3-3] + \arrow["{*}"{description}, from=2-4, to=3-3] + \arrow["{*}"{description}, from=3-1, to=4-2] + \arrow["{*}"{description}, from=3-3, to=4-2] +\end{tikzcd} +~~~ + +We can recurse yet again on $y' \to^{*} v$ and $y' \to^{*} y$. + +~~~{.quiver .tall-2} +\begin{tikzcd} + && a \\ + & {x'} && {y'} \\ + x && u && y \\ + & v \\ + && w + \arrow[from=1-3, to=2-2] + \arrow[from=1-3, to=2-4] + \arrow["{*}"{description}, from=2-2, to=3-1] + \arrow["{*}"{description}, from=2-4, to=3-5] + \arrow["{*}"{description}, from=2-2, to=3-3] + \arrow["{*}"{description}, from=2-4, to=3-3] + \arrow["{*}"{description}, from=3-1, to=4-2] + \arrow["{*}"{description}, from=3-3, to=4-2] + \arrow["{*}"{description}, from=3-5, to=5-3] + \arrow["{*}"{description}, from=4-2, to=5-3] +\end{tikzcd} +~~~ + +The bottom half of the square yields the desired pair of reductions, +finishing the proof. + +~~~{.quiver .tall-2} +\begin{tikzcd} + && a \\ + & {x'} && {y'} \\ + x && u && y \\ + & v \\ + && w + \arrow[from=1-3, to=2-2] + \arrow[from=1-3, to=2-4] + \arrow["{*}"{description}, from=2-2, to=3-1] + \arrow["{*}"{description}, from=2-4, to=3-5] + \arrow["{*}"{description}, from=2-2, to=3-3] + \arrow["{*}"{description}, from=2-4, to=3-3] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-1, to=4-2] + \arrow["{*}"{description}, from=3-3, to=4-2] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=5-3] + \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=4-2, to=5-3] +\end{tikzcd} +~~~ + +```agda +strong-normalising+locally-confluent→confluent + : is-strongly-normalising R → is-locally-confluent R + → is-confluent R +strong-normalising+locally-confluent→confluent + {R = R} sn local-conf {a} {x} {z} a→*x a→*y = + Wf-induction _ sn + (λ a → + ∀ {x y} → Refl-trans R a x → Refl-trans R a y + → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z)) + (λ a ih {x} {y} a→*x a→*y → + Refl-trans-case-fork + (λ a x y + → (∀ a' → Trans R a a' + → ∀ {x y} → Refl-trans R a' x → Refl-trans R a' y + → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z)) + → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z)) + (λ a→*y _ → inc (_ , a→*y , reflexive)) + (λ a→*x _ → inc (_ , reflexive , a→*x)) + (λ a→x' x'→*x a→y' y'→*y ih → do + u , x'→*u , y'→*u ← local-conf a→x' a→y' + v , x→*v , u→*v ← ih _ [ a→x' ] x'→*x x'→*u + w , v→*w , y→*w ← ih _ [ a→y' ] (transitive y'→*u u→*v) y'→*y + pure (w , transitive x→*v v→*w , y→*w)) + hlevel! + a→*x a→*y ih) + a a→*x a→*y +``` + +## The Commutative Union Lemma + +Confluence proofs can be very fiddly, so it would be useful to be able to +modularise the proofs somewhat. Ideally, we would be able to split +a rewriting system $R$ into a union $S \cup T$, and then prove confluence +of $S$ and $T$ separately. This approach is too naïve, but can be repaired +by requiring that $S$ and $T$ [commute]. + +[commute]: Rewriting.Commute.html + +The proof of this fact requires some machinery. We say that a rewrite +system is **strongly confluent** if we can resolve squares of shape (1), +and that it has the **diamond property** if we can resolve squares of shape +(2). + +~~~{.quiver} +\begin{tikzcd} + & x &&&& x \\ + y && z && y && z \\ + & {\exists w} &&&& {\exists w} \\ + & {(1)} &&&& {(2)} + \arrow[from=1-2, to=2-1] + \arrow[from=1-2, to=2-3] + \arrow[dashed, from=2-5, to=3-6] + \arrow[dashed, from=2-7, to=3-6] + \arrow[from=1-6, to=2-5] + \arrow[from=1-6, to=2-7] + \arrow["{*}", dashed, from=2-3, to=3-2] + \arrow["{=}"', dashed, from=2-1, to=3-2] +\end{tikzcd} +~~~ + +```agda +has-diamond : (R : Rel A A ℓ) → Type _ +has-diamond R = is-resolvable R R R R + +is-strongly-confluent : (R : Rel A A ℓ) → Type _ +is-strongly-confluent R = strongly-commutes-with R R +``` + +The diamond property implies strong confluence, which in turn implies +confluence. + +```agda +diamond→strongly-confluent : has-diamond R → is-strongly-confluent R +diamond→strongly-confluent diamond x↝y x↝z = do + w , y↝w , x↝w ← diamond x↝y x↝z + pure (w , [ y↝w ] , [ x↝w ]) + +strongly-confluent→confluent : is-strongly-confluent R → is-confluent R +strongly-confluent→confluent = strongly-commutes→commutes + +diamond→confluent : has-diamond R → is-confluent R +diamond→confluent = strongly-confluent→confluent ∘ diamond→strongly-confluent +``` + +With that bit of machinery out of the way, we can proceed with the +proof. Recall that if the reflexive-transitive closures of two +relations are equivalent, then we can transfer confluence across the +equivalence. Furthermore, the reflexive transitive-closure of $R \cup S$ +is equivalent to the reflexive-transitive closure of $S^{*} \circ +R^{*}$, so it suffices to show that $S^{*} \circ R^{*}$ is confluent. + +We shall do so by establishing that $S^{*} \circ R^{*}$ has the diamond +property. Doing so requires filling the following diagram: + +~~~{.quiver} +\begin{tikzcd} + x & {z'} & z \\ + {y'} && \bullet \\ + y & \bullet & \bullet + \arrow["{R^{*}}"', from=1-1, to=2-1] + \arrow["{S^{*}}"', from=2-1, to=3-1] + \arrow["{R^{*}}", from=1-1, to=1-2] + \arrow["{S^{*}}", from=1-2, to=1-3] + \arrow["{R^{*}}"', dashed, from=3-1, to=3-2] + \arrow["{S^{*}}"', dashed, from=3-2, to=3-3] + \arrow["{R^{*}}", dashed, from=1-3, to=2-3] + \arrow["{S^{*}}", dashed, from=2-3, to=3-3] +\end{tikzcd} +~~~ + +We can use confluence of $R^{*}$ to fill in the upper-left square. + +~~~{.quiver} +\begin{tikzcd} + x & {z'} & z \\ + {y'} & a & \bullet \\ + y & \bullet & \bullet + \arrow["{R^{*}}"', from=1-1, to=2-1] + \arrow["{S^{*}}"', from=2-1, to=3-1] + \arrow["{R^{*}}", from=1-1, to=1-2] + \arrow["{S^{*}}", from=1-2, to=1-3] + \arrow["{R^{*}}"', dashed, from=3-1, to=3-2] + \arrow["{S^{*}}"', dashed, from=3-2, to=3-3] + \arrow["{R^{*}}", dashed, from=1-3, to=2-3] + \arrow["{S^{*}}", dashed, from=2-3, to=3-3] + \arrow["{R^{*}}"', from=2-1, to=2-2] + \arrow["{R^{*}}", from=1-2, to=2-2] + \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=2-2] +\end{tikzcd} +~~~ + +We can then use commutativity of $R$ and $S$ to fill in the upper-right +and lower-left squares. + +~~~{.quiver} +\begin{tikzcd} + x & {z'} & z \\ + {y'} & a & c \\ + y & b & \bullet + \arrow["{R^{*}}"', from=1-1, to=2-1] + \arrow["{S^{*}}"', from=2-1, to=3-1] + \arrow["{R^{*}}", from=1-1, to=1-2] + \arrow["{S^{*}}", from=1-2, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=3-2] + \arrow["{S^{*}}"', dashed, from=3-2, to=3-3] + \arrow["{R^{*}}", from=1-3, to=2-3] + \arrow["{S^{*}}", dashed, from=2-3, to=3-3] + \arrow["{R^{*}}", from=2-1, to=2-2] + \arrow["{R^{*}}"', from=1-2, to=2-2] + \arrow["{S^{*}}", from=2-2, to=3-2] + \arrow["{S^{*}}"', from=2-2, to=2-3] + \arrow["Comm"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=2-1, to=3-2] + \arrow["Comm"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-2, to=2-3] +\end{tikzcd} +~~~ + +Finally, we can use confluence of $S$ to fill in the lower-right square, +finishing the proof. + +~~~{.quiver} +\begin{tikzcd} + x & {z'} & z \\ + {y'} & a & c \\ + y & b & w + \arrow["{R^{*}}"', from=1-1, to=2-1] + \arrow["{S^{*}}"', from=2-1, to=3-1] + \arrow["{R^{*}}", from=1-1, to=1-2] + \arrow["{S^{*}}", from=1-2, to=1-3] + \arrow["{R^{*}}"', from=3-1, to=3-2] + \arrow["{S^{*}}"', from=3-2, to=3-3] + \arrow["{R^{*}}", from=1-3, to=2-3] + \arrow["{S^{*}}", from=2-3, to=3-3] + \arrow["{R^{*}}", from=2-1, to=2-2] + \arrow["{R^{*}}"', from=1-2, to=2-2] + \arrow["{S^{*}}"', from=2-2, to=3-2] + \arrow["{S^{*}}", from=2-2, to=2-3] + \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=2-2, to=3-3] +\end{tikzcd} +~~~ + +```agda +commutes+confluent→union-confluent + : commutes-with R S + → is-confluent R → is-confluent S + → is-confluent (R ∪r S) +commutes+confluent→union-confluent {R = R} {S = S} comm R-conf S-conf = + refl-trans-clo-equiv+confluent→confluent + refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo + (diamond→confluent S*∘R*-diamond) + where + S*∘R*-diamond : has-diamond (Refl-trans S ∘r Refl-trans R) + S*∘R*-diamond {x} {y} {z} x↝*y x↝*z = do + y' , x↝₁y' , y'↝₂y ← x↝*y + z' , x↝₁z' , z'↝₂z ← x↝*z + a , y'↝₁a , z'↝₁a ← R-conf x↝₁y' x↝₁z' + b , a↝₂b , y↝₁b ← comm y'↝₁a y'↝₂y + c , a↝₂c , z↝₁c ← comm z'↝₁a z'↝₂z + w , b↝₂w , c↝₂w ← S-conf a↝₂b a↝₂c + pure (w , pure (b , y↝₁b , b↝₂w) , pure (c , z↝₁c , c↝₂w)) +``` diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md new file mode 100644 index 000000000..58d614ff2 --- /dev/null +++ b/src/Rewriting/StronglyNormalising.lagda.md @@ -0,0 +1,81 @@ + + +```agda +module Rewriting.StronglyNormalising where +``` + + + +# Strongly Normalising Rewrite Systems + +An abstract rewriting system is **strongly normalising** if its +[transitive closure] is a [well-founded relation]. + +[transitive closure]: Data.Rel.Closure.Transitive.html +[well-founded relation]: Data.Wellfounded.Base.html + +```agda +is-strongly-normalising : (A → A → Type ℓ) → Type _ +is-strongly-normalising _↝_ = Wf (λ x y → Trans _↝_ y x) +``` + +This definition is classically equivalent to the non-existence of infinite +reduction sequences. However, strong normalisation is more useful +constructively, as we can use it to perform induction. However, the +latter notion is still useful; we call such rewrite systems **terminating**. + +```agda +is-terminating : (A → A → Type ℓ) → Type _ +is-terminating {A = A} _↝_ = + ¬ (∃[ aₙ ∈ (Nat → A) ] (∀ n → Trans _↝_ (aₙ n) (aₙ (suc n)))) +``` + +If a rewrite system is strongly normalising, then it is terminating. +Aiming for a contradiction, let us assume that we have some infinite +chain $a_0 \leadsto a_1 \leadsto \cdots$ of reductions. We then perform +well-founded induction where our motive states that, for all $n$, there +is no reduction $a \leadsto^{+} a_{n+1}$. The induction step proceeds +by recurring on $a_{n+1}$, which steps to $a_{n+2}$. This has the effect +of following the infinite chain of reductions, leading to a divergence. +We can extract the proof of false by applying this induction to the +step $a_0 \leadsto a_1$ of the sequence. + +```agda +strongly-normalising→terminating : is-strongly-normalising _↝_ → is-terminating _↝_ +strongly-normalising→terminating {_↝_ = _↝_} sn ∥chain∥ = + ∥-∥-proj! $ do + (aₙ , step) ← ∥chain∥ + inc $ Wf-induction _ sn + (λ a → ∀ n → ¬ Trans _↝_ a (aₙ (suc n))) + (λ a ih n aᵢ↝aₙ₊₁ → ih (aₙ (suc n)) aᵢ↝aₙ₊₁ (suc n) (step (suc n))) + (aₙ 0) 0 (step zero) +``` + + + +We can use the prior fact to show that strongly normalising rewrite +systems contain no loops, by using the constant sequence $a \leadsto a$ +as our infinite chain. + +```agda +strongly-normalising→acyclic + : ∀ {A : Type ℓ} {_↝_ : A → A → Type ℓ'} + → is-strongly-normalising _↝_ + → ¬ (∃[ a ∈ A ] (Trans _↝_ a a)) +strongly-normalising→acyclic sn ∥loop∥ = + strongly-normalising→terminating sn $ + ∥-∥-map (λ (a , a↝a) → (λ _ → a) , λ n → a↝a) ∥loop∥ +```