Normalization without reducibility
type: Item
instance of: scholarly article
title: Normalization without reducibility
zbMATH Open document ID: 0966.03015
DOI: 10.1016/S0168-0072(00)00030-0
author: René David
published in: Annals of Pure and Applied Logic
publication date: 2001-07-24T00:00:00Z
review text: This paper can be added to a long list of proofs for the well-known characterizations of -- strongly, weakly, head and weak head -- normalizing terms in the intersection type discipline. Motivated by the fact that Gallier has proven these characterizations in a uniform and semantical way, the author tries to use a syntactic method to prove them in a uniform way. I wonder whether this proof is correct and hope the wrong statement of Lemma 18 part 1 was a distraction of the author. The bibliography of this paper does not contain references to all original proofs, for instance Pottinger's 1980 paper in the Curry Festschrift is missing [\textit{G. Pottinger}, ``A type assignment for the strongly normalizable lambda terms'', in: J. P. Seldin et al. (eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, London etc., 561-578 (1980; Zbl 0469.03006)]. Moreover other papers that prove strong normalization along similar syntactic lines are not mentioned, like van \textit{D. T. van Daalen}'s PhD thesis [The language theory of Automath, Techn. Hoegeschool Eindhoven (1980; Zbl 0422.68045)].
reviewed by: Paula Severi
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1562993
MaRDI profile type: Publication
cites work: Q4222034
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A filter lambda model and the completeness of type assignment
cites work: A new type assignment for λ-terms
cites work: Functional Characters of Solvable Terms
cites work: Q4850465
cites work: Typing untyped \(\lambda\)-terms, or reducibility strikes again!
cites work: Q3997016
cites work: Typing and computational properties of lambda expressions
cites work: Complete restrictions of the intersection type discipline
Wikidata QID: Q126382660
description: scientific article; zbMATH DE number 1562993