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.
- We could view them all neutral terms because they are just variables
recthat 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
- 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
Lamis the constructor for function types and
Appthe 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?