## Paper: Characterizing X-separability and one-side invertibility in λ-β-Θ-calculus (at LICS 1988)

**Corrado Böhm Adolfo Piperno**

### Abstract

Given a finite set T≡{T_{1}, . . . ,T_{t}} of terms of the λ-β-K-calculus and a set X_{T}≡{x_{1}, . . ., x_{n}} of free variables (occurring in the elements of T), X_{T}-separability is the problem of deciding whether there exists a simultaneous substitution for the elements of X _{T} transforming T into the set Z≡{Z_{1}, . . . Z_{t}} of arbitrary terms. The X_{T}-separability problem is proved to be solvable for any approximation T^{#} of the set T by terms in λ-β-Θ-normal form. Since the characterization is constructive, if the terms T^{,#}_{i}≡λx_{1} . . . x _{n}. T^{#}_{i} (i=1, . . ., t) are closed then the sequence T^{#}_{1 }, . . ., T^{#}_{t} induces a family of mappings (from n to t dimensions) whose surjectivity and right-invertibility becomes decidable. The left-invertibility
of this family is proved to be decidable too

### BibTeX

@InProceedings{BhmPiperno-CharacterizingXsepa, author = {Corrado Böhm and Adolfo Piperno}, title = {Characterizing X-separability and one-side invertibility in λ-β-Θ-calculus }, booktitle = {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)}, year = {1988}, month = {July}, pages = {91--101}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }