Skip to content

Instantly share code, notes, and snippets.

@twanvl
Created October 23, 2013 10:07
Show Gist options
  • Save twanvl/7115932 to your computer and use it in GitHub Desktop.
Save twanvl/7115932 to your computer and use it in GitHub Desktop.
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