Normal order is the standard full-reducing strategy of the pure lambda calculus. It delivers the normal form of a term if it exists or diverges otherwise. It can be defined as a hybrid strategy following either a normal (leftmost) or a spine (quasi-leftmost) approach. Which are the proper corresponding versions in Plotkin’s lambda-value calculus? The answer is value normal order and value spine order. We construct these strategies from meta-theoretic considerations and introduce a precise characterisation for hybrid strategies.

The Standardisation Theorem and the Quasi-Leftmost Reduction Theorem substantiate the normal and the spine approach respectively in the classical lambda calculus. Plotkin gave the former for a calculus with strict functional semantics. We provide an analogous of the latter for Plotkin’s calculus, which we call the Negative-Weak Reduction Theorem. This shows that value spine order is correct and complete for full-reduction in lambda-value. Value spine order speeds up normalisation by early contracting some of the redices in the body of lambda abstractions, which has an impact in various language mechanisms (thunking) and features (beta-conversion testing).

This joint work with Pablo Nogueira has been submitted to ICFP2012.