module LambdaTermination where
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
data List (a : Set) : Set where
[] : List a
_::_ : a -> List a -> List a
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
data Unit : Set where
U : Unit
data Absurd : Set where
Not : Set -> Set
Not x = x -> Absurd
contradiction : {a : Set} -> Absurd -> a
contradiction ()
data Type : Set where
O : Type
_=>_ : Type -> Type -> Type
el : Type -> Set
el O = Unit
el (s => t) = el s -> el t
Context : Set
Context = List Type
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
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'
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
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))
data Reducible : forall {ty} -> Closed ty -> Set where
Red : forall {ty} -> {c1 c2 : Closed ty} -> Step c1 c2 -> Reducible c1
NF : forall {ty} -> Closed ty -> Set
NF c = Not (Reducible c)
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 ())
data Terminates : forall {ty} -> Closed ty -> Set where
Halts : forall {ty} {c nf : Closed ty} -> NF nf -> Steps c nf -> Terminates c
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))
NormalizableEnv : forall {ctx} -> Env ctx -> Set
NormalizableEnv Nil = Unit
NormalizableEnv (Cons x env) = Pair (Normalizable _ x) (NormalizableEnv env)
normalizable-terminates : forall {ty c} -> Normalizable ty c -> Terminates c
normalizable-terminates {O} n = n
normalizable-terminates {ty => ty₁} (x , x₁) = x
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)
clapp-normalization : forall {A B} -> {c1 : Closed (A => B)} -> {c2 : Closed A} ->
Normalizable (A => B) c1 -> Normalizable A c2 -> Normalizable B (Clapp c1 c2)
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
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
normalizable-env : forall {ctx : Context} -> (env : Env ctx) -> NormalizableEnv env
normalizable-env Nil = U
normalizable-env (Cons x env₁) = (normalization _ x) , (normalizable-env env₁)