Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
New proof of confluence thing (see https://gist.github.com/twanvl/7453495), which will hopefully also extend to lambda calculus.
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)
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
You can’t perform that action at this time.