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

Authors: Corrado Böhm Enrico Tronci

Abstract

The separability problem is: given a finite set F≡{M₁,..,M_n} of λ-terms to find a context C[ ] such that C[M_i]=y_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.[]) Δ₁ .. Δ_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₀! 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}
  }