Formal Design of an Abstract Machine for Constraint Logic Programming

Christoph Beierle^{a}

aFachbereich Informatik, Fernuniversität Hagen, D-58084 Hagen, Germany e-mail: Christoph.Beierle@fernuni-hagen.de

Abstract: By studying properties of CLP over an unspecified constraint domain X one obtains general results applicable to all instances of CLP(X). The purpose of this paper is to study a general implementation scheme for CLP(X) by designing a generic extension WAM(X) of the WAM and a corresponding generic compilation scheme of CLP(X) programs to WAM(X) code which is based on Börger and Rosenzweig’s WAM specification and correctness proof. Thus, using the evolving algebra specification method, we obtain not only a formal description of our WAM(X) scheme, but also a mathematical correctness proof for the design.^{∗}

Keyword Codes: D.1.6, F.3.1 Keywords: Logic Programming, Specifying and Verifying about Programs

[To appear in: B. Pehrson, I. Simon (eds): Proceedings of the IFIP Congress 94, Elsevier, Amsterdam, 1994]

1. INTRODUCTION

Recently, Gurevich’s evolving algebra approach has not only been used for the description of the (operational) semantics of various programming languages (Modula-2, Occam, Prolog, Prolog III, Smalltalk, Parlog, C; see [9]), but also for the description and analysis of implementation methods: Börger and Rosenzweig [6] provide a mathematical elaboration of Warren’s Abstract Machine [14,1] for executing Prolog. The description consists of several refinement levels together with correctness proofs, and a correctness proof w.r.t. Börger’s phenomenological Prolog description [5]. Based on Börger and Rosenzweig’s WAM description, [2] provides a mathematical specification of the PAM, a WAM extension to type-constraint logic programming, and proves its correctness w.r.t. PROTOS-L, a logic programming language with polymorphic order-sorted types [4]. [7] extends the correctness proof in [6] to the compilation of CLP(R) programs to the Constraint Logic Arithmetic Machine (CLAM) [12], [11]. These approaches demonstrate how the evolving algebra approach naturally allows for modifications and extensions in the description of both the semantics of programming languages as well as in the description of implementation methods.

However, both [2] and [7] aim at the specification and verification of specific systems that are within the constraint logic programming paradigm. CLP(R) is a particular instance (by arithmetic constraints over the real numbers) of CLP [10], a framework for constraint handling in logic programming; similarly, the type constraints of PROTOS-L could be seen as an instance CLP(T YPE). On the other hand, many other approaches to constraint logic programming can be seen as instances of CLP. E.g., Trilogy [13] could be viewed as CLP(Z), or Prolog III [8] could be viewed as instantiating CLP by constraints over boolean and rational terms. Thus, by studying properties of CLP over an unspecified constraint domain X (denoted by CLP(X) in the sequel) one obtains general results applicable to all instances of CLP(X). The purpose of this paper is to study a general implementation scheme for CLP(X) by designing a generic extension WAM(X) of the WAM and a corresponding generic compilation scheme of CLP(X) programs to WAM(X) code. Based on the mathematical WAM specification and correctness proof in [6], we extend the work of [2] to general constraints. Thus, we obtain not only a formal description of our WAM(X) scheme, but also a mathematical correctness proof for the design.

∗Acknowledgements: I am most grateful to Egon Börger for many fruitful and encouraging discussions; the research reported here has profited very much from our joint work described in [2] and [3].

Although in this paper we keep the domain X of constraints abstract, we will provide one further step of reuse of logic programming and WAM technology (and of the evolving algebra specification of [6] as well). Since a constraint solver for X also gives us a constraint solver for equational constraints in T_{Σ}(X), the algebra of freely generated terms over X, we will consider such constraints over T_{Σ}(X). The equational constraint solving part will be done by term unification properly extended to interface with the (non-equational) constraint solver over X. An important aspect of this paper will thus be the exact specification of the interaction between the unification part (which will be refined down to the basic WAM level, representing one of the major WAM principles) and the - still abstract - general constraint solver. For notational convenience we will, however, stick to the names CLP(X) and WAM(X). Furthermore, we assume that the reader is familiar with the WAM and the WAM specification given in [6]. For further details of the WAM(X) specification we refer to [3].

