Needed reduction and spine strategies for the lambda calculus (Q1097253)

A redex R in a lambda-term M is called needed if in every reduction of M to normal form (some residual of) R is contracted. Among others the following results are proved: 1. R is needed in M iff R is contracted in the leftmost reduction path of M. 2. Let \({\mathcal R}: M_ 0\to M_ 1\to M_ 2\to..\). reduce redexes \(R_ i: M_ i\to M_{i+1}\), and have the property that \(\forall i.\exists j\geq i\). \(R_ j\) is needed in \(M_ j\). Then \({\mathcal R}\) is normalizing, i.e., if \(M_ 0\) has a normal form, then \({\mathcal R}\) is finite and terminates at that normal form. 3. Neededness is an undecidable property, but has several efficiently decidable approximations, various versions of the so-called spine redexes.