Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Formalization of untyped lambda calculus, with proof of confluence.
-- Formalization of untyped lambda calculus
module 2013-10-23-lambda where
open import Level hiding (zero;suc)
open import Function using (_∘_;id;_⟨_⟩_)
open import Data.Empty
open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Product as P hiding (map;zip)
open import Data.Nat using (ℕ;suc)
open import Relation.Nullary
open ≡-Reasoning
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
infixl 6 _$_
-- The type of untyped lambda terms with free variables α
data T (α : Set) : Set where
-- a term can be a variable
V : α T α
-- or an application
_$_ : (x : T α) (y : T α) T α
-- or an abstraction of a term with one more free variable
Λ : T (Var α) T α
-- T forms a functor
map : {α β} β) T α T β
map f (V x) = V (f x)
map f (x $ y) = map f x $ map f y
map f (Λ x) = Λ (map (Var.map f) x)
map-T : {α β} T β) Var α T (Var β)
map-T f = unvar (V zero) (map suc ∘ f)
-- and a monad
bind : {α β} T β) T α T β
bind f (V x) = f x
bind f (x $ y) = bind f x $ bind f y
bind f (Λ x) = Λ (bind (map-T f) x)
-- note: we can't define the monad in terms of join directly,
-- because the termination checker doesn't know that map preserves the size of the argument
join : {α} T (T α) T α
join = bind id
-- we can use the monad for substitution
subst : {α} T α T (Var α) T α
subst x = bind (unvar x V)
-- 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 : {α β} {f g : α β} (f=g : x f x ≡ g x) (x : T α) map f x ≡ map g x
map-cong f=g (V x) = cong V (f=g x)
map-cong f=g (x $ y) = cong₂ _$_ (map-cong f=g x) (map-cong f=g y)
map-cong f=g (Λ x) = cong Λ (map-cong (unvar refl (cong suc ∘ f=g)) x)
map-id : {α} (x : T α) map id x ≡ x
map-id (V x) = refl
map-id (x $ y) = cong₂ _$_ (map-id x) (map-id y)
map-id (Λ x) = cong Λ (map-cong (unvar refl (\_ refl)) x ⟨ trans ⟩ map-id x)
map-map : {α β γ} (f : β γ) (g : α β) (x : T α)
map f (map g x) ≡ map (f ∘ g) x
map-map f g (V x) = refl
map-map f g (x $ y) = cong₂ _$_ (map-map f g x) (map-map f g y)
map-map f g (Λ x) = cong Λ (map-map (Var.map f) (Var.map g) x
⟨ trans ⟩ map-cong (unvar refl (\_ refl)) x)
-- let's also prove some properties of the monad
bind-cong : {α β} {f g : α T β}
(f=g : x f x ≡ g x) (x : T α) bind f x ≡ bind g x
bind-cong f=g (V x) = f=g x
bind-cong f=g (x $ y) = cong₂ _$_ (bind-cong f=g x) (bind-cong f=g y)
bind-cong f=g (Λ x) = cong Λ (bind-cong (unvar refl (cong (map suc) ∘ f=g)) x)
bind-map : {α β} (f : α β)→ (x : T α) bind (V ∘ f) x ≡ map f x
bind-map f (V x) = refl
bind-map f (x $ y) = cong₂ _$_ (bind-map f x) (bind-map f y)
bind-map f (Λ x) = cong Λ (bind-cong (unvar refl (\_ refl)) x
⟨ trans ⟩ bind-map (Var.map f) x)
bind-map₁ : {α β γ} (f : β T γ) (g : α β) (x : T α)
bind f (map g x) ≡ bind (f ∘ g) x
bind-map₁ f g (V x) = refl
bind-map₁ f g (x $ y) = cong₂ _$_ (bind-map₁ f g x) (bind-map₁ f g y)
bind-map₁ f g (Λ x) = cong Λ (bind-map₁ _ _ x
⟨ trans ⟩ bind-cong (unvar refl (\_ refl)) x)
bind-map₂ : {α β γ} (f : β γ) (g : α T β) (x : T α)
bind (map f ∘ g) x ≡ map f (bind g x)
bind-map₂ f g (V x) = refl
bind-map₂ f g (x $ y) = cong₂ _$_ (bind-map₂ f g x) (bind-map₂ f g y)
bind-map₂ f g (Λ x) = cong Λ (bind-cong (unvar refl (lem ∘ g)) x
⟨ trans ⟩ bind-map₂ _ _ x)
where
lem : y map suc (map f y) ≡ map (Var.map f) (map suc y)
lem y = map-map _ _ y ⟨ trans ⟩ sym (map-map _ _ y)
bind-bind : {α β γ} (f : β T γ) (g : α T β) (x : T α)
bind f (bind g x) ≡ bind (bind f ∘ g) x
bind-bind f g (V x) = refl
bind-bind f g (x $ y) = cong₂ _$_ (bind-bind f g x) (bind-bind f g y)
bind-bind f g (Λ x) = cong Λ (bind-bind _ _ x
⟨ trans ⟩ bind-cong (unvar refl (lem ∘ g)) x)
where
lem : y bind (map-T f) (map suc y) ≡ map suc (bind f y)
lem y = bind-map₁ _ _ y ⟨ trans ⟩ bind-map₂ _ _ y
-- derived properties
bind-return : {α} (x : T α) bind V x ≡ x
bind-return x = bind-map id x ⟨ trans ⟩ map-id x
-- derived properties
map-subst : {α β} (f : α β) (x : T α) (y : T (Var α))
map f (subst x y) ≡ subst (map f x) (map (Var.map f) y)
map-subst f x y
= sym (bind-map₂ _ _ y)
⟨ trans ⟩ bind-cong (unvar refl (\_ refl)) y
⟨ trans ⟩ sym (bind-map₁ _ _ y)
bind-subst : {α β} (f : α T β) (x : T α) (y : T (Var α))
bind f (subst x y) ≡ subst (bind f x) (bind (map-T f) y)
bind-subst f x y
= bind-bind _ _ y ⟨ trans ⟩
bind-cong (unvar refl (sym ∘ lem)) y ⟨ trans ⟩
sym (bind-bind _ _ y)
where
lem : y bind (unvar (bind f x) V) (map suc (f y)) ≡ f y
lem y = bind-map₁ _ _ (f y) ⟨ trans ⟩ bind-return (f y)
open Properties public
open Term hiding (map;bind)
-- Here are some example terms
i k s : T ⊥
i = Λ (V zero)
k = Λ (Λ (V (suc zero)))
s = Λ (Λ (Λ (V (suc (suc zero)) $ V zero $ (V (suc zero) $ V zero))))
-- Beta reduction
infix 5 _-β→_ _-β*→_
data _-β→_ {α} : T α → T α → Set where
$₁_ : {x x' y} x -β→ x' (x $ y) -β→ (x' $ y)
$₂_ : {x y y'} y -β→ y' (x $ y) -β→ (x $ y')
Λ : {x x'} x -β→ x' Λ x -β→ Λ x'
β! : {x y} (Λ x $ y) -β→ subst y x
_-β*→_ : {α} T α T α Set
_-β*→_ = Star _-β→_
-- We can do β-reduction manually
-- SKK → λK0(K0) → λ0
lemma₁ : (s $ k $ k) -β*→ i
lemma₁ = $₁ β! ◅ β! ◅ Λ ($₁ β!) ◅ Λ β! ◅ ε
-- Beta reduction is decidable
eval₁ : {α} (x : T α) Dec (∃ (_-β→_ x))
eval₁ (V x) = no no-V
where
no-V : {α} {x : α} ¬ ∃ (_-β→_ (V x))
no-V (_ , ())
eval₁ (x $ y) = eval-$ x y
where
no-$ : {α x y}
¬ ∃ (_-β→_ {α} x)
¬ ∃ (_-β→_ y)
¬ ∃ (\x' x ≡ Λ x')
¬ ∃ (_-β→_ (x $ y))
no-$ nx ny nΛ (._ , $₁ s) = nx (, s)
no-$ nx ny nΛ (._ , $₂ s) = ny (, s)
no-$ nx ny nΛ (._ , β!) = nΛ (, refl)
eval-$ : {α} x y Dec (∃ (_-β→_ {α} (x $ y)))
eval-$ x y with eval₁ x | eval₁ y
eval-$ x y | _ | yes (y' , s) = yes (x $ y' , $₂ s)
eval-$ x y | yes (x' , s) | _ = yes (x' $ y , $₁ s)
eval-$ (Λ x) _ | no nx | no ny = yes (, β!)
eval-$ (V _) _ | no nx | no ny = no (no-$ nx ny \{(_ , ())})
eval-$ (_ $ _) _ | no nx | no ny = no (no-$ nx ny \{(_ , ())})
eval₁ (Λ x) with eval₁ x
... | yes (x' , s) = yes (Λ x' , Λ s)
... | no n = no (no-Λ n)
where
no-Λ : {α x}
¬ ∃ (_-β→_ {Var α} x)
¬ ∃ (_-β→_ (Λ x))
no-Λ nx (._ , Λ x) = nx (, x)
-- And we can run β* up to n steps
eval : {α} (x : T α) ∃ (Star _-β→_ x)
eval 0 x = , ε
eval (suc n) x with eval₁ x
... | yes (x' , s) = , (s ◅ proj₂ (eval n x'))
... | no _ = , ε
-- which makes it much nicer to prove lemma₁
solve : {α} {x y : T α} (n : ℕ) (proj₁ (eval n x) ≡ y) x -β*→ y
solve {x = x} n refl = proj₂ (eval n x)
lemma₁' : (s $ k $ k) -β*→ i
lemma₁' = solve 4 refl
module Relations where
infix 3 _||_
-- Here are some lemmas about confluence
record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
(R : A → C → Set r) (S : B → C → Set s)
(a : A) (b : B) : Set (la ⊔ lb ⊔ lc ⊔ r ⊔ s) where
constructor _||_
field {c} : C
field reduce₁ : R a c
field reduce₂ : S b c
GenConfluent : {a r s t u} {A : Set a} (R : Rel A r) (S : Rel A s) (T : Rel A t) (U : Rel A u)
Set (a ⊔ r ⊔ s ⊔ t ⊔ u)
GenConfluent R S T U = {a b c} R a b S a c CommonReduct' T U b c
Confluent : {a r} {A : Set a} (R : Rel A r) Set (a ⊔ r)
Confluent R = GenConfluent R R R R
LocalConfluent : {a r} {A : Set a} (R : Rel A r) Set (a ⊔ r)
LocalConfluent R = GenConfluent R R (Star R) (Star R)
SemiConfluent : {a r} {A : Set a} (R : Rel A r) Set (a ⊔ r)
SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)
--StrongConfluent : {a r} {A : Set a} (R : Rel A r) Set (a ⊔ r)
--StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)
module CommonReduct where
CommonReduct : {a r} {A : Set a} (R : Rel A r) Rel A (a ⊔ r)
CommonReduct R = CommonReduct' R R
maps : {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
{f g h : A B}
(∀ {u v} R u v S (f u) (h v))
(∀ {u v} R u v S (g u) (h v))
(∀ {u v} CommonReduct R u v CommonReduct S (f u) (g v))
maps f g (u || v) = f u || g v
map : {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
{f : A B}
(R =[ f ]⇒ S) (CommonReduct R =[ f ]⇒ CommonReduct S)
map g (u || v) = g u || g v
zip : {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : Rel A r} {S : Rel B s} {T : Rel C t}
{f : A B C}
(f Preserves₂ R ⟶ S ⟶ T)
(f Preserves₂ CommonReduct R ⟶ CommonReduct S ⟶ CommonReduct T)
zip f (ac || bc) (df || ef) = f ac df || f bc ef
open CommonReduct public using (CommonReduct)
-- semi confluence implies confluence for R*
SemiConfluent-to-Confluent : {a r A} {R : Rel {a} A r} SemiConfluent R Confluent (Star R)
SemiConfluent-to-Confluent conf ε ab = ab || ε
SemiConfluent-to-Confluent conf ab ε = ε || ab
SemiConfluent-to-Confluent conf (ab ◅ bc) ad with conf ab ad
... | be || de with SemiConfluent-to-Confluent conf bc be
... | cf || ef = cf || (de ◅◅ ef)
-- note: could be weakened to require StrongConfluent
Confluent-to-SemiConfluent : {a r A} {R : Rel {a} A r} Confluent R SemiConfluent R
Confluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
Confluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
... | be || ce with Confluent-to-SemiConfluent conf ce cd
... | ef || df = be ◅ ef || df
Confluent-Star : {a r A} {R : Rel {a} A r} Confluent R Confluent (Star R)
Confluent-Star = SemiConfluent-to-Confluent ∘ Confluent-to-SemiConfluent
open Relations public
-- We could prove confluence via parallel reduction
data Parβ {α} : T α → T α → Set where
V : (x : α) Parβ (V x) (V x)
_$_ : {x x' y y'} Parβ x x' Parβ y y' Parβ (x $ y) (x' $ y')
Λ : {x x'} Parβ x x' Parβ (Λ x) (Λ x')
_$_◅β : {x x' y y'} Parβ x x' Parβ y y' Parβ (Λ x $ y) (subst y' x')
ε-Par : {α} {x : T α} Parβ x x
ε-Par {α} {V x} = V x
ε-Par {α} {x $ x₁} = ε-Par $ ε-Par
ε-Par {α} {Λ x} = Λ ε-Par
β→Par : {α} _-β→_ ⇒ Parβ {α}
β→Par ($₁ x) = β→Par x $ ε-Par
β→Par ($₂ x) = ε-Par $ β→Par x
β→Par (Λ x) = Λ (β→Par x)
β→Par β! = ε-Par $ ε-Par ◅β
Par→β : {α} Parβ {α} ⇒ _-β*→_
Par→β (V x) = ε
Par→β (x $ y) = Star.gmap (\xx xx $ _) $₁_ (Par→β x)
◅◅ Star.gmap (\yy _ $ yy) $₂_ (Par→β y)
Par→β (Λ x) = Star.gmap Λ Λ (Par→β x)
Par→β (x $ y ◅β) = Star.gmap (\yy _ $ yy) $₂_ (Par→β y)
◅◅ Star.gmap (\xx Λ xx $ _) ($₁_ ∘ Λ) (Par→β x)
◅◅ _-β→_.β! ◅ ε
Par*→β : {α} Star (Parβ {α}) ⇒ _-β*→_
Par*→β = Par→β ⋆
-- Parallel reduction is preserved under map and bind
map-Par : {α β x x'}
(f : α β)
Parβ x x'
Parβ (Term.map f x) (Term.map f x')
map-Par f (V x) = V (f x)
map-Par f (x $ y) = map-Par f x $ map-Par f y
map-Par f (Λ x) = Λ (map-Par (Var.map f) x)
map-Par f (_$_◅β {u} {u'} {v} {v'} x y) rewrite map-subst f v' u'
= map-Par (Var.map f) x $ map-Par f y ◅β
bind-Par : {α β y y'} {f g : α T β}
(fg : x Parβ (f x) (g x))
Parβ y y'
Parβ {β} (Term.bind f y) (Term.bind g y')
bind-Par fg (V x) = fg x
bind-Par fg (x $ y) = bind-Par fg x $ bind-Par fg y
bind-Par fg (Λ x) = Λ (bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x)
bind-Par {g = g} fg (_$_◅β {u} {u'} {v} {v'} x y) rewrite bind-subst g v' u'
= bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x $ bind-Par fg y ◅β
subst-Par : {α x y x' y'} Parβ {α} x x' Parβ y y' Parβ (subst x y) (subst x' y')
subst-Par x y = bind-Par (unvar x V) y
confluence-Par : {α} Confluent (Parβ {α})
confluence-Par (V .x) (V x) = V x || V x
confluence-Par (u $ x) (v $ y) = CommonReduct.zip _$_ (confluence-Par u v) (confluence-Par x y)
confluence-Par (Λ u) (Λ v) = CommonReduct.map Λ (confluence-Par u v)
confluence-Par (Λ u $ x) (v $ y ◅β) with confluence-Par u v | confluence-Par x y
... | uw || vw | xz || yz = uw $ xz ◅β || subst-Par yz vw
confluence-Par (u $ x ◅β) (Λ v $ y) with confluence-Par u v | confluence-Par x y
... | uw || vw | xz || yz = subst-Par xz uw || vw $ yz ◅β
confluence-Par (u $ x ◅β) (v $ y ◅β) with confluence-Par u v | confluence-Par x y
... | uw || vw | xz || yz = subst-Par xz uw || subst-Par yz vw
confluence-Par* : {α} Confluent (Star (Parβ {α}))
confluence-Par* = Confluent-Star confluence-Par
-- And now we get confluence for β*
confluence : {α} Confluent (Star (_-β→_ {α}))
confluence ab ac = CommonReduct.map Par*→β (confluence-Par* (Star.map β→Par ab) (Star.map β→Par ac))
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.