Intersection types for combinatory logic
type: Item
instance of: scholarly article
title: Intersection types for combinatory logic
zbMATH Open document ID: 0771.03004
DOI: 10.1016/0304-3975(92)90306-Z
author: Mariangiola Dezani-Ciancaglini
author: J. Roger Hindley
published in: Theoretical Computer Science
publication date: 1993-01-17T00:00:00Z
review text: The \(\to\) based type-language for \(\lambda\)-calculus was extended in 1977 by adding a universal type \(\omega\) and a connective \(\cap\) for the intersection of two types. This system, when suitably axiomatised, has the following desirable properties. (i) The set of types given to a \(\lambda\)-term does not change under \(\beta\)-conversion. (ii) The sets of normalizing and solvable \(\lambda\)-terms can be characterized neatly by the types of their members. (iii) \(\lambda\)-models can be built in which the interpretation of a \(\lambda\)-term coincides with the set of all types that can be assigned to it. The authors now propose an extension of the Curry style type assignment system for combinators to include \(\omega\) and \(\cap\) and they prove that, given certain conditions on combinator bases and abstraction algorithms, an exact equivalence between \(\lambda\) terms and combinators with intersection types can be achieved. As a result (i), (ii) (for strong reduction) and (iii) hold for combinators with intersection types. The conditions mentioned are satisfied by the most commonly used bases and abstraction algorithms. In the \(\lambda\)-system of intersection types the rule (\(\leq\)) can be replaced by a typed version of rule \((\eta)\). The authors present a combinatory logic version of this altered system, but this extension of typed combinatory logic is not so simple, but then neither was the extension from weak to \(\beta\eta\)-equality for untyped combinatory logic.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 96044
zbMATH Keywords: extension of the Curry style type assignment system
zbMATH Keywords: equivalence between \(\lambda\) terms and combinators with intersection types
zbMATH Keywords: combinatory logic
reviewed by: Martin W. Bunder
describes a project that uses: Forsythe
MaRDI profile type: Publication
cites work: Q3342534
cites work: A filter lambda model and the completeness of type assignment
cites work: Q3221961
cites work: Functional Characters of Solvable Terms
cites work: Type theories, normal forms, and \(D_{\infty}\)-lambda-models
cites work: Q5565113
cites work: Combinatory Reductions and Lambda Reductions Compared
cites work: Standard and Normal Reductions
cites work: Q3659755
cites work: Types with intersection: An introduction
cites work: Q4722037
cites work: Abstraction problems in combinatory logic: A compositive approach
cites work: Characterization theorems for a filter lambda model
cites work: Principal type schemes for an extended type theory
cites work: Another algorithm for bracket abstraction
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
Wikidata QID: Q126989194
full work available at URL: 0304-3975(92)90306-z
OpenAlex ID: W1966026637
description: scientific article; zbMATH DE number 96044