Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Proof of the open problem in section 7 of "Pure Subtype Systems" by DeLesley S. Hutchins.
module 2013-11-13-confluence-problem where
open import 2013-11-13-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
--------------------------------------------------------------------------------------------------
-- Depth based solution
--------------------------------------------------------------------------------------------------
module DepthBased where
-- depth of a term
depth : V
depth `A = zero
depth (`C x) = depth x
depth (`D x y) = suc (depth x ⊔ depth y)
-- steps of bounded depth
-- `Step n` works under at most n `Ds, and also produces terms no more than n deep
data Step : (n : ℕ) → Rel₀ V where
aca : {n} Step n (`A) (`C `A)
d₁ : {n a b} (da : depth a ≤ n) StarSym (Step n) a b Step (suc n) (`D a b) a
d₂ : {n a b} (db : depth b ≤ n) StarSym (Step n) a b Step (suc n) (`D a b) b
under-c : {n a a'} (x : Step n a a') Step n (`C a) (`C a')
under-d : {n a b a' b'} (x : Star (Step n) a a') (y : Star (Step n) b b') Step (suc n) (`D a b) (`D a' b')
-- we can do many steps at a lower level
many : {n a b} (da : depth a ≤ n) (xs : Star (Step n) a b) Step (suc n) a b
-- for convenience in confluence proof there is an 'empty' step
ε : {n a} Step n a a
lift-step : {m n} m ≤ n Step m ⇒ Step n
lift-step m≤n aca = aca
lift-step (s≤s m≤n) (d₁ da x) = d₁ (≤-trans da m≤n) (StarSym.map (lift-step m≤n) x)
lift-step (s≤s m≤n) (d₂ db x) = d₂ (≤-trans db m≤n) (StarSym.map (lift-step m≤n) x)
lift-step m≤n (under-c x) = under-c (lift-step m≤n x)
lift-step (s≤s m≤n) (under-d x y) = under-d (Star.map (lift-step m≤n) x) (Star.map (lift-step m≤n) y)
lift-step (s≤s m≤n) (many da xs) = many (≤-trans da m≤n) (Star.map (lift-step m≤n) xs)
lift-step m≤n ε = ε
-- depth of output is ≤ depth of input
step-depth : {n} Step n =[ depth ]⇒ _≥_
steps-depth : {n} Star (Step n) =[ depth ]⇒ _≥_
step-depth aca = ≤-refl
step-depth (d₁ {a = a} {b = b} _ _) = ≤-step (m≤m⊔n (depth a) (depth b))
step-depth (d₂ {a = a} {b = b} _ _) = ≤-step (n≤m⊔n (depth a) (depth b))
step-depth (under-c x) = step-depth x
step-depth (under-d x y) = s≤s (≤⊔≤ (steps-depth x) (steps-depth y))
step-depth (many _ x) = steps-depth x
step-depth ε = ≤-refl
steps-depth xs = Star.foldMap _≥_ (flip ≤-trans) ≤-refl step-depth xs
-- Conversion from Step to ⟶ is easy
from-step : {n} Step n ⇒ Star _⟶_
from-step aca = aca ◅ ε
from-step (d₁ _ x) = d₁ (StarSym.concatMap' from-step x) ◅ ε
from-step (d₂ _ x) = d₂ (StarSym.concatMap' from-step x) ◅ ε
from-step (under-c x) = Star.map under-c (from-step x)
from-step (under-d x y) = Star.map under-d₁ (Star.concatMap from-step x)
◅◅ Star.map under-d₂ (Star.concatMap from-step y)
from-step (many _ xs) = Star.concatMap from-step xs
from-step ε = ε
-- Now we can convert from ⟶ to Step
module Any where
Any : {A B : Set} (A Rel₀ B) Rel₀ B
Any R b c = ∃ \a R a b c
open Any using (Any)
to-step : _⟶_ ⇒ Any Step
to-steps : Star _⟶_ ⇒ Any (Star ∘ Step)
to-eq : _==_ ⇒ Any (StarSym ∘ Step)
to-step aca = zero , aca
to-step (d₁ {a = a} {b = b} eq) with to-eq eq
... | n , eq' = suc (n ⊔ (depth a ⊔ depth b))
, d₁ (≤-trans (m≤m⊔n (depth a) (depth b)) (n≤m⊔n n _))
(StarSym.map (lift-step (m≤m⊔n _ _)) eq')
to-step (d₂ {a = a} {b = b} eq) with to-eq eq
... | n , eq' = suc (n ⊔ (depth a ⊔ depth b))
, d₂ (≤-trans (n≤m⊔n (depth a) (depth b)) (n≤m⊔n n _))
(StarSym.map (lift-step (m≤m⊔n _ _)) eq')
to-step (under-c x) = P.map id under-c (to-step x)
to-step (under-d₁ x) = P.map suc (\x' under-d (x' ◅ ε) ε) (to-step x)
to-step (under-d₂ y) = P.map suc (\y' under-d ε (y' ◅ ε)) (to-step y)
to-symstep : Sym _⟶_ ⇒ Any (Sym ∘ Step)
to-symstep (fwd x) = P.map id fwd (to-step x)
to-symstep (bwd x) = P.map id bwd (to-step x)
to-steps ε = zero , ε
to-steps (x ◅ xs) with to-step x | to-steps xs
... | m , x' | n , xs' = (m ⊔ n) , lift-step (m≤m⊔n m n) x' ◅ Star.map (lift-step (n≤m⊔n m n)) xs'
to-eq ε = zero , ε
to-eq (x ◅ xs) with to-symstep x | to-eq xs
... | m , x' | n , xs' = (m ⊔ n) , Sym.map (lift-step (m≤m⊔n m n)) x'
◅ StarSym.map (lift-step (n≤m⊔n m n)) xs'
-- if x has depth ≤ n, then all steps out of it also have depth ≤ n
-- This depends on confluence, we pass in confluence explicitly, to help the termination checker.
lower-step : {n a b} (∀ {m} m ≤′ n GlobalConfluent (Step m)) Step (suc n) a b depth a ≤ n Star (Step n) a b
lower-steps : {n a b} (∀ {m} m ≤′ suc n GlobalConfluent (Step m)) Star (Step (suc n)) a b depth a ≤ n Star (Step n) a b
lower-eq : {n a b} (∀ {m} m ≤′ suc n GlobalConfluent (Step m)) StarSym (Step (suc n)) a b depth a ≤ n depth b ≤ n StarSym (Step n) a b
lower-step conf aca da = aca ◅ ε
lower-step conf (d₁ {a = a} {b = b} _ eq) (s≤s da) =
d₁ (≤-trans (m≤m⊔n (depth a) (depth b)) da)
(lower-eq conf eq (≤-trans (m≤m⊔n (depth a) (depth b)) da)
(≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
lower-step conf (d₂ {a = a} {b = b} _ eq) (s≤s da) =
d₂ (≤-trans (n≤m⊔n (depth a) (depth b)) da)
(lower-eq conf eq (≤-trans (m≤m⊔n (depth a) (depth b)) da)
(≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
lower-step conf (under-c x) da = Star.map under-c (lower-step conf x da)
lower-step conf (under-d {a = a} {b = b} x y) (s≤s da) =
under-d (lower-steps conf x (≤-trans (m≤m⊔n (depth a) (depth b)) da))
(lower-steps conf y (≤-trans (n≤m⊔n (depth a) (depth b)) da)) ◅ ε
lower-step conf (many _ xs) da = xs
lower-step conf ε da = ε
lower-steps conf ε da = ε
lower-steps conf (x ◅ xs) da = lower-step (conf ∘ ≤′-step) x da ◅◅ lower-steps conf xs (≤-trans (step-depth x) da)
lower-eq {n} conf xs da db with from-StarSym (conf ≤′-refl) xs
... | us || vs = Star.map fwd (lower-steps conf us da)
◅◅ Star.reverse bwd (lower-steps conf vs db)
-- It's confluence time
confluent : {n} Confluent (Step n)
gconfluent : {n} GlobalConfluent (Step n)
gconfluent-upto : {m n} m ≤′ n GlobalConfluent (Step m)
confluent x ε = ε || x
confluent ε y = y || ε
confluent {n = suc n} (many da xs) y with gconfluent {n} xs (lower-step {n} gconfluent-upto y da)
... | u || v = many (≤-trans (steps-depth xs) da) u || many (≤-trans (step-depth y) da) v
confluent {n = suc n} x (many da ys) with gconfluent {n} (lower-step {n} gconfluent-upto x da) ys
... | u || v = many (≤-trans (step-depth x) da) u || many (≤-trans (steps-depth ys) da) v
confluent aca aca = ε || ε
confluent (d₁ _ eq) (d₁ _ _) = ε || ε
confluent (d₂ _ eq) (d₂ _ _) = ε || ε
confluent {n = suc n} (d₁ da eq) (d₂ db _) with from-StarSym (gconfluent {n}) eq
... | u || v = many da u || many db v
confluent {n = suc n} (d₂ db eq) (d₁ da _) with from-StarSym (gconfluent {n}) eq
... | u || v = many db v || many da u
confluent (d₁ da eq) (under-d u v) = many da u
|| d₁ (≤-trans (steps-depth u) da)
(StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v))
confluent (d₂ db eq) (under-d u v) = many db v
|| d₂ (≤-trans (steps-depth v) db)
(StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v))
confluent (under-d u v) (d₁ da eq) = d₁ (≤-trans (steps-depth u) da)
(StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v)) || many da u
confluent (under-d u v) (d₂ db eq) = d₂ (≤-trans (steps-depth v) db)
(StarSym.into (bwd u) ◅◅ eq ◅◅ StarSym.into (fwd v)) || many db v
confluent (under-c x) (under-c y) = CR.map under-c (confluent x y)
confluent (under-d x y) (under-d u v) = CR.zip under-d (gconfluent x u) (gconfluent y v)
gconfluent {n} = Confluent-Star (confluent {n})
gconfluent-upto ≤′-refl = gconfluent
gconfluent-upto (≤′-step m≤n) = gconfluent-upto m≤n
⟶-gconfluent : GlobalConfluent _⟶_
⟶-gconfluent x y with to-steps x | to-steps y
... | m , x' | n , y' with gconfluent (Star.map (lift-step (m≤m⊔n m n)) x') (Star.map (lift-step (n≤m⊔n m n)) y')
... | u || v = Star.concatMap from-step u || Star.concatMap from-step v
-- Q.E.D.
-- Utilities about relations
-- In particular, define what confluence means.
module 2013-11-13-relations where
open import Level hiding (zero;suc)
open import Function -- using (_∘_;id;_⟨_⟩_)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
--------------------------------------------------------------------------------
-- 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
--------------------------------------------------------------------------------
-- 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;_◅_;_◅◅_;ε;_⋆)
--------------------------------------------------------------------------------
-- 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 ◅ε
open Refl public hiding (module Refl;map)
--------------------------------------------------------------------------------
-- Symmetric closure
--------------------------------------------------------------------------------
module Sym where
data Sym {l r} {A : Set l} (R : Rel A r) (a : A) : A → Set (l ⊔ r) where
fwd : {b} R a b Sym R a b
bwd : {b} R b a Sym R a b
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 (module Sym;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)
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) = Star.reverse Sym.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
infix 3 _||_
-- Here are some lemmas about confluence
record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
(R : A → C → Set r) (S : B → C → Set 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
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
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)
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 r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
{f g h : A B}
(∀ {u v} R u v S (f u) (h v))
(∀ {u v} R u v S (g u) (h v))
(∀ {u v} CommonReduct R u v CommonReduct S (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 : Rel A r}
{x y} CommonReduct R x y CommonReduct R y x
swap (u || v) = v || u
open CommonReduct public using (CommonReduct)
module CR = CommonReduct
-- semi confluence implies confluence for R*
SemiConfluent-to-GlobalConfluent : {a r A} {R : Rel {a} A r} SemiConfluent R GlobalConfluent R
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)
-- note: could be weakened to require StrongConfluent
Confluent-to-SemiConfluent : {a r A} {R : Rel {a} A r} Confluent R SemiConfluent R
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 A} {R : Rel {a} A r} ReflConfluent R SemiConfluent R
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 A} {R : Rel {a} A r} Confluent R GlobalConfluent R
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
open Relations public
--------------------------------------------------------------------------------
-- Empty relation
--------------------------------------------------------------------------------
module Empty {a} {A : Set a} where
Empty : Rel A Level.zero
Empty _ _ =
confluent : Confluent Empty
confluent ()
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.