On sets of terms having a given intersection type

TL;DR

This paper explores the properties of sets of terms with specific intersection types, proving that strongly normalizing terms have unique typings and that such sets can form numeral systems, advancing the understanding of intersection type systems.

Contribution

It introduces the concept of uniqueness typing for strongly normalizing terms and analyzes the structure of sets of terms with given intersection types, including their algebraic and numeral system properties.

Findings

Every strongly normalizing term admits a unique intersection type.

The set of closed terms with a given type is uniformly separable.

Infinite sets of terms with a given type can form an adequate numeral system.

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 $(\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.