Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

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

Authors: Corrado Böhm Adolfo Piperno


Given a finite set T≡{T1, . . . ,Tt} of terms of the λ-β-K-calculus and a set XT≡{x1, . . ., xn} of free variables (occurring in the elements of T), XT-separability is the problem of deciding whether there exists a simultaneous substitution for the elements of X T transforming T into the set Z≡{Z1, . . . Zt} of arbitrary terms. The XT-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≡λx1 . . . 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


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