Normalization by evaluation for extensional type theories

Question

Is there material on how to implement normalization for (any flavor of) ETT?

This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when trying to write NbE for ETT. (I understand that NbE in this case is undecidable, but NbE for UTLC is also undecidable, but it doesn't have this problem.)

• Usual languages don't possess an apparent LCCC (or whatever) structure. Of course, I can choose to implement ETT in ETT, but that sort of misses the point. How can I construct a semantic domain for me to normalize into?
• Operationally, I have difficulty defining normal and neutral forms. Usually, neutral forms should look like a series of eliminators (function applications, pair projections) stuck on a variable. And normal forms should be neutral forms wrapped in constructors (lambdas, pair constructors). But for ETT, say under a context $\Gamma$ containing $\mathit{eq} : \mathsf{Nat} = (\mathsf{Nat} \to \mathsf{Nat})$, we can write stuff like $$\Gamma \vdash 2(1) = (1+1)(1) : \mathsf{Nat},$$ which is the number 1 applied to the number 2. This is problematic because $2(1)$ is not normal or neutral according to the previously said standard. But it should!

Fundamentally the operational problem is caused by the semantic one, but it is more concrete and apparent.

Answer 1

For many partial languages, although conversion is undecidable, we can decide conversion up to non-termination. For example, in pure LC, conversion is decidable for the $\beta$-normalizing terms.

In ETT, it is still possible to define the $\beta$-reduction relation and talk about $\beta$-normal terms, but conversion is not decidable for such terms. ETT allows assuming arbitrary equational theories in contexts, so $\beta\eta$-rules for the "native" ETT type formers capture only a tiny fragment of conversion.

The best we can do as far as I see, is to semi-decide the $\beta\eta$-rules for native ETT type formers and ignore equality reflection. For this, we can do untyped NbE in the manner of Chapter 3 here. However, as you mentioned, we can't sensibly split normals and neutrals anymore, because computation can block even on a canonical value, for example we can apply true : Bool as a function. So we just mix all semantic values together, and compute all the well-typed $\beta$-redexes, and block computation in ill-typed cases.

For example, it makes sense to have the following evaluator for an untyped lambda calculus which additionally supports $\mathsf{Bool}$ primitives and gets stuck on ill-typed eliminations:

import Data.Maybe

type Name = String

data Tm = Var Name | App Tm Tm | IfThenElse Tm Tm Tm 
        | TTrue | TFalse | Lam Name Tm

data Val = VVar Name | VApp Val Val | VIfThenElse Val Val Val 
         | VTrue | VFalse | VLam Name (Val -> Val)

type Env = [(Name, Val)]

eval :: Env -> Tm -> Val
eval e t = case t of
  Var x -> fromJust $ lookup x e
  App t u -> case eval e t of
    VLam _ t -> t (eval e u)
    t        -> VApp t (eval e u)
  IfThenElse t u v -> case eval e t of
    VTrue -> eval e u
    VFalse -> eval e v
    t      -> VIfThenElse t (eval e u) (eval e v)
  TTrue -> VTrue
  TFalse -> VFalse
  Lam x t -> VLam x (\u -> eval ((x, u):e) t)

fresh :: Env -> Name -> Name
fresh e x = case lookup x e of
  Just{} -> fresh e (x ++ "'")
  _      -> x

-- beta-eta conversion
conv :: Env -> Val -> Val -> Bool
conv e t t' = case (t, t') of
  (VVar x, VVar x') -> x == x'
  (VApp t u, VApp t' u') -> conv e t t' && conv e u u'
  (VIfThenElse t u v, VIfThenElse t' u' v') ->
    conv e t t' && conv e u u' && conv e v v'
  (VTrue, VTrue) -> True
  (VFalse, VFalse) -> True
  (VLam x t, VLam x' t') ->
    let y = fresh e x; v = VVar y
    in conv ((y, v):e) (t v) (t' v)
  (VLam x t, t') ->
    let y = fresh e x; v = VVar y
    in conv ((y, v):e) (t v) (VApp t' v)
  (t, VLam x' t') ->
    let y = fresh e x'; v = VVar y
    in conv ((y, v):e) (VApp t v) (t' v)
  _ -> False

For ETT, we analogously add more type/term formers and eliminators. For the identity type, we would probably add the type former itself and refl, but no elimination rule.

Overall, I don't know if there's any compelling use case for an incomplete ETT conversion checker. If we want more definitional equalities than vanilla MLTT, I believe it's more promising to move to some other decidable type theory (such as observational TT). The above solution is merely what I would write if I were tasked with writing an incomplete ETT conversion checker.