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

Authors: Corrado Böhm Adolfo Piperno

Abstract

Given a finite set T≡{T₁, . . . ,T_t} of terms of the λ-β-K-calculus and a set X_T≡{x₁, . . ., 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₁, . . . 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₁ . . . x _n. T^#_i (i=1, . . ., t) are closed then the sequence T^#₁ , . . ., 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}
  }