2. AN ABSTRACT NOTION OF CONSTRAINTS

The basic universes and functions in CLP(X) algebras dealing with terms and substitutions are taken directly from the standard Prolog algebras. For a formalization of constraints - in the spirit of constraint logic programming - we introduce a new abstract universe X-CONSTRAINT, connected to terms via the function

dom: X-CONSTRAINT → VARIABLE ^{∗}

yielding all variables occurring in an X-CONSTRAINT, called the domain of a constraint. Constraints are then defined as equations or (X-)constraints, i.e.

CONSTRAINT ⊆ EQUATION ∪ X-CONSTRAINT

Let CSS denote the set of all sets of constraints together with nil ∈ CSS denoting an inconsistent constraint system. The unifiability notion of ordinary Prolog is now replaced by a more general (for the moment abstract) constraint solving function:

        solvable: CSS → BOOL

telling us whether the given constraint system is solvable or not. From every (solution of a) solvable constraint system we can extract a substitution part. Thus, we introduce a function

solution: CSS → SUBST × CSS ∪ {nil}

where solution(CS) = nil iff solvable(CS) = false. For the trivially solvable empty constraint system we have solution(∅) = (∅,∅) and the functions

        subst part: CSS → SUBST
        cs part:  CSS → CSS

are the two obvious projections of solution. Since we want to consider equational constraints over the term algebra T_{Σ}(X) freely generated over X, we have to express that in solution(CS) = (s,c) the two solution components s and c are compatible with this requirement. That is, either the domains of s and c are disjoint, or, if a variable x is in both domains, in the substitution part it can only be identified with another variable since as a constraint variable it must still be a free variable. Thus we require:

        if solution(CS) = (s,c) ≠ nil then
           ∀ x ∈ dom(s) ∩ dom(c) . ∃ y ∈ VARIABLE .

x≐ y ∈ s and, if y ∈ dom(c), then x = y in any interpretation of c.

Having refined the notions of unifiability and substitution to constraint solvability and (solvable) constraint system, respectively, we can now also refine the related notion of substitution result to terms with constrained variables. The latter involves three arguments:

1. a term t to be instantiated,

2. constraints for the variables of t (and possibly other variables) given by ct, and 3. a constraint system CS (containing in general also a substitution part) to be applied.

Since a CS-solution consists of an ordinary substitution sCS together with constraints cCS via solution(CS) = (sCS, cCS), the result of the constraint application can be introduced by

        conres(t, ct, CS) = (t_{1}, c_{1})

as a pair consisting of the instantiated term t_{1} and constraints c_{1}. For this function

conres: TERM × CSS × CSS → TERM × CSS ∪ {nil}

we impose the following integrity constraints:

∀ t ∈ TERM, ct ∈ CSS, CS ∈ CSS .

        if solvable(ct ∪ CS) then
                                  conres(t, ct, CS) = (t_{1}, c_{1})

where:

                                  t_{1} = subres(t,subst part(ct ∪ CS))
                                  c_{1} = cs part(ct ∪ CS)

else

                                  conres(t, ct, CS) = nil

Thus, the condition that a constraint system CS “can be applied” to a term t with variables constrained by ct means that ct is compatible with CS, i.e. solvable(CS ∪

ct) = true.

3. CLP(X) ALGEBRAS WITH COMPILED AND / OR STRUCTURE

As our starting point we can take CLP(X) algebras with compiled AND/OR structure. This is motivated by the fact that the constraint mechanism is orthogonal both to the compilation of the predicate structure (OR structure) as well as to the compilation of the clause structure (AND structure). Leaving the notion of terms and substitutions as abstract as in 2, we can use the compiled AND/OR structure development for Prolog in [6] which was also used for PROTOS-L in [2] and for CLP(R) in [7]. Essentially we just have have to replace substitutions (resp. substitutions with type constraints) by the more general constraint systems, where the new instruction add constraint enlarges the current constraint system accumulated so far.

