2.5. Normal and Neutral Terms🔗

The inductive predicates Normal and Neutral describe the normal forms of the named language. A lambda is normal when its body is normal; a neutral term is a variable applied to normal arguments.

\frac{e\ \mathsf{normal}}{\lambda x.\ e\ \mathsf{normal}} \qquad \frac{e\ \mathsf{neutral}}{e\ \mathsf{normal}}

\frac{}{x\ \mathsf{neutral}} \qquad \frac{e_1\ \mathsf{neutral} \qquad e_2\ \mathsf{normal}} {e_1\ e_2\ \mathsf{neutral}}

This mutual definition separates introduction forms from stuck computations: lambdas are normal directly, while neutral terms are variables applied to normal arguments.