摘要：Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri (CDV) [CDV81], 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 (Γ, A) such that ● Γ ⊢ M ∶ A ● Γ ⊢ N ∶ A Ô⇒ M =βη 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.
