Intersection types for combinatory logic (Q1199823)

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.