Type theories, normal forms, and \(D_{\infty}\)-lambda-models
type: Item
instance of: scholarly article
title: Type theories, normal forms, and \(D_{\infty}\)-lambda-models
zbMATH Open document ID: 0645.03011
DOI: 10.1016/0890-5401(87)90042-3
author: Mariangiola Dezani-Ciancaglini
author: Mario Coppo
author: Maddalena Zacchi
published in: Information and Computation
publication date: 1987-01-01T00:00:00Z
review text: The study of a special filter model for the \(\lambda\)-calculus (in the sense of H. Barendregt), denoted \({\mathcal F}^*\), is the main objective of this paper. The type assignement system, on which the definition of \({\mathcal F}^*\) is based, is the classical Curry's type assignement to which \(\omega\) (the universal type), the operator \(\Lambda\) (intersection) - for type formation, and an ``inclusion'' relation on types are added. Much more, the initial set of atomic types is a two- element set. It is proved that \({\mathcal F}^*\) is isomorphic with an inverse limit space \(D^*_{\infty}\) constructed from a (three point) lattice with a nonstandard initial projection, which is not (Hilbert- Post) complete. A nice characterization (the first purely semantic one?) for a term to be normalizable is also given.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03G10
zbMATH DE Number: 4051566
zbMATH Keywords: normalizable term
zbMATH Keywords: filter model
zbMATH Keywords: \(\lambda \)-calculus
zbMATH Keywords: type assignement
reviewed by: Cristian Masalagiu
MaRDI profile type: Publication
full work available at URL: 0890-5401(87)90042-3
OpenAlex ID: W1979206410
cites work: Q3221960
cites work: A filter lambda model and the completeness of type assignment
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: \(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
cites work: Q4109650
cites work: A new type assignment for λ-terms
cites work: Q4198724
cites work: Functional Characters of Solvable Terms
cites work: Q3036694
cites work: Q3221961
cites work: Combinatory logic. With two sections by William Craig.
cites work: Q3043110
cites work: Q3345747
cites work: Lambda‐Calculus Models and Extensionality
cites work: Q3659755
cites work: The completeness theorem for typing lambda-terms
cites work: Q4101793
cites work: A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
cites work: What is a model of the lambda calculus?
cites work: Q4163188
cites work: Q5649639
cites work: Data Types as Lattices
cites work: Q3959414
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Intensional interpretations of functionals of finite type I
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
description: scientific article; zbMATH DE number 4051566