Discriminators in Lambda Calculus

Abstract

The paper treats the problems of discriminability and separability for a wide class of infinite sets of terms in the pure lambda calculus. The technique used is a generalization of the Bohm out technique for extracting substitutional instances from the sets of terms. A unification of this technique on an appropriate class of terms enables the construction of an algorithm of extraction which leads to the construction of a discriminator for an infinite set of terms having the distinctive paths. In [11] some conditions under which a r.e. set of terms is a numeral system were done. For the opposite direction, i.e. construction of the distinctive paths for the discriminable or separable set of terms, we used the sequentiality and continuity theorem with a combination of a slight generalization of the Wadsworth's version of the lambda calculus (cf. [8]). The connection between the semantic notion of discriminability and the syntactic notion of distinctiveness, as known in the case of finite sets of terms, is extended here to the class of terms on which the (generalized) Bohm out technique can be applied.