Solving equations in lambda-calculus. (English) Zbl 0686.03009
Logic colloq. ’88, Proc. Colloq., Padova/Italy 1988, Stud. Logic Found. Math. 127, 139-160 (1989).
[For the entire collection see Zbl 0673.00007.]
The paper reviews the solvability problem for some classes of equations and equation systems encountered in \(\lambda\)-calculus and combinatory logic. Particular emphasis is given to the problems of discriminability, separability and X-separability of terms, which are proved to be special cases of the problem of satisfiability of the predicate “the set of terms F is X-weakly separable”, whose solvability is characterized in the paper itself.
Undecidability results are given for some classes of systems of equations, together with partial characterizations of the one-side invertibility problems for \(\lambda\)-terms. Some open problems have been solved in a subsequent work by the second and the third author [Regular systems of equations in \(\lambda\)-calculus, in: Proc. Third Italian Conf. Theor. Comput. Sci., Mantova, 373-384 (World Scientific 1989)].
The paper reviews the solvability problem for some classes of equations and equation systems encountered in \(\lambda\)-calculus and combinatory logic. Particular emphasis is given to the problems of discriminability, separability and X-separability of terms, which are proved to be special cases of the problem of satisfiability of the predicate “the set of terms F is X-weakly separable”, whose solvability is characterized in the paper itself.
Undecidability results are given for some classes of systems of equations, together with partial characterizations of the one-side invertibility problems for \(\lambda\)-terms. Some open problems have been solved in a subsequent work by the second and the third author [Regular systems of equations in \(\lambda\)-calculus, in: Proc. Third Italian Conf. Theor. Comput. Sci., Mantova, 373-384 (World Scientific 1989)].
Reviewer: A.Piperno
MSC:
| 03B40 | Combinatory logic and lambda calculus |
