Intersection types for combinatory logic (Q1199823)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Intersection types for combinatory logic |
scientific article |
Statements
Intersection types for combinatory logic (English)
0 references
17 January 1993
0 references
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.
0 references
extension of the Curry style type assignment system
0 references
equivalence between \(\lambda\) terms and combinators with intersection types
0 references
combinatory logic
0 references