On sets of terms having a given intersection type
arXiv:1809.08169 · doi:10.46298/lmcs-18(3:35)2022
Abstract
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 such that 1) 2) 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öhm-out technique, adapted to terms of a given intersection type.