## Paper: X-Separability and Left-Invertibility in lambda-calculus (at LICS 1987)

**Corrado Böhm Enrico Tronci**

### Abstract

The separability problem is: given a finite set
*F≡{M _{1},..,M_{n}*} of λ-terms to find a
context C[ ] such that C[

*M*]=y

_{i}_{i}(i=1,..,n), where the y

_{i}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 charcaterized 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 ΔM

_{i}=y

_{i}(i=1,..,n) (this is Böhm's theorem) but also such that Δ Δ =y

_{0}! 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.

### BibTeX

@InProceedings{BhmTronci-XSeparabilityandLef, author = {Corrado Böhm and Enrico Tronci}, title = {X-Separability and Left-Invertibility in lambda-calculus}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {320--328 }, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }