Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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

This comment has been minimized.

Copy link

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

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.