A note on discriminability of lambda terms (Q2785599)

Discriminable sets of \(\lambda\)-terms, i.e. sets whose elements are internally distinguishable in the lambda-calculus, are used for representing some kinds of data (for example keys) in the lambda-calculus. We treated the problem of discriminability exhaustively in ``Discriminators in lambda calculus'' [J. Comput. Inf. Technol. 3, No. 4, 255-277 (1995)], where we constructed discriminators for sets of \(\lambda\)-terms whose subterms of members have bounded orders and bounded degrees on some subtrees of their Böhm trees. Nevertheless the problem of characterizing discriminable sets remains still open. While degrees of members of a discriminable set can be unbounded (see 3.7. in the paper cited above) we prove in this paper that their orders must be bounded. This result is a generalization of the fact that the set \(\{K^nI\mid n\in\mathbb{N}\}=\{\lambda x_0\dots x_n.x_n\mid n\in\mathbb{N}\}\), where \(K=\lambda xy.x\), is not discriminable [see \textit{H. P. Barendregt}, The lambda calculus. Its syntax and semantics. Revised edition (1984; Zbl 0551.03007), 20.3.2].