What is a neutral term?

Question

A neutral/normal term in the lambda calculus is typically defined

data nf = Lam of nf | Neu of ne
data ne = Var of int | App of ne * nf

Now the question is what to do about constructors and eliminators such as pairs, projections, natural numbers, or the recursor.

1. We could view them all neutral terms because they are just variables pair, fst, snd, zero, succ, rec that happen to have some semantic meaning. For example:

data ne = Var of int | App of ne * nf 
| Pair of nf * nf | Fst of nf | Snd of nf
| Zero | Succ of nf | Rec of nf * nf * nf

2. But this question considers an alternative, namely to view constructors (pairs, natural numbers) as normal terms and eliminators (projections, recursor) as neutral terms, which also seems to make sense considering Lam is the constructor for function types and App the eliminator. For example:

data nf = Lam of nf | Neu of ne
| Pair of nf * nf 
| Zero | Succ of nf
data ne = Var of int | App of ne * nf
| Fst of ne | Snd of ne 
| Rec of nf * nf * ne

(Edit) It seems in the first approach, terms are only normal up to $\lambda$-reductions, whereas in the second, terms are in fully normal form.

Is there an advantage to one approach over the other?

Answer 1

A neutral term is a variable, or an eliminator stuck on a neutral term. Basically a stack of eliminators applied to a variable.

These terms are called neutral, and distinguished from other normal forms, because they have not reduced to a constructor, but they cannot reduce further (because the eliminators are stuck on a variable).

With this in mind, your second definition of the type of normals and neutrals is the correct one. I would say this approach has the advantage of actually representing normal forms. I'm not sure why you would want a language with pairs where fst (pair zero zero) does not reduce.

I would also caution that constructors like pair and zero, and eliminators like fst and rec really are not "just variables", anymore than lam is just a variable. Of course they are "variables" in the sense that they are strings of characters, but as you say, they have semantic meaning distinct from variables. When I used "variable" earlier in this answer, I meant a thing with the semantics of a variable, that can be the subject of substitution.