Needed reduction and spine strategies for the lambda calculus (Q1097253)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Needed reduction and spine strategies for the lambda calculus |
scientific article |
Statements
Needed reduction and spine strategies for the lambda calculus (English)
0 references
1987
0 references
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.
0 references
needed redex
0 references
reduction to normal form
0 references
programming languages
0 references
spine redexes
0 references