[Prev][Next][Index][Thread]
Logic colloq '88
Here are my current title and abstract.
Constructive comments appreciated.
Solving equations in lambda-calculus
C.Boehm, A.Piperno and E. Tronci
Dpt.of Mathematics
Univ. of Roma "La Sapienza",Italy
Abstract
Equational theories like type-free lambda calculus and combinatory logic have
shown their power in computer science, allowing terms to represent data
as well as programs and offering general solutions to fixpoint equations for
recursive or explicitly defined functions. In the last 20 years
important theoretical results have been obtained solving systems of
equations of shape
(1) x M_i = y_i (i=1,..,n)
where the M_i's are known terms,the unknown x does not occur in M_i,
and y_i is an arbitrary variable.
A strong increase of generality is achieved considering
systems of shape
(2) M_i x_1..x_h = y_i (i=1,..,n)
where h is a (fixed) positive integer and the y_i's are not necessarily
pairwise different.
In this work the solvability of such systems is characterized.
Many problems that arise in lambda-calculus can be stated and
characterized specializing a system of equations of shape (2).
Typical examples are:
- X-separability, i.e. requiring that the y_i's are pairwise different;
- Separability, i.e. not fixing h but only assuming that h is'large enough';
- Boehm's theorem,i.e. separability with the assumption that the M_i's
are pairwise nonconvertible beta-eta-normal forms;
- surjectivity, left- and right-invertibility of combinatory mappings;
- the searching for a singleton basis for the combinatory logic.
Furthermore, a single equation can be solved via a system
of equations. Using this idea beta-eta-left-invertibility is
characterized for a class of lambda-terms.
_______________