Formalization of untyped lambda calculus, with proof of confluence.

2013-10-23-lambda.agda

-- 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))