Conservation and Uniform Normalization in Lambda Calculi with Erasing Reductions

Autor: Morten Heine Sørensen, Peter Møller Neergaard
Rok vydání: 2002
Předmět:
Zdroj: Information and Computation. 178(1):149-179
ISSN: 0890-5401
DOI: 10.1006/inco.2002.3153
Popis: For a notion of reduction in a λ-calculus one can ask whether a term satisfies conservation and uniform normalization. Conservation means that single-step reductions of the term preserve infinite reduction paths from the term. Uniform normalization means that either the term will have no reduction paths leading to a normal form or all reduction paths will lead to a normal form. In the classical conservation theorem for ∧I the distinction between the two notions is not clear: uniform normalization implies conservation, and conservation also implies uniform normalization. The reason for this is that ∧I is closed under reduction, due to the fact that reductions never erase terms in ∧I. More generally for nonerasing reductions, the two notions are equivalent on a set closed under reduction. However, when turning to erasing reductions the distinction becomes important as conservation no longer implies uniform normalization. This paper presents a new technique for finding uniformly normalizing subsets of a λ-calculus. This is done by combining a syntactic and a semantic criterion. The technique is demonstrated by several applications. The technique is used to present a new uniformly normalizing subset of the pure λ-calculus; this subset is a superset of ∧I and thus contains erasing K-redexes. The technique is also used to prove strong normalization from weak normalization of the simply typed λ-calculus extended with pairs; this is an extension of techniques developed recently by Sørensen and Xi. Before presenting the technique the paper presents a simple proof of a slightly weaker form of the characterization of perpetual redexes by Bergstra and Klop; this is a step for the later applications of the technique.
Databáze: OpenAIRE
Externí odkaz: