ualc interpreter (reduction semantics, singlestep, cbn) with strong normalization and termination proofs

ualc-with-sn-proof.agda

open import Agda.Primitive using () renaming (lzero to l0)
open import Induction.WellFounded using (Acc; acc)
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality
open import Data.Empty using (⊥-elim)
open import Relation.Binary using (Rel)
open import Function using (flip)
open import Data.Nat renaming (ℕ to Nat)
open import Data.Nat.Properties
open import Data.Nat.Induction using (<-wellFounded)
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)

private
  variable
    l r n m : Nat

ap  = cong
ap₂ = cong₂
_∙_ = trans ; infixl 5 _∙_
~_  = sym   ; infix  6 ~_

infix 7 #_

-- A partition of variables between subterms
-- AKA a pair of nats where suc is done one side at a time
data Split : (l r : Nat) → Set where
  N  : Split 0 0
  L  : Split l r → Split (suc l) r
  R  : Split l r → Split l (suc r)

-- Terms with Split for application
data Term : Nat → Set where
  var     : Term 1
  lam     : Term (suc n) → Term n
  era     : Term n → Term n
  raw-app : Split l r → (l + r ≡ n) → Term l → Term r → Term n

-- combination of "raw-app" and "app" provides an interface to work with application such that
-- we avoid any usage transport or coercion since we can manipulate the type of the app with the
-- equivalence itself (as its type is indexed by eq's RHS)
app : Split l r → Term l → Term r → Term (l + r)
app s t u = raw-app s refl t u

+-commʳ : ∀ (n m p : Nat) → n + m + p ≡ n + p + m
+-commʳ n m p = trans (+-assoc n m p) (trans (cong (n +_) (+-comm m p)) (sym (+-assoc n p m)))

-- coercion is avoidable with right-biased addition or a usage of +-comm at raw-app, but this is simple enough
-- smart constructors to fix indices disparities
coe-L : ∀ {n} → n ≡ l → Split l r → Split n r
coe-L refl sp = sp

coe-R : ∀ {n} → n ≡ r → Split l r → Split l n
coe-R refl sp = sp

-- extend one side of a Split with `m` variables
append-L : ∀ m → Split l r → Split (l + m) r
append-L {l} {r} zero sp = coe-L (+-identityʳ l) sp
append-L {l} {r} (suc m) sp = coe-L (+-suc l m) (L (append-L m sp))

append-R : ∀ m → Split l r → Split l (r + m)
append-R {l} {r} zero sp = coe-R (+-identityʳ r) sp
append-R {l} {r} (suc m) sp = coe-R (+-suc r m) (R (append-R m sp))

#_ : Term n → Nat
# var = 0
# (lam bod) = suc (# bod)
# (era trm) = suc (# trm)
# (raw-app _ _ fun arg) = # fun + # arg

subs : ∀ (t : Term (suc n)) (u : Term m)
     → Σ[ trm ∈ Term (n + m) ] (# trm ≡ # t + # u)
subs var u = u , refl
subs (lam bod) u =
    let bod' , sz' = subs bod u
    in lam bod' , cong suc sz'
subs (era trm) u = 
    let trm' , sz' = subs trm u
    in era trm' , cong suc sz'
subs {_} {m} (raw-app {l} {r} sp eq fun arg) u with sp
... | L {l₁} sp =
    let fun' , fsz' = subs fun u
    in raw-app (append-L m sp) (+-commʳ l₁ m r ∙ ap (_+ m) (suc-injective eq)) fun' arg ,
       ap (_+ # arg) fsz' ∙ +-commʳ (# fun) (# u) (# arg)
... | R {l₁} {r₁} sp =
    let arg' , asz' = subs arg u
    in raw-app (append-R m sp) (~ +-assoc l r₁ m ∙ ap (_+ m) (suc-injective (~ +-suc l r₁ ∙ eq))) fun arg' ,
       ap (# fun +_) asz' ∙ ~ +-assoc (# fun) (# arg) (# u)

subs' : ∀ (t : Term (suc n)) (u : Term m) → Term (n + m)
subs' = λ t u → (subs t u) .fst

#-eq : ∀ (t : Term (suc n)) (u : Term m) → # subs' t u ≡ # t + # u
#-eq t u = snd (subs t u)

#-subst : ∀ {n m} (t : Term n) → (eq : n ≡ m) → (# t) ≡ (# (subst Term eq t))
#-subst var refl = refl
#-subst (lam bod) refl = cong suc (#-subst bod refl)
#-subst (era trm) refl = cong suc (#-subst trm refl) 
#-subst (raw-app _ _ fun arg) refl = cong₂ _+_ (#-subst fun refl) (#-subst arg refl)

mutual
  data Value : Term n → Set where
    vlam : ∀ {bod : Term (suc n)} → Value bod → Value (lam bod)
    neu : ∀ {t : Term n} → Neutral t → Value t

  data Neutral : Term n → Set where
    nvar : Neutral var
    napp : ∀ {l r} {aff eq} {t : Term l} {u : Term r} → Neutral t → Value u → Neutral {n} (raw-app aff eq t u)
    nera : ∀ {t : Term n} → Value t → Neutral (era t)

data Clos : Set where
  here    : Term 0 → Clos      -- The term itself, no era at head
  next    : Clos → Clos        -- An era wrapping the closure
  gotcha  : Term 1 → Clos      -- Found the lambda body

peel : Term 0 → Clos
peel (era t) = next (peel t)
peel (lam bod) = gotcha bod
peel t = here t  -- var or app, stop peeling

-- Count the eras in a closure
era-count : Clos → Nat
era-count (here   _) = 0
era-count (next   c) = suc (era-count c)
era-count (gotcha _) = 0

-- Wrap a term with n eras
wrap-eras : Nat → Term n → Term n
wrap-eras zero t = t
wrap-eras (suc n) t = era (wrap-eras n t)

get-body : Clos → Term 1
get-body (gotcha bod) = bod
get-body _ = var -- falback for non-lambda cases

peel-size : Clos → Nat
peel-size (here t) = # t
peel-size (next c) = suc (peel-size c)
peel-size (gotcha bod) = suc (# bod)

closed≤1 : ∀ (t : Term 0) → 1 ≤ # t
closed≤1 (lam t) = s≤s z≤n
closed≤1 (era t) = s≤s z≤n
closed≤1 (raw-app N _ fun arg) =
  let #f = closed≤1 fun
      #a = closed≤1 arg
  in +-mono-≤ #f (≤-trans z≤n #a) 
closed≤1 (raw-app {l} (R {r = r} aff) eq _ _) =
  ⊥-elim (1+n≢0 (+-comm (suc r) l ∙ eq))

peel-lemma : ∀ {t : Term 0} {u : Term n}
           → (# wrap-eras (era-count (peel t)) u) < # t + # u
peel-lemma {t = lam t} {u} =
  ≤-trans ≤-refl (s≤s (m≤n⇒m≤o+n (# t) ≤-refl))
peel-lemma {t = era t} = s≤s (peel-lemma {t = t})
peel-lemma {t = raw-app N refl fun arg} {u} =
  let #f = closed≤1 fun
      #a = closed≤1 arg
      #fau = +-mono-≤ (+-mono-≤ #f #a) (≤-reflexive (erefl (# u)))
  in ≤-trans (s≤s (n≤1+n (# u))) #fau
peel-lemma {t = raw-app {l} (R {r = r} aff) eq _ _} =
  ⊥-elim (1+n≢0 (+-comm (suc r) l ∙ eq))

infix 2 _~>_

data _~>_ : Term n → Term n → Set where

  ξ-l : ∀ {aff eq} {fun fun' : Term l} {arg : Term r}
    → fun ~> fun' 
      ----------------
    → _~>_ {n} (raw-app aff eq fun arg) (raw-app aff eq fun' arg)

  ξ-r : ∀ {aff eq} {fun : Term l} {arg arg' : Term r}
    → arg ~> arg'
      ----------------
    → _~>_ {n} (raw-app aff eq fun arg) (raw-app aff eq fun arg')

  β-app : ∀ {aff} {eq} {bod : Term (suc l)} {arg : Term r}
      ---------------------------------
    → _~>_ {n} (raw-app aff eq (lam bod) arg) (subst Term eq (subs' bod arg))

  ζ-lam : ∀ {bod bod' : Term (suc n)}
    → bod ~> bod'
    -----------
    → lam bod ~> lam bod'

  ζ-era : ∀ {trm trm' : Term n}
    → trm ~> trm'
    -----------
    → era trm ~> era trm'

  β-era : ∀ {aff eq} {fun : Term 0} {arg : Term l}
    → let clos = peel fun in
    _~>_ {n} (raw-app aff eq fun arg) (subst Term eq (wrap-eras (era-count clos) (subs' (get-body clos) arg)))

-- _~>_ implies a strict (total order) over size
~>-strict : ∀ (t u : Term n) → t ~> u → # u < # t
~>-strict t u (ξ-l {fun = fun} {fun'} {arg} st) =
    +-monoˡ-< (# arg) (~>-strict fun fun' st)
~>-strict t u (ξ-r {fun = fun} {arg} {arg'} st) =
    +-monoʳ-< (# fun) (~>-strict arg arg' st)
~>-strict t u (β-app {eq = eq} {bod = bod} {arg}) =
    s≤s (≤-reflexive (~ #-subst (subs' bod arg) eq ∙ (#-eq bod arg)))
~>-strict t u (ζ-lam {bod = bod} {bod'} st) = s<s (~>-strict bod bod' st)
~>-strict t u (ζ-era {trm = trm} {trm'} st) = s<s (~>-strict trm trm' st)
~>-strict t u (β-era {eq = eq} {fun = lam fun} {arg}) =
    s<s (≤-trans (≤-reflexive (~ (#-subst (subs' fun arg) eq)))
                   (≤-reflexive (#-eq fun arg)))
~>-strict {n} t u (β-era {eq = eq} {fun = era fun'} {arg}) =
  let asdf = ~ (#-subst (era (wrap-eras (era-count (peel fun')) (subs' var arg))) eq)
  in s<s (≤-trans (≤-trans (≤-reflexive asdf)
         (peel-lemma {t = fun'} {u = subs' var arg})) (+-monoʳ-≤ (# fun') ≤-refl))
~>-strict t u (β-era {eq = eq} {fun = raw-app N refl fun' arg} {arg'}) =
  let #f = closed≤1 fun'
      #a = closed≤1 arg
      #fau = +-mono-≤ (+-mono-≤ #f #a) (≤-reflexive (erefl (# u)))
      #r : # subst Term eq (subs' var arg') ≤ # arg'
      #r = ≤-reflexive (~ (#-subst arg' eq))
  in ≤-trans (s≤s (n≤1+n (# u)))
      (≤-trans #fau (+-monoʳ-≤ ((# fun') + # arg) #r)) --#fau
~>-strict t u (β-era {fun = raw-app {l} (R {r = r} af) eq fun' arg}) =
  ⊥-elim (1+n≢0 (+-comm (suc r) l ∙ eq))

size-wf : ∀ (t : Term n) → Acc _<_ (# t)
size-wf t = <-wellFounded (# t)

sn : ∀ (t : Term n) → Acc _<_ (# t) → Acc (flip _~>_) t
sn t (acc rs) = acc λ { {y} x → sn y (rs (~>-strict t y x))}

SN : ∀ (t : Term n) → Acc (flip _~>_) t
SN t = sn t (size-wf t)

-- reflexive transitive closure
data _~>*_ : Term n → Term n → Set where
  qed*  : ∀ {t : Term n} → t ~>* t
  step* : ∀ {t u v : Term n} → t ~> u → u ~>* v → t ~>* v

data Progress {n : Nat} (t : Term n) : Set where
  step : ∀ {u} → t ~> u → Progress t
  done : Value t → Progress t

progress : ∀ {n} (t : Term n) → Progress t
progress var = done (neu nvar)
progress (lam bod) with progress bod
... | step bod~>bod' = step (ζ-lam bod~>bod')
... | done bod-val = done (vlam bod-val)
progress (era trm) with progress trm
... | step trm~>trm' = step (ζ-era trm~>trm')
... | done trm-val = done (neu (nera trm-val))
progress (raw-app {l} {r} aff eq fun arg) with progress fun
... | step fun~>fun' = step (ξ-l fun~>fun')
... | done (vlam {bod = bod} bod-val) = step β-app
... | done (neu nfun) with progress arg
...   | step arg~>arg' = step (ξ-r arg~>arg')
...   | done arg-val with nfun
...     | nvar = done (neu (napp nvar arg-val))
...     | napp {aff = aff'} nfun' u-val = done (neu (napp (napp nfun' u-val) arg-val))
progress (raw-app {zero} {r} aff eq fun arg)  | done (neu nfun) | done arg-val | nera fun'-val =
  step {u = subst Term eq (wrap-eras (era-count (peel fun)) (subs' (get-body (peel fun)) arg))}
    (subst (λ x → raw-app aff eq fun arg ~> x) refl β-era)
progress (raw-app {suc l} {r} aff eq fun arg) | done (neu nfun) | done arg-val | nera fun'-val =
  done (neu (napp (nera fun'-val) arg-val))

eval-with-proof : ∀ {n} (t : Term n) → Σ[ u ∈ Term n ] (t ~>* u × Value u)
eval-with-proof t = eval' t (SN t) where
  eval' : ∀ {n} (t : Term n) → Acc (flip _~>_) t → Σ[ u ∈ Term n ] (t ~>* u × Value u)
  eval' t a with progress t
  ... | done val = t , qed* , val
  eval' t (acc rs) | step {u} t~>u with eval' u (rs t~>u)
  ... | u' , u~>*u' , u'-val = u' , (step* t~>u u~>*u') , u'-val

normal : ∀ {n} → Term n → Term n
normal t = (eval-with-proof t) .fst

-- tests
nrm-both-sides : ∀ (t u : Term n) → Set
nrm-both-sides x y = normal x ≡ normal y

-- applying id to itself yields the id
id-ap = app N (lam var) (lam var)
id-mono = app N id-ap id-ap

-- no omega thus
result-id : nrm-both-sides id-mono id-ap
result-id = refl

-- apply erased id to id leads to era id
trm-1 = app N (era (lam var)) (lam var)
result-1 = era (lam var)

trm-ap-1 : nrm-both-sides trm-1 result-1
trm-ap-1 = refl

-- test with era id on argument
trm-2 = app N (lam var) (era (lam var))
result-2 = era (lam var)

trm-ap-2 : nrm-both-sides trm-2 result-2
trm-ap-2 = refl

-- Test 3: Applying an erased identity to a variable
trm-3 = app (R N) (era (lam var)) var
result-3 = era var

trm-ap-3 : nrm-both-sides trm-3 result-3
trm-ap-3 = refl

-- Test 4: Nested application with erasure peeling
trm-4 = app N (era (era (lam var))) (lam var)
result-4 = era (era (lam var))

trm-ap-4 : nrm-both-sides trm-4 result-4
trm-ap-4 = refl

-- some facts about multistep relation (to show it is indeed a refl trans closure)

-- ξ and ζ equivalences implies multi-step relation is a congruence
app-cong₂ : ∀ {aff eq} {fun fun' : Term l} {arg arg' : Term r}
          → fun ~>* fun'
          → arg ~>* arg'
          → _~>*_ {n} (raw-app aff eq fun arg) (raw-app aff eq fun' arg')
app-cong₂ qed* qed* = qed*
app-cong₂ (step* p r) qed* = step* (ξ-l p) (app-cong₂ r qed*)
app-cong₂ qed* (step* q s) = step* (ξ-r q) (app-cong₂ qed* s)
app-cong₂ (step* p r) (step* q s) = step* (ξ-l p) (app-cong₂ r (step* q s))

app-L-cong : ∀ {aff eq} {fun fun' : Term l} {arg : Term r}
          → fun ~>* fun'
          → _~>*_ {n} (raw-app aff eq fun arg) (raw-app aff eq fun' arg)
app-L-cong st = app-cong₂ st qed*

app-R-cong : ∀ {aff eq} {fun : Term l} {arg arg' : Term r}
          → arg ~>* arg'
          → _~>*_ {n} (raw-app aff eq fun arg) (raw-app aff eq fun arg')
app-R-cong st = app-cong₂ qed* st

era-cong : ∀ {t u : Term n} 
          → t ~>* u 
          → era t ~>* era u
era-cong qed* = qed*
era-cong (step* p r) = step* (ζ-era p) (era-cong r)

lam-cong : ∀ {t u : Term (suc n)} 
          → t ~>* u 
          → lam t ~>* lam u
lam-cong qed* = qed*
lam-cong (step* p r) = step* (ζ-lam p) (lam-cong r)

-- multistep is transitive
trans* : ∀ {t u v : Term n} → t ~>* u → u ~>* v → t ~>* v 
trans* qed* q = q
trans* (step* p r) qed* = step* p r
trans* (step* p r) (step* q s) = step* p (trans* r (step* q s))