4. TERM REPRESENTATION

The representation of terms and substitutions in the WAM(X) can be introduced in several steps. Following the development in [6] we first introduce the treatment of the low-level run-time unification but we keep the (non-equational) constraints completely abstract. Thus, in the WAM(X) algebras to be developed here we introduce a 0-ary function xcs holding the current non-substitutional constraint system accumulated so far. The only deviation from the WAM’s resp. PAM’s term representation is that we want to distinguish between data area locations l representing free variables with no constraints at all (tag(l) = VAR) and free constrained variables (tag(l) = CVAR).

4.1. Unification

Low-level unification in the WAM(X) can be carried out as in the WAM (see [1]) if we refine the bind operation into one that takes into account also the constraints of the variables (see [4] for the case of type constraints). The bind operation may thus also fail and initiate backtracking if the constraints are not satisfied. Thus, we can use the treatment of unification as described in [6], while leaving the bind operation abstract for the moment, not only in order to postpone the discussion of occur check and trailing but also to stress the fact that the bind operation will take care of the constraints for the variables. For the abstract bind update we impose the following modified

BINDING CONDITION 1: For any l_{1}, l_{2}, l ∈ DATAARRA with unbound(l_{1}), with term, term' values of term(l) before and after execution of bind(l_{1},l_{2}), we have: If

        xcs' = xcs ∪ {mk var(l_{1})≐ term(l_{2})}

is solvable, then term' = conres(term, xcs') and cs part(xcs’) will be the new value of xcs; otherwise backtracking will be executed.

With this generalized binding assumption we easily obtain a correspondingly modified unification lemma, expressing the effect of the unify(l_{1},l_{2}) update.

4.2. Getting of terms

Whereas the compilation of body goals and the required term creation by putting instructions does not involve unification and thus remains unchanged, the getting of terms does involve unification. Parts of it are compiled into the getting instructions (like get structure followed by a sequence of unify instructions) and the remaining unification tasks are handled by the low-level unify procedure.

The get value, unify value, and unify variable instructions are as in the WAM or the PAM case. The first get structure rule for WAM(X) is still as before, covering the situation when in get structure(f,x_{i}) x_{i} is bound to a non-variable term. When x_{i} is unbound, it must be bound to a newly created term with top-level symbol f. Whereas in the WAM this will always succeed, in the WAM(X) case a possible constraint of x_{i} must be taken into account:

                if RUN
                  & code(p) = get structure(f,x_{i})
                  & unbound(deref(x_{i}))
                  & NOT(constrained(x_{i}))    | constrained(x_{i})

then

                  h ← <STRUC,h+>           | backtrack
                  bind(deref(x_{i}),h)         |
                  val(h+) := f              |
                  h := h++                  |
                  mode := Write             |
                  succeed                   |

The Getting Lemma now takes into account the constraint system accumulated in xcs.

4.3. Putting of Constraints

The compile function is refined to issue a new put constraint instruction (for realization of add constraint of Section 3):

                if RUN & code(p) = put constraint(C)
                then addtoxcs(ρ(C))

where ρ is the variable renaming substitution {Y_{i} ≐ mk var(y_{i}) | i=1,…,l}, vars(C) = {Y_{1},…,Y_{l}}, and where the crucial addtoxcs update must satisfy the ADD CONSTRAINT CONDITION: For any l ∈ DATAAREA with term, term' values of term(l) before and after execution of addtoxcs(C) we have: If xcs' = xcs ∪ {C} is solvable then term' = conres(term,xcs') and cs part(xcs’) will be the new value of xcs, and any of the variables in vars(C) will be tagged as a constraint variable (i.e. constrained(deref(y_{i})); otherwise backtracking will be executed.

5. CLP(X) ALGEBRAS

5.1. Environment and Choicepoint Representation

The stack of states and environments of CLP(X) algebras remains unchanged except that we extend the choice point information by a location xcs(l) ≡ l - 6 to hold the current (non-equational part of the) constraint system. It is stored in the stack when a new choice point is created (by executing a try me else or try instruction) and retrieved when updating or removing a choice point (by a retry[ me else] or trust[ me else] instruction).

5.2. Trailing

Trailing is done exactly as in the PAM, i.e. compared to the WAM not only the location l but also its value val(l) is trailed and recovered upon backtracking, ensuring that VAR and CVAR tags are restored correctly. While still leaving the binding update abstract, we pose the following

TRAILING CONDITION: Let l_{1}, l_{2}, l ∈ DATAAREA, C ∈ CSS. If val(l) before execution of bind(l_{1},l_{2}) (resp. addtoxcs(C)) is different from val(l) after successful execution of bind(l_{1},l_{2}) (resp. addtoxcs(C)), then the location l has been trailed with trail(l).

For the WAM(X) algebras developed so far from CLP(X) algebras with compiled AND/OR structure we can now generalize the “Pure Prolog Theorem” of [6].

5.3. Additional WAM optimizations in the WAM(X)

Environment trimming and last call optimization (LCO) are among the most prominent optimizations in the WAM; other crucial points in the WAM design is the classsification of variables into temporary and permanent variables, as well as their initialization “on the fly”, or the indexing methods. For a discussion of these aspects we refer to [1] and [6]. In the case of type constraints we showed in [2] how the treamtment of these WAM optimizations in [6] carried over to the PAM, including the realization of the Cut operator. The same argumentation applies to the WAM(X) extension since no constraint related actions are involved, allowing us to extend the correctnes theorems of [6] to the full WAM(X) with all WAM characteristics like environment trimming, LCO, or indexing.

REFERENCES

1. H. Aït-Kaci. Warren’s Abstract Machine: A Tutorial Reconstruction. MIT Press, Cambridge, MA, 1991.

2. C. Beierle and E. Börger. Correctness proof for the WAM with types. In E. Börger, H. Kleine Büning, G. Jäger, and M. M. Richter, editors, Computer Science Logic - CSL’91, volume 626 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992.

3. C. Beierle and E. Börger. Evolving algebra specification of an abstract machine for constraint logic programming. Technical Report, FernUniversität Hagen, 1994. (to appear).

4. C. Beierle and G. Meyer. Run-time type computations in the Warren Abstract Machine. The Journal of Logic Programming, 18(2):123–148, February 1994.

5. E. Börger. A logical operational semantics of full Prolog. Part I. Selection core and control. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, CSL’89 - 3rd Workshop on Computer Science Logic, volume 440 of Lecture Notes in Computer Science, pages 36–64. Springer-Verlag, Berlin, 1990.

6. E. Börger and D. Rosenzweig. The WAM - definition and compiler correctness. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence. North-Holland, 1994. (to appear).

7. E. Börger and R. Salamone. CLAM specification for provably correct compilation of CLP(R) programs. In E. Börger, editor, Specification and Validation Methods for Programming Languages and Systems. Oxford University Press, 1994. (to appear).

8. A. Colmerauer. An introduction to Prolog-III. Communications of the ACM, 33(7):69–906, July 1990.

9. Y. Gurevich. Evolving algebras. A tutorial introduction. EATCS Bulletin, 43, February 1991.

10. J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proceedings of the 14th ACM Symposium on Principles of Programming Languages, pages 111–119. ACM, January 1987.

11. J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. An abstract machine for CLP(R). Technical report, IBM Research Devision, 1992.

12. J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) language and system. ACM TOPLAS, pages 339–395, July 1992.

13. P. Voda. The constraint language Trilogy. Technical report, Complete Logic Systems, North Vancouver, BC, Canada, 1988.

14. D. H. D. Warren. An Abstract PROLOG Instruction Set. Technical Report 309, SRI, 1983.