Equational programming in lambda-calculus via SL-systems .1.

A system of equations in the lambda-calculus is a set of formulas of Lambda (the equations) together with a finite set of variables of Lambda (the unknowns). A system L is said to be beta-solvable (beta eta-solvable) iff there exists a simultaneous substitution with closed lambda-terms for the unknowns that makes the equations of L theorems in the theory beta (beta eta). A system L can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for L yields executable codes for such programs. A class G of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for G defines a compiler for such language. This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form x (M) over right arrow = z, where x is an unknown and z is a free variable which is not an unknown. We show that the beta (beta eta)-solvability problem for SL-systems is undecidable. On the other hand we are able to define a class of SL-systems (regular SL-systems) for which the beta-solvability problem is decidable in Polynomial Time. Such class yields an equational programming language in which self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way.