{{ message }}

Instantly share code, notes, and snippets.

# twanvl/2013-11-13-relations.agda

Created Dec 21, 2013
Proof of confluence of beta reduction + D reduction (a simple form of eta for pairs), for the untyped lambda calculus. See http://lambda-the-ultimate.org/node/4835 for a discussion.
 module 2013-11-13-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 zip : ∀ {la lb lc r s t} {A : Set la} {B : Set lb} {C : Set lc} {R : Rel A r} {S : Rel B s} {T : Rel C t} → {f : A → B → C} → Reflexive R → Reflexive S → (∀ {a b c d} → R a b → S c d → T (f a c) (f b d)) → ∀ {a b c d} → Star R a b → Star S c d → Star T (f a c) (f b d) zip reflR reflS g xs ys = map (\x → g x reflS) xs ◅◅ map (\y → g reflR y) ys 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) zip : ∀ {la lb lc r s t} {A : Set la} {B : Set lb} {C : Set lc} {R : Rel A r} {S : Rel B s} {T : Rel C t} → {f : A → B → C} → Reflexive R → Reflexive S → (∀ {a b c d} → R a b → S c d → T (f a c) (f b d)) → ∀ {a b c d} → StarSym R a b → StarSym S c d → StarSym T (f a c) (f b d) zip reflR reflS g xs ys = map (\x → g x reflS) xs ◅◅ map (\y → g reflR y) ys 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 zips : ∀ {a b c d e f g h i r s t u v w} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} {F : Set f} {G : Set g} {H : Set h} {I : Set i} {R : REL A C r} {S : REL B C s} {T : REL D F t} {U : REL E F u} {V : REL G I v} {W : REL H I w} {f : A → D → G} {g : B → E → H} {h : C → F → I} → (∀ {x y u v} → R x y → T u v → V (f x u) (h y v)) → (∀ {x y u v} → S x y → U u v → W (g x u) (h y v)) → (∀ {x y u v} → CommonReduct' R S x y → CommonReduct' T U u v → CommonReduct' V W (f x u) (g y v)) zips f g (x || y) (u || v) = f x u || g y 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)) concatCR : ∀ {a r A} {R : Rel {a} A r} → GlobalConfluent R → StarSym (CommonReduct (Star R)) ⇒ CommonReduct (Star R) concatCR conf ε = ε || ε concatCR conf (fwd (ad || bd) ◅ bc) with concatCR conf bc ... | be || ce with conf bd be ... | df || ef = ad ◅◅ df || ce ◅◅ ef concatCR conf (bwd (bd || ad) ◅ bc) with concatCR conf bc ... | be || ce with conf bd be ... | df || ef = ad ◅◅ df || ce ◅◅ ef open Relations public -------------------------------------------------------------------------------- -- Empty relation -------------------------------------------------------------------------------- module Empty {a} {A : Set a} where Empty : Rel A Level.zero Empty _ _ = ⊥ confluent : Confluent Empty confluent () --gconfluent : GlobalConfluent Empty --gconfluent = {!!} -------------------------------------------------------------------------------- -- Triple common reduction -------------------------------------------------------------------------------- module CRPlus where infix 3 _|[_]|_ record CommonReductPlus {l r A} (R : Rel {l} A r) a b c : Set (l ⊔ r) where constructor _|[_]|_ field {d} : A field reduce₁ : R a d field reduce₂ : R b d field reduce₃ : R c d toCR : CommonReduct R a c toCR = reduce₁ || reduce₃ --fromCR : {l r A} {R : Rel {l} A r} {a b} → CommonReduct a b → ConfluentPlus : ∀ {a r A} (R : Rel {a} A r) → Set (a ⊔ r) ConfluentPlus R = ∀ {a b c} → R a b → R a c → CommonReductPlus R b a c
 module 2013-12-21-confluence-beta-d where open import 2013-11-13-relations open import Function open import Relation.Binary hiding (Sym) open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl) open ≡-Reasoning -------------------------------------------------------------------------------- -- Lambda calculus -------------------------------------------------------------------------------- module Var where -- The type (Var α) has one more element than the type α -- it is isomorphic to Maybe α data Var (α : Set) : Set where zero : Var α suc : α → Var α -- Case analysis for Var unvar : ∀ {α} {β : Var α → Set} → β zero → ((x : α) → β (suc x)) → (x : Var α) → β x unvar z _ zero = z unvar _ s (suc x) = s x map : ∀ {α β} → (α → β) → Var α → Var β map f = unvar zero (suc ∘ f) one : ∀ {α} → Var (Var α) one = suc zero two : ∀ {α} → Var (Var (Var α)) two = suc one open Var public hiding (map;module Var) module Term where data Term (A : Set) : Set where var : (a : A) → Term A lam : (a : Term (Var A)) → Term A app : (a : Term A) → (b : Term A) → Term A dup : (a : Term A) → (b : Term A) → Term A -- T forms a functor map : ∀ {A B} → (A → B) → Term A → Term B map f (var a) = var (f a) map f (lam x) = lam (map (Var.map f) x) map f (app x y) = app (map f x) (map f y) map f (dup x y) = dup (map f x) (map f y) map-Term : ∀ {A B} → (A → Term B) → Var A → Term (Var B) map-Term f = unvar (var zero) (map suc ∘ f) -- and a monad bind : ∀ {A B} → (A → Term B) → Term A → Term B bind f (var a) = f a bind f (lam x) = lam (bind (map-Term f) x) bind f (app x y) = app (bind f x) (bind f y) bind f (dup x y) = dup (bind f x) (bind f y) -- we can use the monad for substitution subst : ∀ {A} → Term (Var A) → Term A → Term A subst a b = bind (unvar b var) a -- We need these properties later on -- these are all just standard functor and monad laws module Properties where -- properties of map, i.e. the functor laws map-cong : ∀ {A B} {f g : A → B} → (f=g : ∀ x → f x ≡ g x) → (x : Term A) → map f x ≡ map g x map-cong f=g (var x) = PE.cong var (f=g x) map-cong f=g (lam x) = PE.cong lam (map-cong (unvar PE.refl (cong suc ∘ f=g)) x) map-cong f=g (app x y) = PE.cong₂ app (map-cong f=g x) (map-cong f=g y) map-cong f=g (dup x y) = PE.cong₂ dup (map-cong f=g x) (map-cong f=g y) map-id : ∀ {A} → (x : Term A) → map id x ≡ x map-id (var x) = PE.refl map-id (lam x) = PE.cong lam (map-cong (unvar PE.refl (\_ → PE.refl)) x ⟨ PE.trans ⟩ map-id x) map-id (app x y) = PE.cong₂ app (map-id x) (map-id y) map-id (dup x y) = PE.cong₂ dup (map-id x) (map-id y) map-map : ∀ {A B C} (f : B → C) (g : A → B) (x : Term A) → map f (map g x) ≡ map (f ∘ g) x map-map f g (var x) = PE.refl map-map f g (lam x) = PE.cong lam (map-map (Var.map f) (Var.map g) x ⟨ PE.trans ⟩ map-cong (unvar PE.refl (\_ → PE.refl)) x) map-map f g (app x y) = PE.cong₂ app (map-map f g x) (map-map f g y) map-map f g (dup x y) = PE.cong₂ dup (map-map f g x) (map-map f g y) -- let's also prove some properties of the monad bind-cong : ∀ {A B} {f g : A → Term B} → (f=g : ∀ x → f x ≡ g x) → (x : Term A) → bind f x ≡ bind g x bind-cong f=g (var x) = f=g x bind-cong f=g (lam x) = PE.cong lam (bind-cong (unvar PE.refl (PE.cong (map suc) ∘ f=g)) x) bind-cong f=g (app x y) = PE.cong₂ app (bind-cong f=g x) (bind-cong f=g y) bind-cong f=g (dup x y) = PE.cong₂ dup (bind-cong f=g x) (bind-cong f=g y) bind-map : ∀ {A B} → (f : A → B) → (x : Term A) → bind (var ∘ f) x ≡ map f x bind-map f (var x) = PE.refl bind-map f (lam x) = PE.cong lam (bind-cong (unvar PE.refl (\_ → PE.refl)) x ⟨ PE.trans ⟩ bind-map (Var.map f) x) bind-map f (app x y) = PE.cong₂ app (bind-map f x) (bind-map f y) bind-map f (dup x y) = PE.cong₂ dup (bind-map f x) (bind-map f y) bind-map₁ : ∀ {A B C} (f : B → Term C) (g : A → B) (x : Term A) → bind f (map g x) ≡ bind (f ∘ g) x bind-map₁ f g (var x) = PE.refl bind-map₁ f g (lam x) = PE.cong lam (bind-map₁ _ _ x ⟨ PE.trans ⟩ bind-cong (unvar PE.refl (\_ → PE.refl)) x) bind-map₁ f g (app x y) = PE.cong₂ app (bind-map₁ f g x) (bind-map₁ f g y) bind-map₁ f g (dup x y) = PE.cong₂ dup (bind-map₁ f g x) (bind-map₁ f g y) bind-map₂ : ∀ {A B C} (f : B → C) (g : A → Term B) (x : Term A) → bind (map f ∘ g) x ≡ map f (bind g x) bind-map₂ f g (var x) = PE.refl bind-map₂ f g (lam x) = PE.cong lam (bind-cong (unvar PE.refl (lem ∘ g)) x ⟨ PE.trans ⟩ bind-map₂ _ _ x) where lem : ∀ y → map suc (map f y) ≡ map (Var.map f) (map suc y) lem y = map-map _ _ y ⟨ PE.trans ⟩ PE.sym (map-map _ _ y) bind-map₂ f g (app x y) = PE.cong₂ app (bind-map₂ f g x) (bind-map₂ f g y) bind-map₂ f g (dup x y) = PE.cong₂ dup (bind-map₂ f g x) (bind-map₂ f g y) bind-bind : ∀ {A B C} (f : B → Term C) (g : A → Term B) (x : Term A) → bind f (bind g x) ≡ bind (bind f ∘ g) x bind-bind f g (var x) = PE.refl bind-bind f g (lam x) = PE.cong lam (bind-bind _ _ x ⟨ PE.trans ⟩ bind-cong (unvar PE.refl (lem ∘ g)) x) where lem : ∀ y → bind (map-Term f) (map suc y) ≡ map suc (bind f y) lem y = bind-map₁ _ _ y ⟨ PE.trans ⟩ bind-map₂ _ _ y bind-bind f g (app x y) = PE.cong₂ app (bind-bind f g x) (bind-bind f g y) bind-bind f g (dup x y) = PE.cong₂ dup (bind-bind f g x) (bind-bind f g y) -- derived properties bind-return : ∀ {A} → (x : Term A) → bind var x ≡ x bind-return x = bind-map id x ⟨ PE.trans ⟩ map-id x map-subst : ∀ {A B} (f : A → B) (a : Term (Var A)) (b : Term A) → map f (subst a b) ≡ subst (map (Var.map f) a) (map f b) map-subst f a b = PE.sym (bind-map₂ _ _ a) ⟨ PE.trans ⟩ bind-cong (unvar PE.refl \_ → PE.refl) a ⟨ PE.trans ⟩ PE.sym (bind-map₁ _ _ a) bind-subst : ∀ {A B} (f : A → Term B) (a : Term (Var A)) (b : Term A) → bind f (subst a b) ≡ subst (bind (map-Term f) a) (bind f b) bind-subst f a b = bind-bind _ _ a ⟨ PE.trans ⟩ bind-cong (unvar PE.refl (\x' → PE.sym (bind-return (f x')) ⟨ PE.trans ⟩ PE.sym (bind-map₁ (unvar (bind f b) var) suc (f x')))) a ⟨ PE.trans ⟩ PE.sym (bind-bind _ _ a) open Properties public open Term public hiding (map;bind;subst;module Term) -------------------------------------------------------------------------------- -- Reduction -------------------------------------------------------------------------------- data Beta {A} : Rel₀ (Term A) where beta : ∀ {a b} → Beta (app (lam a) b) (Term.subst a b) dup₁ : ∀ {a b} → StarSym Beta a b → Beta (dup a b) a dup₂ : ∀ {a b} → StarSym Beta a b → Beta (dup a b) b under-lam : ∀ {a a'} → Beta a a' → Beta (lam a) (lam a') under-app₁ : ∀ {a a' b} → Beta a a' → Beta (app a b) (app a' b) under-app₂ : ∀ {a b b'} → Beta b b' → Beta (app a b) (app a b') under-dup₁ : ∀ {a a' b} → Beta a a' → Beta (dup a b) (dup a' b) under-dup₂ : ∀ {a b b'} → Beta b b' → Beta (dup a b) (dup a b') -- we want to prove confluence of Beta -------------------------------------------------------------------------------- -- Simple dup rule -------------------------------------------------------------------------------- data IStep {A} : Rel₀ (Term A) where beta : ∀ {a b} → IStep (app (lam a) b) (Term.subst a b) dup : ∀ {a} → IStep (dup a a) a under-lam : ∀ {a a'} → IStep a a' → IStep (lam a) (lam a') under-app : ∀ {a a' b b'} → IStep a a' → IStep b b' → IStep (app a b) (app a' b') under-dup : ∀ {a a' b b'} → IStep a a' → IStep b b' → IStep (dup a b) (dup a' b') under-var : ∀ {a} → IStep (var a) (var a) irefl : ∀ {A} → Reflexive (IStep {A}) irefl {A} {var a} = under-var irefl {A} {lam x} = under-lam irefl irefl {A} {app x y} = under-app irefl irefl irefl {A} {dup x y} = under-dup irefl irefl -- isteps are preserved under map,bind,subst map-istep : ∀ {A B} → (f : A → B) → IStep =[ Term.map f ]⇒ IStep map-istep f (beta {a} {b}) rewrite map-subst f a b = beta map-istep f dup = dup map-istep f (under-lam x) = under-lam (map-istep _ x) map-istep f (under-app x y) = under-app (map-istep f x) (map-istep f y) map-istep f (under-dup x y) = under-dup (map-istep f x) (map-istep f y) map-istep f under-var = under-var bind-istep : ∀ {A B} (f : A → Term B) → IStep =[ Term.bind f ]⇒ IStep bind-istep f (beta {a} {b}) rewrite bind-subst f a b = beta bind-istep f dup = dup bind-istep f (under-lam x) = under-lam (bind-istep _ x) bind-istep f (under-app x y) = under-app (bind-istep f x) (bind-istep f y) bind-istep f (under-dup x y) = under-dup (bind-istep f x) (bind-istep f y) bind-istep f under-var = irefl -- conversion beta-to-isteps : ∀ {A} → Beta {A} ⇒ StarSym IStep betas-to-isteps : ∀ {A} → StarSym (Beta {A}) ⇒ StarSym IStep beta-to-isteps beta = fwd beta ◅ ε beta-to-isteps (dup₁ x) = StarSym.map (\u → under-dup irefl u) (StarSym.sym \$ betas-to-isteps x) ◅◅ fwd dup ◅ ε beta-to-isteps (dup₂ x) = StarSym.map (\u → under-dup u irefl) (betas-to-isteps x) ◅◅ fwd dup ◅ ε beta-to-isteps (under-lam x) = StarSym.map under-lam (beta-to-isteps x) beta-to-isteps (under-app₁ x) = StarSym.map (\u → under-app u irefl) (beta-to-isteps x) beta-to-isteps (under-app₂ x) = StarSym.map (\u → under-app irefl u) (beta-to-isteps x) beta-to-isteps (under-dup₁ x) = StarSym.map (\u → under-dup u irefl) (beta-to-isteps x) beta-to-isteps (under-dup₂ x) = StarSym.map (\u → under-dup irefl u) (beta-to-isteps x) betas-to-isteps ε = ε betas-to-isteps (fwd x ◅ xs) = beta-to-isteps x ◅◅ betas-to-isteps xs betas-to-isteps (bwd x ◅ xs) = StarSym.sym (beta-to-isteps x) ◅◅ betas-to-isteps xs istep-to-betas : ∀ {A} → IStep {A} ⇒ StarSym Beta istep-to-betas beta = fwd beta ◅ ε istep-to-betas dup = fwd (dup₁ ε) ◅ ε istep-to-betas (under-lam x) = StarSym.map under-lam (istep-to-betas x) istep-to-betas (under-app x y) = StarSym.map under-app₁ (istep-to-betas x) ◅◅ StarSym.map under-app₂ (istep-to-betas y) istep-to-betas (under-dup x y) = StarSym.map under-dup₁ (istep-to-betas x) ◅◅ StarSym.map under-dup₂ (istep-to-betas y) istep-to-betas under-var = ε -------------------------------------------------------------------------------- -- Step: parallel beta reduction, and dup reduction guarded by IStep -------------------------------------------------------------------------------- data Step {A} : Rel₀ (Term A) where beta : ∀ {a a' b b'} → Step a a' → Step b b' → Step (app (lam a) b) (Term.subst a' b') dup₁ : ∀ {a a' b} → StarSym IStep a b → Step a a' → Step (dup a b) a' under-lam : ∀ {a a'} → Step a a' → Step (lam a) (lam a') under-app : ∀ {a a' b b'} → Step a a' → Step b b' → Step (app a b) (app a' b') under-dup : ∀ {a a' b b'} → Step a a' → Step b b' → Step (dup a b) (dup a' b') under-var : ∀ {a} → Step (var a) (var a) srefl : ∀ {A} → Reflexive (Step {A}) srefl {A} {var a} = under-var srefl {A} {lam x} = under-lam srefl srefl {A} {app x y} = under-app srefl srefl srefl {A} {dup x y} = under-dup srefl srefl -- conversion istep-to-step : ∀ {A} → IStep {A} ⇒ Step istep-to-step beta = beta srefl srefl istep-to-step dup = dup₁ ε srefl istep-to-step (under-lam x) = under-lam (istep-to-step x) istep-to-step (under-app x y) = under-app (istep-to-step x) (istep-to-step y) istep-to-step (under-dup x y) = under-dup (istep-to-step x) (istep-to-step y) istep-to-step under-var = srefl step-to-betas : ∀ {A} → Step {A} ⇒ Star Beta step-to-betas (beta x y) = Star.map (under-app₁ ∘ under-lam) (step-to-betas x) ◅◅ Star.map under-app₂ (step-to-betas y) ◅◅ beta ◅ ε step-to-betas (dup₁ x y) = dup₁ (StarSym.concatMap istep-to-betas x) ◅ step-to-betas y ◅◅ ε step-to-betas (under-lam x) = Star.map under-lam (step-to-betas x) step-to-betas (under-app x y) = Star.map under-app₁ (step-to-betas x) ◅◅ Star.map under-app₂ (step-to-betas y) step-to-betas (under-dup x y) = Star.map under-dup₁ (step-to-betas x) ◅◅ Star.map under-dup₂ (step-to-betas y) step-to-betas under-var = ε step-to-isteps : ∀ {A} → Step {A} ⇒ StarSym IStep step-to-isteps = Star.concatMap beta-to-isteps ∘ step-to-betas -- steps are preserved under map,bind,subst map-step : ∀ {A B} → (f : A → B) → Step =[ Term.map f ]⇒ Step map-step f (beta {a' = a'} {b' = b'} x y) rewrite map-subst f a' b' = beta (map-step _ x) (map-step f y) map-step f (dup₁ x y) = dup₁ (StarSym.map (map-istep f) x) (map-step f y) map-step f (under-lam x) = under-lam (map-step _ x) map-step f (under-app x y) = under-app (map-step f x) (map-step f y) map-step f (under-dup x y) = under-dup (map-step f x) (map-step f y) map-step f under-var = under-var bind-step : ∀ {A B} {f g : A → Term B} (fg : ∀ x → Step (f x) (g x)) → ∀ {x y} → Step x y → Step (Term.bind f x) (Term.bind g y) bind-step {g = g} fg (beta {a' = a'} {b' = b'} x y) rewrite bind-subst g a' b' = beta (bind-step (unvar srefl (map-step suc ∘ fg)) x) (bind-step fg y) bind-step fg (dup₁ x y) = dup₁ (StarSym.map (bind-istep _) x) (bind-step fg y) bind-step fg (under-lam x) = under-lam (bind-step (unvar srefl (map-step suc ∘ fg)) x) bind-step fg (under-app x y) = under-app (bind-step fg x) (bind-step fg y) bind-step fg (under-dup x y) = under-dup (bind-step fg x) (bind-step fg y) bind-step fg under-var = fg _ subst-step : ∀ {A a a' b b'} → Step a a' → Step {A} b b' → Step (Term.subst a b) (Term.subst a' b') subst-step aa bb = bind-step (unvar bb \_ → srefl) aa -- confluence sconfluent : ∀ {A} → Confluent (Step {A}) sconfluent under-var under-var = under-var || under-var sconfluent (beta x y) (beta u v) = CR.zip subst-step (sconfluent x u) (sconfluent y v) sconfluent (beta x y) (under-app (under-lam u) v) = CR.zips subst-step beta (sconfluent x u) (sconfluent y v) sconfluent (under-app (under-lam x) y) (beta u v) = CR.zips beta subst-step (sconfluent x u) (sconfluent y v) sconfluent (dup₁ x y) (dup₁ u v) = sconfluent y v sconfluent (dup₁ x y) (under-dup u v) with sconfluent y u ... | y' || u' = y' || dup₁ (StarSym.sym (step-to-isteps u) ◅◅ x ◅◅ step-to-isteps v) u' sconfluent (under-dup u v) (dup₁ x y) with sconfluent y u ... | y' || u' = dup₁ (StarSym.sym (step-to-isteps u) ◅◅ x ◅◅ step-to-isteps v) u' || y' sconfluent (under-lam x) (under-lam u) = CR.map under-lam (sconfluent x u) sconfluent (under-app x y) (under-app u v) = CR.zip under-app (sconfluent x u) (sconfluent y v) sconfluent (under-dup x y) (under-dup u v) = CR.zip under-dup (sconfluent x u) (sconfluent y v) isteps-to-steps : ∀ {A} → StarSym (IStep {A}) ⇒ CommonReduct (Star Step) isteps-to-steps = from-StarSym (Confluent-Star sconfluent) ∘ StarSym.map istep-to-step betas-to-steps : ∀ {A} → Star (Beta {A}) ⇒ CommonReduct (Star Step) betas-to-steps = isteps-to-steps ∘ Star.concatMap beta-to-isteps -------------------------------------------------------------------------------- -- Combined, we get confluence for beta+D -------------------------------------------------------------------------------- beta-confluent : ∀ {A} → GlobalConfluent (Beta {A}) beta-confluent ab ac with betas-to-steps ab | betas-to-steps ac ... | ad || bd | ae || ce with Confluent-Star sconfluent ad ae ... | df || ef = Star.concatMap step-to-betas (bd ◅◅ df) || Star.concatMap step-to-betas (ce ◅◅ ef)

### delesley commented Jan 14, 2014

 I found the following counter-example to eta-contraction of pairs: http://www.seas.upenn.edu/~sweirich/types/archive/1991/msg00014.html