Created
December 21, 2013 23:48
-
-
Save twanvl/8076766 to your computer and use it in GitHub Desktop.
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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I found the following counter-example to eta-contraction of pairs:
http://www.seas.upenn.edu/~sweirich/types/archive/1991/msg00014.html