一句话：证明每个强规范化 λ 项都有唯一交集类型，并揭示给定类型闭项集的可分离性与数字系统性质。
本文在 Coppo、Dezani-Ciancaglini 与 Venneri（1981）交集类型指派系统的一个变体中，研究具有给定交集类型的 λ 项集合。作者首先讨论交集类型代数的若干表示及相应类型指派规则的选择，并利用内部化的 Böhm-out 技术分析给定交集类型下的项。主要结果是：每个强规范化项 M 都存在唯一类型（uniqueness typing）(Γ,A)，使得 Γ⊢M:A，且任何满足 Γ⊢N:A 的项 N 都与 M 在 βη 下相等。此外，具有给定类型的闭项集是一致可分离的；若该集合无限，则构成一个 adequate numeral system。
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair $(\Gamma,A)$ such that 1) $\Gamma \vdash M : A$ 2) $\Gamma \vdash N : A \Longrightarrow M =_{\beta\eta} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules. Moreover, we show that the set of closed terms with a given type is uniformly separable, and, if infinite, forms an adequate numeral system. The proof of this fact uses an internal version of the B\"ohm-out technique, adapted to terms of a given intersection type.