Intersection types, \(\lambda\)-models, and Böhm trees. (English) Zbl 0946.03016

Takahashi, Masako (ed.) et al., Theories of types and proofs. Based on the workshop, Tokyo, Japan, September 1997. Tokyo: Mathematical Society of Japan. MSJ Mem. 2, 45-97 (1998).
The paper under review offers a thorough introduction to the syntax and the semantics of type assignments systems, which comprise the so-called intersection types and were introduced by the Turin school already in the late seventies. Since then, intersection types have become a basic tool for characterizing fundamental proof-theoretic properties of terms in the pure (untyped) lambda calculus, as well as for devising a semantics of the untyped lambda calculus (via the technique of filter lambda models). Besides the natural function space constructor \(\rightarrow\), the main type assignement systems of this paper comprise a new type constructor \(\land\), which plays the role of a lattice-theoretic meet. Consequently, the typical feature of the intersection type \(\sigma \land \tau\) is that it can be assigned to a term \(M\) if and only if \(M\) possesses both types \(\sigma\) and \(\tau\) (this should be contrasted with the rule characterizing the cartesian product as type constructor).
Sections 1-6 comprise a description of the system CDV; besides \(\land\), CDV allows a universal type \(\omega\). Section 2 offers examples of type assignments; typically, CDV can assign types to terms that usually require recursive types (like the paradoxical combinator or the selfapplication operation). Of course, type assignments in CDV are preserved by \(\beta\) reduction (section 3). Sections 4-5 deal with the notions of head normal form (hnf) and approximant. The informal idea is that hnfs formalize the notion of partially computed result, while the set of approximants of a given term \(M\) represents all possible partial results of computations of terms beta convertible to \(M\). The approximation theorem 5.2 ensures that we do not miss any type assignable to a given term by looking to its approximants.
Section 6 illustrates the main theoretical motivation of CDV: the characterization Theorems 6.1-6.3 for the classes of solvable, normalizable and strongly normalizable terms. An important virtue of intersection types is that they can be naturally supplemented with a subtyping relation \(\sigma \leq \tau\) and subtyping turns out to be important for object-oriented languages. Sections 7-9 discuss extensions of CDV by subtyping. The main system BCD consists of a type assignment system in the proper sense together with axioms and rules for the subtyping relation \(\leq\) (assumed as primitive). BCD can account for the \(\eta\)-rule, it still enjoys the approximation Theorem and it yields a smoother characterization Theorem (solvable terms are the terms typable with types different from \(\omega\); normalizable terms are the terms typable with types not containing \(\omega\); strongly normalizable terms are the terms typable without using \(\omega\) in the derivation).
Section 10 contains an introduction to the semantics of type assignments and to lambda models (introduced as reflexive objects in the category of complete algebraic lattices); types are interpreted as (possibly non-computable) subsets of lambda models and a soundness theorem is proved. Section 11-12 investigate the so-called filter lambda models and present a completeness theorem for type assignments induced by BCD. The key notion is the notion of extended applicative type structures \(\mathcal{A}\) (EATS for short); roughly, an EATS is the abstract counterpart of a model of intersection types with subtyping. The collection \(\mathcal{F}(\mathcal{A})\) of filters over an EATS \(\mathcal{A}\) can be endowed with an applicative structure, which becomes a lambda model (the filter lambda model over \(\mathcal{A}\)) under an additional continuity constraint of \(\mathcal{A}\) (12.4). It turns out that the canonical EATS \(\mathcal{T}\) associated to BCD is continuous and that the set of types derivable for a term \(M\) in BCD just coincides with the denotation of \(M\) in the filter lambda model over \(\mathcal{T}\), and this readily leads to completeness (theorem 11.5). Section 13 contains a new result, relating types and Böhm trees (BTs for short; BTs represent in tree form the stable relevant information that can be extracted from a term \(M\) by computing it). The problem the authors address is to use the type system BCD for distinguishing terms having distinct BTs. This is solved by means of the notion of principal pair of an \(\eta\)-approximant and proving an appropriate theorem (13.3) to the effect that, if a term has an approximant \(A\) with type \(\tau\) in the context \(\Gamma\), where \((\Gamma, \tau)\) is the principal pair of \(A\), but \(\neg A \sqsubseteq_{\eta} A'\) (\(\sqsubseteq_{\eta}\) being the natural partial ordering on BTs), then \(A'\) cannot have the type \(\tau\) in the context \(\Gamma\). The approximation theorem for BCD then easily allows to discriminate terms with different BTs. The theorem has also a nice semantical application, as it yields a new proof of the theorem, characterizing the lambda theory of the filter model induced by BCD by means of equality of BTs.
Reviewer’s remark. The paper guides the reader through twenty years of results in an area of strategic interest, where several techniques and notions merge together, ranging from the foundations of functional programming to proof theory and mathematical logic in general. The choice of intersection types is motivated by a number of results, which are clearly spelled out by the authors in a readable and informal style: indeed, technical notions and definitions are wisely intertwined with examples and heuristic considerations. A number of proofs of fundamental results in the area are also outlined. We find that the paper fully satisfies its introductory and expository aim.
Page \(70^{13}\): table 8 does not exist.
For the entire collection see [Zbl 0919.00041].


03B40 Combinatory logic and lambda calculus
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations