Equational programming in λ-calculus via SL-systems. Part 2

A system of equations in the λ-calculus is a set of formulas of Λ (the equations) together with a finite set of variables of Λ (the unknowns). A system s is said to be β-solvable (βη-solvable) iff there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the equations of s theorems in the theory β (βη). A system s can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for s yields executable codes for such programs.

A class of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for defines a compiler for such language.

This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form , wherex is an unknown and z is a free variable which is not an unknown.

It is known that the β (βη)-solvability problem for SL-systems is undecidable.

Here we show that there is a class of SL-systems (NP-regular SL-systems) for which the β-solvability problem is NP-complete. Moreover, we show that any SL-system s can be transformed into an NP-regular SL-system s. This transformation consists of adding abstractions to the LHS occurrences of the RHS variables of s. In this sense NP-regular SL-systems isolate the source of undecidability for SL-systems, namely: a shortage of abstractions on the LHS occurrences of the RHS variables.

NP-regular SL-systems yield an equational programming language in which unrestrained 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. However, existence of executable code satisfying a specification in such language is an NP-complete problem. This is the price we have to pay for allowing unrestrained self-application in our language.