module Palmse.Combinators.Nbe where
open import Palmse.Combinators.TyTm
open import Palmse.Product
-- First we define the glueing semantics for types. The meaning of a term of natural
-- number type is a term (its normal form). The meaning of a function term
-- is a term (the normal form of the function) and a function from the meaning of the
-- input to the meaning of the output.
[[_]]₀ : Ty -> Set
[[ N ]]₀ = Tm N
[[ a => b ]]₀ = Tm (a => b) × ([[ a ]]₀ -> [[ b ]]₀)
-- We need an application in the model:
appsem : {a b : Ty} -> [[ a => b ]]₀ -> [[ a ]]₀ -> [[ b ]]₀
appsem {a} {b} (e , f) e' = f e'
-- Reification (to go from semantics to syntax) is easy. In the base case we just
-- return the normal natural number which is also the meaning. In the function case
-- we return the first component (the normal form).
reify : (a : Ty) -> [[ a ]]₀ -> Tm a
reify N e = e
reify (a => b) (e , f) = e
-- The meaning of terms is defined as follows. The case of K is easy and instructive.
-- The first component of the pair is the meaning of K standing alone, which is K itself
-- (K is the normal form of K)
-- The first component of the second component will be used for computing the normal
-- form of K applied to one argument. It is K applied to the normal form of that argument
-- which in turn is obtained by reifying the meaning of that argument.
-- The second component of the second component will be used for normalizing K applied
-- to two arguments. This is the normal form of the first of these two arguments.
[[_]]₁ : {a : Ty} -> Tm a -> [[ a ]]₀
[[ ze ]]₁ = ze
[[ su ]]₁ = (su ,
\e -> su ´ e)
[[ k {a} {b} ]]₁ = (k ,
\x -> (k ´ (reify a x) ,
\y -> x))
[[ s {a} {b} {c} ]]₁ = (s ,
(\x -> s ´ (reify (a => b => c) x) ,
(\y -> s ´ (reify (a => b => c) x) ´ (reify (a => b) y) ,
(\z -> appsem (appsem x z) (appsem y z)))))
[[ e ´ e' ]]₁ = appsem [[ e ]]₁ [[ e' ]]₁
-- Finally, we are ready to define the normalization function by composing meaning and
-- reification.
nbe : (a : Ty) -> Tm a -> Tm a
nbe a e = reify a [[ e ]]₁