9
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ Trebor is asking how to implement Trebor $\endgroup$
    – ice1000
    May 12 at 15:56
  • $\begingroup$ I just edited the extensional-equality tag but now I'm not sure the name matches its description, since the description refers to equality reflection, whereas extensional equality may refer to an extensional principle such as functional extensionality... perhaps a better name would be equality-reflection or extensional-type-theory? $\endgroup$
    – Couchy
    May 12 at 20:55
  • $\begingroup$ @Couchy Perhaps yes, and let's change it before any ambiguous uses crop up. $\endgroup$
    – Trebor
    May 13 at 0:35
  • $\begingroup$ I would lean towards extensional-type-theory then since it is appears more common $\endgroup$
    – Couchy
    May 13 at 3:33

1 Answer 1

5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.