X-separability in lambda-calculus

The separability problem is: given a finite set F≡{M1,..,Mn} of λ-terms to find a context C[ ] such that C[Mi]=yi (i=1,..,n), where the yi are arbitary variables. Solvability of such a problem has been fully studied ten years ago. Replacing free variables belonging to a set X of cardinality w by suitable terms thoughout F is the same as using only contexts having the structure ΔX[]≡(λ X.[]) Δ1 .. Δw. This induces a new problem: the X-separability problem which solvability is constructively characterized in the paper for a class of λ-terms. The major difficulty surmounted is the treatment of self-application. A typical result arises if F consists of mutually distinct β-η-normal closed forms. In such a case not only Δ exists such that ΔMi=yi (i=1,..,n) (this is Böhm's theorem) but also such that Δ Δ =y0! Another example of self-recognition is exhibited in the paper. The problem of the β-η-left-invertibility is also faced and a class of λ-terms has been recognized which are β-η-left-invertible iff a relates set of terms is β-η-X-separable.