Skip to content

Instantly share code, notes, and snippets.

@twanvl

twanvl/2013-12-20-confluence-problem-v2.agda

Created December 20, 2013 22:35
Show Gist options
  • Save twanvl/8062712 to your computer and use it in GitHub Desktop.
Save twanvl/8062712 to your computer and use it in GitHub Desktop.
Download ZIP
New proof of confluence thing (see https://gist.github.com/twanvl/7453495), which will hopefully also extend to lambda calculus.
Raw
2013-12-20-confluence-problem-v2.agda
module 2013-12-20-confluence-problem-v2 where
open import 2013-12-20-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP
open import Relation.Nullary
open import Induction.WellFounded
open import Induction.Nat
open ≡-Reasoning
open import Algebra.Structures
open IsDistributiveLattice isDistributiveLattice using () renaming (∧-comm to ⊔-comm)
open IsCommutativeSemiring isCommutativeSemiring using (+-comm;+-assoc)
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)
--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------
n≤m⊔n : ∀ m n → n ≤ m ⊔ n
n≤m⊔n m n rewrite ⊔-comm m n = m≤m⊔n n m
⊔≤ : ∀ {m n o} → m ≤ o → n ≤ o → m ⊔ n ≤ o
⊔≤ z≤n n≤o = n≤o
⊔≤ (s≤s m≤o) z≤n = s≤s m≤o
⊔≤ (s≤s m≤o) (s≤s n≤o) = s≤s (⊔≤ m≤o n≤o)
≤⊔≤ : ∀ {a b c d} → a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
≤⊔≤ {a} {b} {c} {d} a≤b c≤d = ⊔≤ (≤-trans a≤b (m≤m⊔n b d)) (≤-trans c≤d (n≤m⊔n b d))
--------------------------------------------------------------------------------------------------
-- The problem
--------------------------------------------------------------------------------------------------
data V : Set where
`A : V
`C : V → V
`D : V → V → V
_==_ : Rel₀ V
data _⟶_ : Rel₀ V where
aca : `A ⟶ `C `A
d₁ : ∀ {a b} → (eq : a == b) → `D a b ⟶ a
d₂ : ∀ {a b} → (eq : a == b) → `D a b ⟶ b
-- Do we also have these? It was not entirely clear from the paper.
-- But I assume so, since otherwise the relation is strongly normalizing and we could prove confluence that way
under-c : ∀ {a a'} → (x : a ⟶ a') → `C a ⟶ `C a'
under-d₁ : ∀ {a a' b} → (x : a ⟶ a') → `D a b ⟶ `D a' b
under-d₂ : ∀ {a b b'} → (y : b ⟶ b') → `D a b ⟶ `D a b'
_==_ = Star (Sym _⟶_)
-- we want to prove confluence of _⟶_
-- but to do that we need to expand _==_, which needs confluence
--------------------------------------------------------------------------------------------------
-- Inverse d step based solution
--------------------------------------------------------------------------------------------------
module InverseBased where
-- Step with inverse d reduction
-- this doesn't matter when it is used in a symmetric transitive closure
data IStep : Rel₀ V where
aca : IStep (`A) (`C `A)
d : ∀ {a} → IStep a (`D a a)
under-c : ∀ {a a'} → (x : IStep a a') → IStep (`C a) (`C a')
under-d : ∀ {a b a' b'} → (x : IStep a a') → (y : IStep b b') → IStep (`D a b) (`D a' b')
ε : ∀ {a} → IStep a a
iunder-ds : ∀ {a b a' b'} → (x : StarSym IStep a a') → (y : StarSym IStep b b') → StarSym IStep (`D a b) (`D a' b')
iunder-ds {a} {b} {a'} {b'} xs ys =
StarSym.map (\x → under-d x ε) xs ◅◅
StarSym.map (\y → under-d ε y) ys
iconfluent : Confluent IStep
iconfluent ε u = u || ε
iconfluent x ε = ε || x
iconfluent x d = d || under-d x x
iconfluent d u = under-d u u || d
iconfluent aca aca = ε || ε
iconfluent (under-c x) (under-c u) = CR.map under-c (iconfluent x u)
iconfluent (under-d x y) (under-d u v) = CR.zip under-d (iconfluent x u) (iconfluent y v)
a-to-is : _⟶_ ⇒ StarSym IStep
as-to-is : StarSym _⟶_ ⇒ StarSym IStep
a-to-is aca = fwd aca ◅ ε
a-to-is (d₁ eq) = iunder-ds ε (StarSym.sym $ as-to-is eq) ◅◅ bwd d ◅ ε
a-to-is (d₂ eq) = iunder-ds (as-to-is eq) ε ◅◅ bwd d ◅ ε
a-to-is (under-c x) = StarSym.map under-c (a-to-is x)
a-to-is (under-d₁ x) = iunder-ds (a-to-is x) ε
a-to-is (under-d₂ x) = iunder-ds ε (a-to-is x)
--as-to-is = StarSym.concatMap a-to-is -- doesn't pass termination checker
as-to-is ε = ε
as-to-is (fwd x ◅ xs) = a-to-is x ◅◅ as-to-is xs
as-to-is (bwd x ◅ xs) = StarSym.sym (a-to-is x) ◅◅ as-to-is xs
i-to-as : IStep ⇒ StarSym _⟶_
i-to-as aca = fwd aca ◅ ε
i-to-as d = bwd (d₁ ε) ◅ ε
i-to-as (under-c x) = StarSym.map under-c (i-to-as x)
i-to-as (under-d x y) = StarSym.map under-d₁ (i-to-as x) ◅◅ StarSym.map under-d₂ (i-to-as y)
i-to-as ε = ε
-- We can use IStep as a condition for steps
-- note that we only need d₁
data BStep : Rel₀ V where
aca : BStep (`A) (`C `A)
d₁ : ∀ {a b} → StarSym IStep a b → BStep (`D a b) a
under-c : ∀ {a a'} → (x : BStep a a') → BStep (`C a) (`C a')
under-d : ∀ {a b a' b'} → (x : BStep a a') → (y : BStep b b') → BStep (`D a b) (`D a' b')
ε : ∀ {a} → BStep a a
bunder-ds : ∀ {a b a' b'} → (x : Star BStep a a') → (y : Star BStep b b') → Star BStep (`D a b) (`D a' b')
bunder-ds {a} {b} {a'} {b'} xs ys =
Star.map (\x → under-d {b = b} x ε) xs ◅◅
Star.map (\y → under-d {a = a'} ε y) ys
b-to-is : BStep ⇒ StarSym IStep
b-to-is aca = fwd aca ◅ ε
b-to-is (d₁ x) = StarSym.map (under-d ε) (StarSym.sym x) ◅◅ bwd d ◅ ε
b-to-is (under-c x) = StarSym.map under-c (b-to-is x)
b-to-is (under-d {b' = b'} x y) = iunder-ds (b-to-is x) (b-to-is y)
b-to-is ε = ε
bconfluent : Confluent BStep
bconfluent ε u = u || ε
bconfluent x ε = ε || x
bconfluent aca aca = ε || ε
bconfluent (under-c x) (under-c u) = CR.map under-c (bconfluent x u)
bconfluent (d₁ x) (d₁ u) = ε || ε
bconfluent (d₁ x) (under-d u v) = u || d₁ (StarSym.sym (b-to-is u) ◅◅ x ◅◅ b-to-is v)
bconfluent (under-d x y) (d₁ u) = d₁ (StarSym.sym (b-to-is x) ◅◅ u ◅◅ b-to-is y) || x
bconfluent (under-d x y) (under-d u v) = CR.zip under-d (bconfluent x u) (bconfluent y v)
i-to-bs : IStep ⇒ CommonReduct (Star BStep)
i-to-bs aca = aca ◅ ε || ε
i-to-bs d = ε || d₁ ε ◅ ε
i-to-bs (under-c x) with i-to-bs x
... | u || v = Star.map under-c u || Star.map under-c v
i-to-bs (under-d x y) with i-to-bs x | i-to-bs y
... | u || v | p || q = bunder-ds u p || bunder-ds v q
i-to-bs ε = ε || ε
is-to-bs : StarSym IStep ⇒ CommonReduct (Star BStep)
is-to-bs ε = ε || ε
is-to-bs (fwd ab ◅ bc) with i-to-bs ab | is-to-bs bc
... | ad || bd | be || ce with Confluent-Star bconfluent bd be
... | df || ef = ad ◅◅ df || ce ◅◅ ef
is-to-bs (bwd ba ◅ bc) with i-to-bs ba | is-to-bs bc
... | bd || ad | be || ce with Confluent-Star bconfluent bd be
... | df || ef = ad ◅◅ df || ce ◅◅ ef
b-to-as : BStep ⇒ Star _⟶_
b-to-as aca = aca ◅ ε
b-to-as (d₁ x) = d₁ (StarSym.concatMap i-to-as x) ◅ ε
b-to-as (under-c x) = Star.map under-c (b-to-as x)
b-to-as (under-d x y) = Star.map under-d₁ (b-to-as x) ◅◅ Star.map under-d₂ (b-to-as y)
b-to-as ε = ε
aconfluent : GlobalConfluent _⟶_
aconfluent ab ac with is-to-bs (Star.concatMap a-to-is ab) | is-to-bs (Star.concatMap a-to-is ac)
... | ad || bd | ae || ce with Confluent-Star bconfluent ad ae
... | df || ef = Star.concatMap b-to-as (bd ◅◅ df) || Star.concatMap b-to-as (ce ◅◅ ef)
Raw
2013-12-20-relations.agda
module 2013-12-20-relations where
open import Level hiding (zero;suc)
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
open import Data.Product using (∃)
open import Induction.WellFounded
--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------
Rel₀ : Set → Set₁
Rel₀ A = Rel A Level.zero
Arrow : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Arrow A B = A → B
Any : ∀ {a b r} {A : Set a} {B : Set b} → (A → Rel B r) → Rel B _
Any r u v = ∃ \x → r x u v
--------------------------------------------------------------------------------
-- Transitive closure
--------------------------------------------------------------------------------
module Star where
open import Data.Star public renaming (map to map'; fold to foldr)
map : ∀ {i j t u} {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u} →
{f : I → J} → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
map g xs = gmap _ g xs
concatMap : ∀ {i j t u}
{I : Set i} {J : Set j} {T : Rel I t} {U : Rel J u}
{f : I → J} → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
concatMap g xs = kleisliStar _ g xs
foldMap : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
{f : I → J} (P : Rel J p) →
Transitive P → Reflexive P → T =[ f ]⇒ P → Star T =[ f ]⇒ P
foldMap {f = f} P t r g = gfold f P (\a b → t (g a) b) r
fold : ∀ {a r} {A : Set a} {R : Rel A r} → {f : A → Set} → (R =[ f ]⇒ Arrow) → (Star R =[ f ]⇒ Arrow)
--fold {f = f} g = Data.Star.gfold f Arrow (\a b → b ∘ g a) id
fold {f = f} g = foldMap {f = f} Arrow (\f g x → g (f x)) id g
open Star public using (Star;_◅_;_◅◅_;ε;_⋆)
--------------------------------------------------------------------------------
-- Non-Reflexive Transitive closure
--------------------------------------------------------------------------------
module Plus where
data Plus {l r} {A : Set l} (R : Rel A r) (a : A) (c : A) : Set (l ⊔ r) where
_◅_ : ∀ {b} → R a b → Star R b c → Plus R a c
plus-acc : ∀ {l} {A : Set l} {R : Rel A l} {x} → Acc (flip R) x → Acc (flip (Plus R)) x
plus-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Plus R x y → Acc (flip (Plus R)) y
star-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Star R x y → Acc (flip (Plus R)) y
plus-acc a = acc (\_ → plus-acc' a)
plus-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
star-acc' a ε = plus-acc a
star-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
well-founded : ∀ {l} {A : Set l} {R : Rel A l} → Well-founded (flip R) → Well-founded (flip (Plus R))
well-founded wf = plus-acc ∘ wf
open Plus public using (Plus;_◅_)
--------------------------------------------------------------------------------
-- Reflexive closure
--------------------------------------------------------------------------------
-- reflexive closure
module Refl where
data Refl {l r} {A : Set l} (R : Rel A r) (a : A) : A → Set (l ⊔ r) where
ε : Refl R a a
_◅ε : ∀ {b} → R a b → Refl R a b
_?◅_ : ∀ {l r} {A : Set l} {R : Rel A r} {x y z : A} → Refl R x y → Star R y z → Star R x z
ε ?◅ yz = yz
xy ◅ε ?◅ yz = xy ◅ yz
map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (∀ {a b} → R a b → S (f a) (f b))
→ ∀ {a b} → Refl R a b → Refl S (f a) (f b)
map g ε = ε
map g (x ◅ε) = g x ◅ε
fromRefl : ∀ {a A r} {R : Rel {a} A r} → Reflexive R → Refl R ⇒ R
fromRefl refl ε = refl
fromRefl refl (x ◅ε) = x
open Refl public hiding (module Refl;map)
--------------------------------------------------------------------------------
-- Symmetric closure
--------------------------------------------------------------------------------
module Sym where
data CoSym {l r s} {A : Set l} (R : Rel A r) (S : Rel A s) (a : A) : A → Set (l ⊔ r ⊔ s) where
fwd : ∀ {b} → R a b → CoSym R S a b
bwd : ∀ {b} → S b a → CoSym R S a b
Sym : ∀ {l r} {A : Set l} (R : Rel A r) (a : A) → A → Set (l ⊔ r)
Sym R = CoSym R R
sym : ∀ {l r} {A : Set l} {R : Rel A r} {a b : A} → Sym R a b → Sym R b a
sym (fwd x) = bwd x
sym (bwd x) = fwd x
map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (∀ {a b} → R a b → S (f a) (f b))
→ ∀ {a b} → Sym R a b → Sym S (f a) (f b)
map g (fwd x) = fwd (g x)
map g (bwd x) = bwd (g x)
open Sym public hiding (map;sym)
--------------------------------------------------------------------------------
-- Symmetric-transitive closure
--------------------------------------------------------------------------------
module StarSym where
StarSym : ∀ {l r} {A : Set l} (R : Rel A r) → Rel A (l ⊔ r)
StarSym R = Star (Sym R)
map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (∀ {a b} → R a b → S (f a) (f b))
→ ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
map g = Star.map (Sym.map g)
sym : ∀ {l r A R} → StarSym {l} {r} {A} R ⇒ flip (StarSym R)
sym = Star.reverse Sym.sym
into : ∀ {l r A R} → Sym (Star R) ⇒ StarSym {l} {r} {A} R
into (fwd xs) = Star.map fwd xs
into (bwd xs) = Star.reverse bwd xs
symInto : ∀ {l r A R} → Sym (StarSym R) ⇒ StarSym {l} {r} {A} R
symInto (fwd xs) = xs
symInto (bwd xs) = sym xs
concat : ∀ {l r A R} → StarSym (StarSym {l} {r} {A} R) ⇒ StarSym R
concat = Star.concat ∘ Star.map symInto
concatMap : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (∀ {a b} → R a b → StarSym S (f a) (f b))
→ ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
concatMap g = Star.concat ∘ Star.map (symInto ∘ Sym.map g)
concatMap' : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (∀ {a b} → R a b → Star S (f a) (f b))
→ ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
concatMap' g = Star.concat ∘ Star.map (into ∘ Sym.map g)
open StarSym public using (StarSym)
--------------------------------------------------------------------------------------------------
-- Relations
--------------------------------------------------------------------------------------------------
module Relations where
-- Here are some lemmas about confluence
-- First the generic stuff
infix 3 _||_
record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
(R : REL A C r) (S : REL B C s)
(a : A) (b : B) : Set (la ⊔ lb ⊔ lc ⊔ r ⊔ s) where
constructor _||_
field {c} : C
field reduce₁ : R a c
field reduce₂ : S b c
module CommonReduct where
CommonReduct : ∀ {a r} {A : Set a} (R : Rel A r) → Rel A (a ⊔ r)
CommonReduct R = CommonReduct' R R
maps : ∀ {a b c d e f r s t u} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} {F : Set f}
{R : REL A C r} {S : REL B C s} {T : REL D F t} {U : REL E F u}
{f : A → D} {g : B → E} {h : C → F}
→ (∀ {u v} → R u v → T (f u) (h v))
→ (∀ {u v} → S u v → U (g u) (h v))
→ (∀ {u v} → CommonReduct' R S u v → CommonReduct' T U (f u) (g v))
maps f g (u || v) = f u || g v
map : ∀ {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
→ {f : A → B}
→ (R =[ f ]⇒ S) → (CommonReduct R =[ f ]⇒ CommonReduct S)
map g (u || v) = g u || g v
zip : ∀ {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : Rel A r} {S : Rel B s} {T : Rel C t}
→ {f : A → B → C}
→ (f Preserves₂ R ⟶ S ⟶ T)
→ (f Preserves₂ CommonReduct R ⟶ CommonReduct S ⟶ CommonReduct T)
zip f (ac || bc) (df || ef) = f ac df || f bc ef
swap : ∀ {a r} {A : Set a} {R S : Rel A r}
→ ∀ {x y} → CommonReduct' R S x y → CommonReduct' S R y x
swap (u || v) = v || u
open CommonReduct public using (CommonReduct)
module CR = CommonReduct
GenConfluent : ∀ {a r s t u} {A : Set a} (R : Rel A r) (S : Rel A s) (T : Rel A t) (U : Rel A u)
→ Set (a ⊔ r ⊔ s ⊔ t ⊔ u)
GenConfluent R S T U = ∀ {a b c} → R a b → S a c → CommonReduct' T U b c
-- With two relations
CoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
CoConfluent R S = GenConfluent R S S R
SemiCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
SemiCoConfluent R S = GenConfluent R (Star S) (Star S) (Star R)
HalfCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
HalfCoConfluent R S = GenConfluent R S (Star S) R
StrongCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
StrongCoConfluent R S = GenConfluent R (Star S) (Star S) (Refl R)
StrongerCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
StrongerCoConfluent R S = GenConfluent R (Star S) (Star S) R
ReflCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
ReflCoConfluent R S = GenConfluent R S (Refl S) (Refl R)
GlobalCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
GlobalCoConfluent R S = CoConfluent (Star R) (Star S)
-- Now with a single relation
Confluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
Confluent R = GenConfluent R R R R
LocalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
LocalConfluent R = GenConfluent R R (Star R) (Star R)
ReflConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
ReflConfluent R = GenConfluent R R (Refl R) (Refl R)
SemiConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)
GlobalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
GlobalConfluent R = Confluent (Star R)
--StrongConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
--StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)
-- semi confluence implies confluence for R*
SemiConfluent-to-GlobalConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → SemiCoConfluent R S → GlobalCoConfluent R S
SemiConfluent-to-GlobalConfluent conf ε ab = ab || ε
SemiConfluent-to-GlobalConfluent conf ab ε = ε || ab
SemiConfluent-to-GlobalConfluent conf (ab ◅ bc) ad with conf ab ad
... | be || de with SemiConfluent-to-GlobalConfluent conf bc be
... | cf || ef = cf || (de ◅◅ ef)
Confluent-to-StrongConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongCoConfluent R S
Confluent-to-StrongConfluent conf ab ε = ε || (ab ◅ε)
Confluent-to-StrongConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ce with Confluent-to-StrongConfluent conf ce cd
... | ef || df = be ◅ ef || df
Confluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongerCoConfluent R S
Confluent-to-StrongerConfluent conf ab ε = ε || ab
Confluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ce with Confluent-to-StrongerConfluent conf ce cd
... | ef || df = be ◅ ef || df
HalfConfluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → HalfCoConfluent R S → StrongerCoConfluent R S
HalfConfluent-to-StrongerConfluent conf ab ε = ε || ab
HalfConfluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ce with HalfConfluent-to-StrongerConfluent conf ce cd
... | ef || df = be ◅◅ ef || df
-- note: could be weakened to require StrongConfluent
Confluent-to-SemiConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → SemiCoConfluent R S
Confluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
Confluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ce with Confluent-to-SemiConfluent conf ce cd
... | ef || df = be ◅ ef || df
ReflConfluent-to-SemiConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → ReflCoConfluent R S → SemiCoConfluent R S
ReflConfluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
ReflConfluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ε = be ?◅ cd || ε
... | be || ce ◅ε with ReflConfluent-to-SemiConfluent conf ce cd
... | ef || df = be ?◅ ef || df
Confluent-Star : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → GlobalCoConfluent R S
Confluent-Star = SemiConfluent-to-GlobalConfluent ∘ Confluent-to-SemiConfluent
from-StarSym : ∀ {a r A} {R : Rel {a} A r} → GlobalConfluent R → Star (Sym R) ⇒ CommonReduct (Star R)
from-StarSym conf ε = ε || ε
from-StarSym conf (fwd ab ◅ bc) with from-StarSym conf bc
... | bd || cd = ab ◅ bd || cd
from-StarSym conf (bwd ba ◅ bc) with from-StarSym conf bc
... | bd || cd with conf (ba ◅ ε) bd
... | be || de = be || cd ◅◅ de
to-StarSym : ∀ {a r A} {R : Rel {a} A r} → CommonReduct (Star R) ⇒ Star (Sym R)
to-StarSym (xs || ys) = Star.map fwd xs ◅◅ Star.reverse bwd ys
-- strong normalization + local confluence implies global confluence
-- we can write SN R as Well-founded (flip R)
well-founded-confluent : ∀ {a A} {R : Rel {a} A a} → Well-founded (flip R) → LocalConfluent R → GlobalConfluent R
well-founded-confluent wf conf = acc-confluent conf (Plus.well-founded wf _)
where
acc-confluent : ∀ {a A} {R : Rel {a} A a} → LocalConfluent R → ∀ {a b c} → Acc (flip (Plus R)) a → Star R a b → Star R a c → CommonReduct (Star R) b c
acc-confluent conf _ ε ac = ac || ε
acc-confluent conf _ ab ε = ε || ab
acc-confluent conf (acc a) (ab ◅ bc) (ad ◅ de) with conf ab ad
... | bf || df with acc-confluent conf (a _ (ab ◅ ε)) bc bf
... | cg || fg with acc-confluent conf (a _ (ad ◅ ε)) de df
... | eh || fh with acc-confluent conf (a _ (ab ◅ bf)) fg fh
... | gi || hi = cg ◅◅ gi || eh ◅◅ hi
confluent-by : ∀ {a A r s} {R : Rel {a} A r} {S : Rel A s}
→ (S ⇒ R) → (R ⇒ S)
→ Confluent R → Confluent S
confluent-by toR fromR confR ab ac = CR.map fromR (confR (toR ab) (toR ac))
open Relations public
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment