module LambdaTermination where

------------------------------------------------------------------------
-- Prelude.
--------------------------------------------------------------------------------

-- Equality, and laws.
data _==_ {a : Set} (x : a) : a -> Set where
 Refl : x == x

cong : forall {a b x y} -> (f : a -> b) -> x == y -> f x == f y
cong f Refl = Refl

symmetry : {a : Set} -> {x y : a} -> x == y -> y == x
symmetry Refl = Refl

transitivity : {a : Set} -> {x y z : a} -> x == y -> y == z -> x == z
transitivity Refl Refl = Refl

-- Lists.
data List (a : Set) : Set where
 []   : List a
 _::_ : a -> List a -> List a

-- Pairs.
data Pair (a b : Set) : Set where
  _,_ : a -> b -> Pair a b

fst : forall {a b} -> Pair a b -> a
fst (x , _) = x

snd : forall {a b} -> Pair a b -> b
snd (_ , x) = x

-- Unit type.
data Unit : Set where
 U : Unit

-- The empty type and negation.
data Absurd : Set where

Not : Set -> Set
Not x = x -> Absurd

contradiction : {a : Set} -> Absurd -> a
contradiction ()

------------------------------------------------------------------------
-- Types and terms.
--------------------------------------------------------------------------------

-- Unit and function types are supported.
data Type : Set where
 O    : Type
 _=>_ : Type -> Type -> Type

el : Type -> Set
el O = Unit
el (s => t) = el s -> el t

-- Type context: the top of this list is the type of the innermost
-- abstraction variable, the next element is the type of the next
-- variable, and so on.
Context : Set
Context = List Type

-- Reference to a variable, bound during some abstraction.
data Ref : Context -> Type -> Set where
 Top : forall {G u} -> Ref (u :: G) u
 Pop : forall {G u v} -> Ref G u -> Ref (v :: G) u

-- A term in the lambda calculus. The language solely consists of
-- abstractions, applications and variable references.
mutual
  data Term : Context -> Type -> Set where
   Abs : forall {G u v} -> (body : Term (u :: G) v) -> Term G (u => v)
   App : forall {G u v} -> (f : Term G (u => v)) -> (x : Term G u) -> Term G v
   Var : forall {G u} -> Ref G u -> Term G u

  data Env : List Type -> Set where
    Nil  : Env []
    Cons : forall {ctx ty} -> Closed ty -> Env ctx -> Env (ty :: ctx)

  data Closed : Type -> Set where
    Closure : forall {ctx ty} -> (t : Term ctx ty) -> (env : Env ctx) -> Closed ty
    Clapp : forall {ty ty'} -> (t : Closed (ty => ty')) -> (t' : Closed ty) -> Closed ty'

--------------------------------------------------------------------------------
---------------------        The simple evaluator             ------------------

lookup : forall {ctx ty} -> Ref ctx ty -> Env ctx -> Closed ty
lookup Top (Cons x env) = x
lookup (Pop i) (Cons x env) = lookup i env


--------------------------------------------------------------------------------
---------------------    Small step evaluation        --------------------------

data Step : forall {ty} -> Closed ty -> Closed ty -> Set where 
  Beta : {ty ty' : Type} {ctx : List Type} {body : Term (ty :: ctx) ty'} {c : Closed ty} {env : Env ctx} ->
    Step (Clapp (Closure (Abs body) env) c) (Closure body (Cons c env))
  Var : forall {ctx ty env} {i : Ref ctx ty} -> 
    Step (Closure (Var i) env) (lookup i env)
  App : forall {ty ty'} {c1 c2 : Closed (ty => ty')} {c : Closed ty} ->
    Step c1 c2 ->
    Step (Clapp c1 c) (Clapp c2 c)
  Dist : forall {ty ty' ctx env} {f : Term ctx (ty => ty')} {x : Term ctx ty} ->
    Step (Closure (App f x) env) (Clapp (Closure f env) (Closure x env))

-- Reducibility.
data Reducible : forall {ty} -> Closed ty -> Set where
 Red : forall {ty} -> {c1 c2 : Closed ty} -> Step c1 c2 -> Reducible c1

-- Non-reducable terms are considered normal forms.
NF : forall {ty} -> Closed ty -> Set
NF c = Not (Reducible c)

-- A sequence of steps that can be applied in succession.
data Steps : forall {ty} -> Closed ty -> Closed ty -> Set where
 Nil  : forall {ty} -> {c : Closed ty} -> Steps c c
 Cons : forall {ty} -> {c1 c2 c3 : Closed ty} -> 
   Step c1 c2 -> Steps c2 c3 -> Steps c1 c3

closures-normal : forall {ctx ty ty'} -> (t : Term (ty :: ctx) ty') -> (env : Env ctx) -> NF (Closure (Abs t) env)
closures-normal t env (Red ())

--------------------------------------------------------------------------------
-- Termination
--------------------------------------------------------------------------------

-- Definition of termination: a sequence of steps exist that ends up in a normal form.
data Terminates : forall {ty} -> Closed ty -> Set where
  Halts : forall {ty} {c nf : Closed ty} -> NF nf -> Steps c nf -> Terminates c

-- Instead of proving termination directly...
--   Try to prove something stronger
Normalizable : (ty : Type) -> Closed ty -> Set
Normalizable O c = Terminates c
Normalizable (ty => ty₁) c = 
  Pair (Terminates c) 
       ((t : Closed ty) -> Normalizable ty t -> Normalizable ty₁ (Clapp c t))

-- Structure that maintains normalization proofs for all elements in the environment.
NormalizableEnv : forall {ctx} -> Env ctx -> Set
NormalizableEnv Nil = Unit
NormalizableEnv (Cons x env) = Pair (Normalizable _ x) (NormalizableEnv env)

-- Normalization implies termination.
normalizable-terminates : forall {ty c} -> Normalizable ty c -> Terminates c
normalizable-terminates {O} n = n
normalizable-terminates {ty => ty₁} (x , x₁) = x


-- Helper lemma's for normalization proof.
normalizableStep : forall {ty} -> {c1 c2 : Closed ty} -> Step c1 c2 ->
   Normalizable ty c2 -> Normalizable ty c1
normalizableStep {O} step (Halts v steps) = Halts v (Cons step steps)
normalizableStep {ty => ty₁} step (Halts v steps , hyp) = 
  (Halts v (Cons step steps)) , 
  (\t nt -> normalizableStep (App step) (hyp t nt))

normalizableSteps : forall {ty} -> {c1 c2 : Closed ty} -> Steps c1 c2 -> Normalizable ty c2 -> Normalizable ty c1
normalizableSteps Nil n = n
normalizableSteps (Cons x steps) n = normalizableStep x (normalizableSteps steps n)

-- The following three lemmas may use mutual recursion. This is done
-- in Agda by separating the type signature and the function
-- definition.

-- Closed applications of the form 'f x' are normalizable when both f and x are normalizable.
clapp-normalization : forall {A B} -> {c1 : Closed (A => B)} -> {c2 : Closed A} -> 
                      Normalizable (A => B) c1  -> Normalizable A c2 -> Normalizable B (Clapp c1 c2)

-- All closure terms are normalizable.
closure-normalization : forall {ctx} -> (ty : Type) -> (t : Term ctx ty) -> (env : Env ctx) -> 
 NormalizableEnv env -> Normalizable ty (Closure t env)


closure-normalization _ (Abs t) env nenv = 
  (Halts (closures-normal t env) Nil) ,
   (\c nc -> normalizableStep Beta (closure-normalization _ t (Cons c env) (nc , nenv))) 
closure-normalization ty (App t t₁) env nenv = 
  let iht = closure-normalization _ t env nenv
      iht1 = closure-normalization _ t₁ env nenv
  in normalizableStep Dist (clapp-normalization iht iht1)
closure-normalization ty (Var x) env nenv = normalizableStep Var (nlookup env x nenv)
  where
  nlookup : forall {ctx ty} -> (env : Env ctx) -> (x : Ref ctx ty) -> NormalizableEnv env -> Normalizable ty (lookup x env)
  nlookup (Cons x₁ e) Top (x₂ , x₃) = x₂
  nlookup (Cons x₁ e) (Pop i) (x₂ , x₃) = nlookup e i x₃

clapp-normalization (x , x₁) nc2 = x₁ _ nc2


-- All terms are normalizable.
normalization : (ty : Type) -> (c : Closed ty) -> Normalizable ty c
normalization ty (Clapp c c₁) = clapp-normalization (normalization _ c) (normalization _ c₁)
normalization ty (Closure t env) = closure-normalization ty t env (normalizable-env env)
  where
  -- An environment is always normalizable
  normalizable-env : forall {ctx : Context} -> (env : Env ctx) -> NormalizableEnv env
  normalizable-env Nil = U
  normalizable-env (Cons x env₁) = (normalization _ x) , (normalizable-env env₁)