IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Second Annual IEEE Symposium on

Logic in Computer Science (LICS 1987)

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

Authors: Corrado Böhm Enrico Tronci


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 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 Δ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.


    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}

Last modified: 2018-06-2121:59
Andrzej Murawski