Needed reduction and spine strategies for the lambda calculus
type: Item
instance of: scholarly article
title: Needed reduction and spine strategies for the lambda calculus
zbMATH Open document ID: 0635.03009
DOI: 10.1016/0890-5401(87)90001-0
author: Henk Barendregt
author: J. R. Kennaway
author: M. R. Sleep
author: Jan Willem Klop
published in: Information and Computation
publication date: 1987-01-01T00:00:00Z
full work available at URL: https://ir.cwi.nl/pub/1726
review text: 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.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4033695
zbMATH Keywords: needed redex
zbMATH Keywords: reduction to normal form
zbMATH Keywords: programming languages
zbMATH Keywords: spine redexes
describes a project that uses: Miranda
MaRDI profile type: Publication
OpenAlex ID: W2147478629
cites work: Q3889024
cites work: Q3342534
cites work: Q3205213
cites work: Minimal and Optimal Computations of Recursive Programs
cites work: Strictness analysis for higher-order functions
cites work: Q3780427
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Sequential evaluation strategies for parallel-or and related reduction systems
cites work: Q3918095
cites work: The Mechanical Evaluation of Expressions
cites work: The next 700 programming languages
cites work: Q4101795
cites work: Q3922646
cites work: A new implementation technique for applicative languages
cites work: Q3721784
Recommended article: Refining reduction in the lambda calculus
Recommended article: Q4521592
Recommended article: Term Rewriting and Applications
Recommended article: Reducibility Proofs in the λ-Calculus
Recommended article: Parallel reductions in \(\lambda\)-calculus
Recommended article: Reduction graphs in the lambda calculus
Recommended article: The self-reduction in lambda calculus
Recommended article: Q5224689
Recommended article: Combinatory weak reduction in lambda calculus
description: scientific article; zbMATH DE number 4033695