Operational Semantics of Constraint Logic Programs with Coroutining ^{1}

Andreas Podelski^{2}

Max-Planck-Institut für Informatik Im Stadtwald, D-6123 Saarbrücken, Germany

podelski@mpi-sb.mpg.de

Gert Smolka

Programming Systems Lab German Research Center for Artificial Intelligence (DFKI) Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany

smolka@dfki.uni-sb.de

Abstract

The semantics of constraint logic programming languages with coroutining facilities (“freeze,” suspension, residuation, etc.) cannot be fully declarative; thus, an operational semantics has to be taken as the defining one. We give a formal operational semantics for a Prolog-like language with cut and entailment-based conditional. The difficulty here is to present the semantics in a form that abstracts away inessential details and highlights the interaction between language constructs. Our approach is derived from those used for concurrent calculi. We use abstract syntax trees, congruence laws and rewrite rules to define the semantics. A computation step is modeled as the application of a rewrite rule to an abstract syntax tree modulo structural congruence. This semantics serves as a defining tool for the language designer and as the interface between the language designer and implementor; it allows the programmer to check his intuition with a formal execution model and it gives him a performance measure for the execution of programs. We have used the semantics to make precise, for the first time, the critical interaction between sequential execution (including backtracking and cut pruning) and coroutining. In particular we exhibit cases where this interaction can lead to indeterministic results (i.e., to non-predictable program execution).

1Appeared in Proceedings of International Conference of Logic Programming (ICLP’95), Kanagawa, Japan, June 1995. Pages 449–463, editor Leon Sterling. MIT Press.

2partially supported by ESPRIT working group Nr. 8666 CONTESSA

1 Introduction

The logical semantics (“ ⊧ ≡ ⊢”) which has been given for logic programming languages [7, 6] has been one reason for their success. It presents these languages as executable specification languages. The declarative semantics becomes practically useful when, for example, programming search problems. These languages are, however, mainly used as programming languages which have declarative as well as purely operational functionalities (such as the ordering of goals, the cut operator, and facilities for coroutining which appear in one form or another^{3} in most CLP- or Prolog-Systems. Also, it is well known that the formal correspondence between declarative and operational semantics is lost even for the “pure” subset of practical language implementations. Thus, the semantics cannot be fully declarative, and we have to take an operational semantics as the defining one.

To achieve the definition of an operational semantics is not difficult in principle; one need only formalize an interpreter. The difficulty is to present the semantics in a form that abstract away inessential details and highlights the interaction between language constructs. The work in [3] gives the operational semantics of “freeze,” but on a very low-level; for example, it formalizes the stepwise search through the list of frozen goals. Such a low-level approach seems suitable for specifying and comparing language implementations, but not so much for designing and specifying the languages themselves. On a very high-level, declarative and operational semantics for comitted-choice languages have been given by Maher in [8], who captured guard satisfaction as constraint entailment. Similar in spirit is the work in [14] which considers a logic programming language with don’t-know choice and guarded rules.

In this paper, we give a short, simple and formally precise description of the operational semantics of logic programs with coroutining facilities. In comparison with [3], our semantics is high-level. In contrast to [3], it treats constraint handling logically . In contrast to [8, 14], our semantics accounts for order (of goals and alternatives), cut and eager wakening and ignores declarative semantics. Our approach is based on abstract-tree rewriting which appeared in a revised representation of the π-calculus [9] and was employed in [15, 16] to formulate calculi for higher-order concurrent constraint programming model. The abstract-tree rewriting model proves particularly useful for constraint programming since constraint propagation and simplification (for testing satisfiability as well as entailment) can be accommodated elegantly by means of the congruence on trees. This congruence is defined using the logical meaning of constraints. Thus, we model constraints logically, as is standard in CLP.

The next section introduces our general approach. Section 3 introduces the notions of constraints and predicate definitions and applications and considers simple programs, which are built up with the operators “ & ” and “ ; ”. Sections 4, 5 and 6 consider programs obtained by adding an operator, either “!”, “ ?” or “∃”, to simple programs. Section 7 considers the combination of all five operators. The article ends with a conclusion section.

3For example: “freeze,” suspension, residuation (negated constraints also introduce an implicit form of coroutining); cf. [5, 10, 11, 4, 1]).

2 The Approach

The ingredients of our semantics are (cf., Figure 1): BNF style rules to define the abstract syntax, reduction rules (“ ⟶ ”) for the operational and congruence laws (“ ≡ ”) for the declarative aspects.

The execution of a program is seen as a sequence of state transitions. The states are modeled by formulae (“continuations”) which are represented as trees as usual. A computation step is modeled as the application of a rewrite rule to an abstract syntax tree modulo structural congruence. Formally, the reduction relation “ ⟹ ” modeling the direct state transitions is an extension of the relation ⟶ given by the reduction rules, namely

\frac{C_{1} ≡ C′_{1}, C_{2} ≡ C′_{2}, C′_{1} ⟶ C′_{2}}{C[C_{1}] ⟹ C[C_{2}]}

for any context C (of the form defined in the corresponding definition) and configurations C_{1}, C′_{1}, C_{2}, C′_{2}. A context is a “tree with a hole;” C[C] denotes the tree obtained from C by putting the tree C into the hole. For example, for the contexts defined in Figure 1 we define •[C] = C and (•; C′)[C] = C; C′.

The trees are made abstract by a congruence. The idea is that congruent trees describe the same state. Formally, the relation ≡ is the congruence generated by the congruence laws.^{4}

The purpose of congruences is twofold: (1) They serve to make trees sufficiently abstract to suitably model states. For example, E_{1} ∧ (E_{2} ∧ E_{3}) and (E_{1} ∧ E_{2}) ∧ E_{3} are different trees; by making them congruent one can talk about the list of conjuncts written as E_{1} ∧ E_{2} ∧ E_{3}. (2) They serve to describe the effect of a functionality of the language on a high level (i.e., declaratively): Instead of modeling the effect through transitions between certain states, one identifies these states through the congruence. For example, we describe the effect of unification by a congruence law (Simplification). The implementation of the language has to ensure that these “hidden” transitions are possible when needed.

3 Simple Programs (“&” and “ ; ”)

We will motivate and explain the definition for the execution of simple programs in Figure 1 at hand of an example. We take the definition of the length predicate, length([],zero). length([HT],succ(N)) :- length(T,N). — and, hereby indicating how the systematic translation from concrete into

4This means, ≡ is the least equivalence relation which respects the congruence laws and the rule: If t_{1} ≡ t′_{1} and t_{2} ≡ t′_{2}, then t_{1} ∘ t_{2} ≡ t′_{1} ∘ t′_{2} for binary tree-composing symbols ∘, and accordingly for ternary ones.

SYNTAX

Expressions  E ::= φ | px̄ | E_{1} & E_{2} | E_{1} ; E_{2}
Configurations C ::= φ:E | ⊥ | C_{1} ; C_{2}
Contexts  C ::= • | C; C

REDUCTION RULES

Application Elaboration φ:px̄ & E ⟶ φ:x̄ = ȳ & E_{1} & E if pȳ ↔ E_{1} in program, V(φ:E) ∩ V(pȳ ↔ E_{1}) = ∅

Constraint Elaboration φ:φ_{1} & E \begin{matrix}⟶ & φ ∧ φ_{1} :E & if Δ |̸= φ ∧ φ_{1} ↔ ⊥, φ_{1} ≠ ⊤ \\ ⟶ & ⊥ & if Δ ⊧ φ ∧ φ_{1} ↔ ⊥ \end{matrix}

Or Elaboration φ:(E_{1} ; E_{2}) & E ⟶ (φ:E_{1} & E) ; (φ:E_{2} & E)

CONGRUENCE LAWS

Sequential And ({Expressions}, & , ⊤) is a monoid.
Sequential Or ({Configurations}, ; , ⊥) is a monoid.
Simplification φ_{1} ≡ φ_{2} if Δ ⊧ φ_{1} ↔ φ_{2}.

Figure 1: Simple Programs (“&” and “ ; ”)

abstract syntax works, translate it to the following syntactic formula.^{5}

length(x, n) ↔ ( \begin{matrix}(x = nil ∧ n = zero) ; \\ ((x = cons(y, z) ∧ n = succ(m)) & length(z, m)) ) \end{matrix}

We say that the predicate length(x, n) is defined by an expression E which is composed of sub-expression with the symbols “ ; ” (read: “Sequential Or”) and “ & ” (read: “Sequential And”). The atomic sub-expressions are either applications px̄ (here: length(z, m)) or constraints φ (here: x = cons(y, z) ∧ n = succ(m)). Constraints are themselves composed of atomic constraints with the symbol “∧” (read: “Logical And”).^{6}

In order to motivate the use of two “And” symbols now, we note that the difference between the two expressions x = f(y, a) ∧ y = a and x = f(y, a) & y = a corresponds to the difference between X=f(a,a) and X=f(Y,a), Y=a in Prolog syntax.^{7} In connection with coroutines, this difference has an operational significance (if the constraint y = a fails, coroutines may be fired in the second case, but not in the first; cf., Section 5).

The semantics is formally parametrized with a constraint system, which defines the syntax and the interpretation of the particular class of first-order logic formulae that we consider ‘constraints’. The constraint system consists of a signature (a set of first-order function symbols f and predicate symbols r) and a consistent first-order theory Δ. The theory can be given as the set of all sentences valid in a given structure; e.g., of finite trees. The abstract syntax of constraints φ is given below (the symbols ⊥ and ⊤ stand for the false and true constants).

5This is not yet a logical definition; i.e., the symbol “↔” does, for now, not have the logical reading “if and only if.” We omit the account of existential quantification until Section 6.

6We use x̄ as an abbreviation for a tuple of pairwise different variables.

7The formally correct expression corresponding to X=f(a,a) is ∃y∃z(x = f(y, z) ∧ y = a ∧ z = a).

Constraints φ ::= r(x̄) | x = y | x = f(ȳ) | ⊥ | ⊤ | φ_{1} ∧ φ_{2} | ∃xφ

The semantics uses the test of satisfiability of constraints (“Δ ⊧ φ ↔ ⊥”).^{8}

For modeling states, we use formulae called configurations C which are, for now, of the form φ: E , i.e., composed of a constraint store φ (a constraint) and a continuation E (an expression) by a symbol “:” (read: “Colon And”). The initial state is modeled as the configuration constituted by the “empty constraint store” ⊤ (standing for the true constraint) and the query expression; for example, if the query is length([a|Z],N), prime(N)?, as

\underbrace{⊤}_{constraint store} : \underbrace{(x = cons(y, z) ∧ y = a) & length(x, n) & prime(n)}_{continuation}

Concluding the introduction of syntax, we recapitulate that we have in total three “And” symbols: “:” for constituting configurations, “∧” to compose constraints, and “ & ” to compose expressions (which constitute continuations and the body of predicate definitions).

All state transitions must be authorized by a reduction rule. Since the first & -conjunct in the continuation is a constraint, we apply the Constraint Elaboration rule to obtain the successor state of the initial state:

\underbrace{⊤ ∧ (x = cons(y, z) ∧ y = a)}_{constraint store} : \underbrace{length(x, n) & prime(n)}_{continuation} .

Now, the first & -conjunct in the continuation is an atom, and we apply the Unfolding rule.

The first & -conjunct in the continuation being a ; -disjunction, we next apply the Or-Elaboration rule. Then, the configuration modeling the successor state is composed of two configurations by the “ ; ”-symbol. Each of the two has a copy of the constraint store and of the remaining conjuncts in the continuation.

Until now, states were represented by configurations of the form φ: E, and we could apply the reduction rules on these configurations in the empty context (which is noted “•”). Now, the configuration is of the form C; C′. Here, •; C′ is the context of C. Hence, we may apply a reduction rule on C; if this application yields C′′, then the configuration C; C′ reduces to the configuration C′′; C′. This means that the reduction of an “ ; ”-disjunction is realized by rewriting the first configuration-disjunct.

8In the example, the constraints correspond to the term equations in Prolog. They are interpreted over the logical structure Δ of finite trees. Here, The signature does not contain any predicate symbols r.

Here, since the first & -conjunct in the continuation is a constraint which is incompatible with the constraint store, the first continuation-disjunct reduces, by applying the Constraint-Elaboration rule, to the configuration ⊥ (the fail-configuration). Hence, we obtain the successor state modeled by a configuration of the form ⊥: C. Since the Sequential-Or congruence law postulates in particular that ⊥; C ≡ C (“⊥ is a neutral element for “ ; ”- composing configuration-disjuncts”), the configuration C models the same state.

In order to illustrate how we model constraint simplification declaratively (instead of using unification), we consider one more transition. Application of the Constraint-Elaboration rule yields the state which is modeled by the configuration:

x = cons(y, z) ∧ y = a ∧ x = cons(y, z) ∧ n = succ(m):length(z, m) & prime(n)

and which is modeled also by the following configuration which is congruent according to the Simplification congruence law.^{9}

(x = cons(y, z) ∧ y = a ∧ n = succ(m)):length(z, m) & prime(n).

To recapitulate and to compare with SLD-resolution, we model Leftmost-Selection through the form of the reduction rules and through the Sequential-And congruence laws (which say that an & -conjunction of expressions in a continuation forms an ordered sequence; i.e., the operator “ & ” is not commutative). We model the Topmost Selection rule through the definition of contexts and through the Sequential-Or congruence laws (i.e., “ ; ” is not a commutative operator on configuration-disjuncts).^{10} We model Success by the fact that the continuation of the first configuration-disjunct in a configuration is equal to ⊤. That is, the configuration is of the form φ : ⊤; C. A transition sequence coming to a state modeled by such a configuration terminates in this state.^{11} We model Failure by the fact that a configuration reduces to the fail-configuration ⊥ if the first & -conjunct in the continuation is a constraint which is is logically inconsistent with the constraint store. The fail-configuration may be the first configuration-disjunct in a configuration modeling an execution state. Then omitting the ⊥-disjunct yields a congruent configuration which models the same state. This is how we model Backtracking.

9The Simplification congruence law does not inflict on the reduction relation (since the Constraint Elaboration rule depends directly on the logical meaning of constraints). It is used for modeling the effect of the constraint solver. It will be used also in Section 6 for modeling the lifetime of local variables.

10The Sequential-Or congruence laws are formulated only for configurations. The Or-Elaboration rule implies, however, that one can apply them also to expressions without changing the semantics; i.e., an “ ; ”-disjunction of expressions may also written as their ordered sequence.

11We model the behavior of Edinburgh-style Prolog where further solutions have to be requested explicitly. Request of further solution amounts to failing the first alternative/configuration.

4 The Cut (“ !”)

We introduce the semantics defined in Figure 2, for Horn clauses with the addition of the cut operator (and still without the account of “∃”).

p(t1):- q1.
p(t2):- q21, !, q22, q23.
p(t3):- q3.
p(t4):- q4.

We translate the above predicate definition in concrete Prolog syntax with cut into the following one in abstract syntax:

p(x) ↔ (\underbrace{(x = t1 & q1)}_{clause before/} ; ! (\underbrace{x = t2 & q21}_{goals before/}, \underbrace{q22 & q23}_{after cut}, \underbrace{x = t3 & q3 ; x = t4 & q4}_{clauses after cut}) )

which uses expressions of the form !(E, E_{1}, E_{2}) , i.e., composed of three subexpressions (E, the cut-guard; E_{1} and E_{2}, the first and second alternatives) by the symbol “!” (read: “cut”). This symbol cannot given a logical meaning which corresponds to its operational semantics.

The translation above gives an idea on how such a translation can be done systematically. It is given for the first time in [13] for replacing cut by DEC-10 Prolog’s if-then-else operator (which is implemented unsoundly).

We will now define the operational semantics of cut-expressions. If an execution state is modeled by a configuration where the first conjunct in the continuation is a cut-expression, then the Cut-Elaboration rule is applied.^{12} The successor state is modeled in the extended-syntax configurations, namely by a configuration of the form !(C_{1}, E, C_{2}) composed of a configuration C_{1} (the guard-configuration), an expression E (the guardcontinuation) and another configuration C_{2} (the alternative configuration) by the “!” symbol.

The definition of contexts yields that in order to model the next successor state, one reduces the guard-configuration; i.e., the reduction of a cut-configuration takes place in the guard-configuration. The guardconfiguration can itself reduce into a cut-configuration, and so forth.

In the case where the guard-configuration in a cut-configuration has failed, i.e., the execution state is modeled by a cut-configuration of the form !(⊥, E, C), we apply the Cut-Failure rule to derive the successor state. It is modeled by the alternative configuration C. In the case where the guard-configuration has succeeded, i.e., the execution state is modeled by a cut-configuration of the form !((φ:⊤; C_{1}), E, C_{2}), we apply the Cut-Success rule to derive the successor state. It is modeled by φ: E, i.e., the first disjunct of the guard-configuration with the guard-continuation. The second disjunct C_{1} of the guard-configuration and the alternative configuration C_{2} are put away with. This is how we model “pruning parts of the search tree.”

12To obtain an intuition of the Cut-Elaboration rule, φ : !(E_{0}, E_{1}, E_{2}) & E ⟶ !((φ : E_{0}), (E_{1} & E), (φ : E_{2} & E)), reformulate the Or-Elaboration rule to φ :

(E_{0} & E_{1} ; E_{2}) & E ⟶ (φ:E_{0} & E_{1} & E) ; (φ:E_{2} & E).

Expressions  E ::= φ | px̄ | E_{1} & E_{2} | E_{1} ; E_{2} | !(E, E_{1}, E_{2})
Configurations C ::= φ:E | ⊥ | C_{1} ; C_{2} | !(C_{1}, E, C_{2})
Contexts  C ::= • | C; C | !(C, E, C)

REDUCTION RULES

Cut Elaboration φ:!(E_{0}, E_{1}, E_{2}) & E ⟶ !((φ:E_{0}), (E_{1} & E), (φ:E_{2} & E))
Cut Failure  !(⊥, E, C) ⟶ C
Cut Success  !((φ:⊤; C_{1}), E, C_{2}) ⟶ φ:E

Figure 2: The Cut (“ !”)

5 Coroutining (“ ?”)

Given the syntax of expressions as in Section 3 (cf., in Figure 1), we will extend it with conditional expressions. For now (cf., Figure 3), these are expressions of the form ?(φ, E_{1}, E_{2}) composed of a constraint φ (the guard) and expressions E_{1} (the then-expression) and E_{2} (the else-expression) by the ternary symbol “ ?” (read: “cond”). The logical meaning is “if φ then E_{1} else E_{2}” which is “φ ∧ E_{1} ∨ ¬φ ∧ E_{2}.” Conditional expressions can be used to express negated constraints: ¬φ is logically equivalent to ?(φ, ⊥, ⊤).

As an example, we give a new definition of the length predicate (cf. the guarded Horn clause length(x, n) :– x = nil [] n = zero), again omitting existential quantification:

length(x, n) ↔ ?(x = nil, \begin{matrix}n = zero, \\ x = cons(y, z) ∧ n = succ(m)) & length(z, m) \end{matrix}

The operational semantics of conditional expressions can be described as follows: For each encountered (i.e., elaborated) cond-expression ?(φ, E_{1}, E_{2}), test whether the constraint store entails or disentails φ. If yes, execute E_{1} or E_{2}, respectively (“fire” or “trigger the coroutine”). Otherwise, suspend and repeat the test (“resume”) after a modification of the constraint store (i.e., after a constraint elaboration).

The operational semantics outlined above implements the “freeze” operator of Prolog-II. For example, freeze(X,p(X)) corresponds to ?(x = a, p(x), p(x)) where a can be any constant.

We will now formalize this operational semantics, so that it: (1) is sound with respect to the logical semantics, (2) reflects the suspension/resumption mechanism, (3) accounts for multiple suspensions, (4) models the trigger condition declaratively, and (5) accounts for the incrementality and locality (to each guard) of the possibly often repeated entailment and disentailment tests.

We introduce a new syntact entity, the pool, which becomes another constituent of configurations, besides the constraint store and the contin-

Expressions  E ::= φ | px̄ | E_{1} & E_{2} | E_{1} ; E_{2} | ?(φ, E_{1}, E_{2})
Pools  P ::= ?(φ, E_{1}, E_{2}) | ⊤ | P_{1} ∧ P_{2}
Configurations  C ::= P:φ:E | ⊥ | C_{1} ; C_{2}

REDUCTION RULES

Cond Elaboration  P:φ: ?(φ_{0}, E_{1}, E_{2}) & E ⟶ P ∧?(φ_{0}, E_{1}, E_{2}):φ:E
Cond Success  P ∧?(⊤, E_{1}, E_{2}):φ:E ⟶ P:φ:E_{1} & E
Cond Failure  P ∧?(⊥, E_{1}, E_{2}):φ:E ⟶ P:φ:E_{2} & E
Control  Cond Success and Cond Failure have priority.

CONGRUENCE LAWS

Parallel And  ({P ools}, ∧, ⊤) is a commutative monoid.
Relative Simp.lification ?(φ_{1}, E_{1}, E_{2}):φ:E ≡ ?(φ_{2}, E_{1}, E_{2}):φ:E
if Δ ⊧ φ_{1} ∧ φ ↔ φ_{2} ∧ φ.

Figure 3: Coroutining (“ ?”)

uation. The pool of a configuration modeling some state describes which cond-expressions have been encountered (i.e., elaborated) but not yet fired so far. Thanks to the Paralled-And congruence laws, these cond-expressions form an unordered list, i.e., a multiset. This is important because this models the fact that the tests resume on all suspensions at the same time, and there is no a priori order on the coroutines that can be fired.

The initial state of an execution is now modeled by a configuration with an empty pool, i.e., equal to ⊤ (and with an empty constraint store, as before).

In a first version, the three reduction rules for cond-expressions are the following.

Cond Elab. P:φ: ?(φ_{1}, E_{1}, E_{2}) & E ⟶ P ∧?(φ_{1}, E_{1}, E_{2}):φ:E
Cond Success P ∧?(φ_{1}, E_{1}, E_{2}):φ:E ⟶ P:φ:E_{1} & E if Δ ⊧ φ → φ_{1}
Cond Failure P ∧?(φ_{1}, E_{1}, E_{2}):φ:E ⟶ P:φ:E_{2} & E if Δ ⊧ φ → ¬φ_{1}

In order to reflect that the resumption of the tests happens after each modification of the constraint store and the coroutine is triggered as soon as possible, we add an applicability condition to all reduction rules other than Cond Success or Failure. This condition says that neither the Success nor the Cond Failure rule are applicable. The condition can, of course, also be formulated locally to each rule. Namely, as: The configuration to be reduced is not congruent to a configuration of the form P ∧?(φ_{1}, , ):φ: where Δ ⊧ φ → φ_{1} or Δ ⊧ φ → ¬φ_{1}.

The semantics given so far satisfies the first four points raised above, but not point (5). The questions open are: Can the trigger condition (i.e., entailment or disentailment) be tested locally, i.e., by looking only at the particular cond-expression? Can this test be done incrementally?

From now on, we will assume that the constraint system can implement Relative Simplification [2], which simplifies a constraint φ_{1} relative to a constraint φ to a constraint φ_{2} such that (1) the conjunction of φ with φ_{1} is equivalent to the conjunction with φ_{2}, (2) if φ entails ∃x̄φ_{1}, then ∃x̄φ_{2} is equivalent to true,^{13} and (3) if φ disentails φ_{1}, then φ_{2} is the false constraint; i.e.,

Δ ⊧ φ ∧ φ_{1} ↔ φ ∧ φ_{2} ;
Δ ⊧ φ → ∃x̄φ_{1} iff Δ ⊧ ∃x̄φ_{2} ↔ ⊤ ;
Δ ⊧ φ → ¬∃x̄φ_{1} iff φ_{2} = ⊥ .

Relative Simplification yields incremental and local, sound and complete tests of entailment and disentailment.

We now add Relative Simplification congruence law and replace the Cond Success and Failure rules by the new versions given in Figure 3. This completes modeling the execution of coroutines.

To come back to the point raised in Section 3 on the difference between φ_{1} ∧ φ_{2} and φ_{1} & φ_{2}, we can now construct an example and use the formal semantics to show that in the one case a suspended cond-expression is fired (possibly leading to an infinite loop) and in the other it is not. Take the definition p(x) ↔?(x = f(y, a), p(x), ⊥) and the initial states ⊤ : ⊤ : p(x) & (x = f(y, z) ∧ z = b) and ⊤ : ⊤ : p(x) & x = f(y, z) & z = b

(corresponding to the queries p(X), X=f(Y,b) and p(X), X=f(Y,Z), Z=b,

respectively).

To indicate a source of non-confluence, one can construct an example where the order chosen for the firing of two competing suspended condexpressions yields two different behaviors (e.g., one leading to an infinite loop and the other not). This is due to the fact that, in our semantics, both condexpressions are moved from the (“concurrent”) pool to the (“sequential”) continuation where they are ordered by their composition with “ & ”.^{14} Take the definitions p(x) ↔?(x = a, p(x), ⊥) and q(x) ↔?(x = a, ⊥, ⊥) and the initial state ⊤: ⊤: p(x) & q(x) & x = a. Execution may lead to either of the states ⊤:(x = a):⊥ & p(x) or ⊤:(x = a):p(x) & ⊥.

We will discuss the interaction of cut and coroutining in Section 7.

6 Existential quantification (“∃”)

The logically correct version of the definition of the length predicate in Section 3 (when ↔ means “if and only if”) has to quantify the variable y in a constraint and the variables z and m in an expression:

13As a special case: If φ entails φ_{1}, then φ_{2} is equivalent to true.

14One may, of course, design a semantics with a different, more fair execution strategy for coroutines.

length(x, n) ↔ (\begin{matrix}(x = nil ∧ n = zero) ; \\ (∃z∃m \underbrace{(∃y(x = cons(y, z)) ∧ n = succ(m) & length(z, m))}_{expression being quantified})) \end{matrix}

The previous version of the Unfolding rule tacitly assumes that the program always contains an appropriate version of the definition of the predicate being unfolded. We did not model that such a version is obtained, for each unfolding, by consistent renaming of all variables occurring in the definition. Also, in the semantics present so far, the new variables introduced by the unfolding are visible everywhere and never disappear again. This is not a complete modeling of the actual operational semantics.

From now on, having extended the syntax of expressions with “∃” (cf., Figure 4), we may assume that the expression defining a predicate px̄ does not have any free variables other than the ones in the tuple x̄. Hence, the new form of the Unfolding rule does not add any free variables to the configuration to which it is applied. Its applicability condition x̄ ∩ ȳ = ∅ (to avoid capturing between the actual parameters x̄ and the formal ones ȳ) can be satisfied (with the Quantifier Renaming congruence law) if x̄ is in the scope of an existential quantifier; hence, it is sufficient to require that the free variables in the query (initial configuration) do not occur in the program.

A quantified expression cannot be elaborated directly. The scope of the quantified variables has to be extended first (by application of the Quantifier Elaboration law). This is possible only if they can not be captured, i.e., come into the scope of a different quantifier. In order to extend the scope of variables that have the same name as others, they have to be renamed first (by application of the Quantifier Renaming law). After the scope of the quantified variables has been extended (“the quantifier is pulled out”), i.e., the whole configuration instead of just the expression is quantified, the configuration can be reduced thanks to the definition of contexts.

Finally, the scope of a variable in an expression can be reduced to any sub-expression that contains all its occurrences (“the quantifier is pulled in”). This could be modeled by congruence laws of the form ∃x(T_{1} ∘ T_{2}) ≡ (∃x T_{1}) ∘ T_{2} where x ∉ V(T_{2}), for any trees T_{1} and T_{2} of any syntactic entity and any composition symbol ∘. In fact, the Quantifier Mobility law in the version given here suffices for our semantics, together with the Quantifier Exchange law. The Simplification law then takes care of removing quantifiers of redundant (“auxiliary”) variables (such as in ∃x x = nil ∧ φ where x ∉ V(φ)) and of removing variables which do no longer appear in a configuration, since ∃xφ ≡ φ if x ∉ V(φ).

This is how we account for the introduction of variables as well as for their scope (i.e., their visibility and life-time), namely through congruence laws which reflect laws for logical quantification.

Expressions  E ::= φ | px̄ | E_{1} & E_{2} | E_{1} ; E_{2} | ∃xE
Configurations  C ::= φ:E | ⊥ | C_{1} ; C_{2} | ∃x C
Contexts  C ::= • | C; C | ∃x C

CONGRUENCE LAWS

Quantifier Exchange ∃x∃yE ≡ ∃y∃xE, ∃x∃yC ≡ ∃y∃xC
Quantifier Renaming C_{1} ≡ C_{2} if C_{1} and C_{2} equal up to α-renaming
Quantifier Mobility ∃x(φ:E; C) ≡ (∃xφ):E; ∃xC if x ∉ V(E)

Figure 4: Existential quantification (“∃”)

7 The complete semantics

The addition of the features discussed in the previous three sections to the base case discussed in Section 3 yields the semantics defined in Figure 5. Two of these feature combinations need to be discussed. We leave the discussion of the combination of “∃” and “ ?” to the full version of this paper.

Cut and Coroutining The complete semantics accounts in particular for the interaction between cut- and cond-expressions. Here, we must remove some ambiguities that are often left open in language specifications or manuals. There are two interesting cases, namely (1) where a suspension lies in the scope of a cut, and (2) where a suspension calls a cut upon triggering.

Our formalization of the semantics defines (i.e., specifies through the form of the Cut Success and Failure rules) that a cut ignores suspensions for its decision. More precisely, if a cut is reached at a moment of execution where a coroutine is suspending, then a potential failure of this co-routine is not anticipated but the cut is executed as if the co-routine did not exist. (It is crucial, of course, that this coroutine can indeed not be fired; this is assured by the additional applicability condition on all rules other than Cond Success and Failure expressing that these two rules have priority.)

In the second case it seems better to leave the specification open and admit non-confluence of terminating executions.^{15} We recall that we postulate that “∧” is a commutative composition symbol over cond-expressions in the Paralled-And congruence law, and thus do not fix the order of reactivations of competing suspensions. In the case where a reactivation leads to the call of an order-dependent control-operator such as the cut, its decision and the subsequent program execution are no longer determined before-hand. One can easily construct an example where two coroutines are fired one after the other and where one of the two calls a cut whose decision is influenced by the other. Take the definitions p(x, y) ↔?(x = a, y = b, ⊥) and q(X, Y) ↔?(x = a, !(r(Y), ⊤, ⊥), ⊥) and r(y) ↔ (y = a; y = b) and the initial state ⊤: ⊤: p(x, y) & q(x, y) & x = a. Its execution leads to either of the two states ⊤: x = a, y = b: !(r(y), ⊤, ⊥) or ⊤: x = a: !(r(y), ⊤ & y = b, ⊥) and from there to ⊤ : x = a, y = b : ⊤ or to ⊥, respectively. We model this indeterminism by the fact that our abstract-tree-rewriting system is non-confluent when such a case is admitted.

15At the end of Section 5 we mentioned non-confluence even in absence of the cut.

8 Conclusion and Future Work

We have presented a formal definition of the operational semantics of constraint logic programs with coroutining. What is it good for? We will list a few benefits.

(1) By modeling program execution through reduction rules and through congruence laws, we have been able to state what the (primarily) operational and what the declarative aspects of the languages are. For instance, we have accounted for the fact that the sequences of goals are ordered, but the representations of constraints as conjunctions are not.

(2) We have abstracted away from details that are relevant only for language implementations, and not for the program execution. Clearly, backtracking is merely a matter of space-efficient implementation.

(3) We have modeled the control operators of the program (such as the order statement for goals and clauses and the cut). This enables the programmer to predict the control flow of his program and to evaluate its performance (assuming a complexity bound for the constraint solver, e.g., a quasi-linear one in the case of Prolog-II).

(4) We have been able to make precise the critical interaction between sequential execution (of expressions in the continuation) and concurrent execution (of suspended conditionals in the pool), in particular in the two cases where a suspension lies in the scope of a cut or a suspension calls a cut upon triggering.

As for future work: Not all of the mathematical formulae which model execution states have a first-order logic reading, nor do all of the rewriting steps which model state transitions. It is now possible, however, to investigate which of them do. This can be useful in order to determine which of the programs do have a declarative reading (in first-order logic).

Along the lines of this paper, one can now start modeling other language functionalities which are considered impure such as assert/retract, request of further solutions, backtrackable assignment, cells, and so on.

One interesting branch of future work would consist of investigating confluence proofs for the reduction relation with coroutining (without coroutining, all reduction steps are deterministic), possibly building on work in [12]. As the examples given above show, only “‘weak” confluence may possibly hold (i.e., confluence of terminating executions), and even this only under a restriction on the use of cut.

Acknowledgements We thank Harald Ganzinger, Michael Hanus, Sverker Janson, Olivier Ridoux and Peter Van Roy for discussions and com-

SYNTAX

Expressions  E ::= φ| px̄| E_{1}&E_{2} |E_{1} ; E_{2} |!(E, E_{1}, E_{2})|?(x̄, φ, E_{1}, E_{2})| ∃xE
Pools  P ::= ?(x̄, φ, E_{1}, E_{2}) | ⊤ | P_{1} ∧ P_{2}
Configurations  C ::= P:φ:E | ⊥ | C_{1} ; C_{2} | ∃xC |!(C_{1}, E, C_{2})
Contexts  C ::= • | C; C |!(C, E, C) | ∃x C

REDUCTION RULES

Application Elab. P:φ:px̄ & E ⟶ P:φ:∃ȳ(x̄ = ȳ & E_{1}) & E

if pȳ ↔ E_{1} in program, x̄ ∩ ȳ = ∅

Constraint Elab. P:φ:φ_{1} & E \begin{matrix}⟶ & P:φ ∧ φ_{1} :E & if Δ |̸= φ ∧ φ_{1} ↔ ⊥, φ_{1} ≠ ⊤ \\ ⟶ & ⊥ & if Δ ⊧ φ ∧ φ_{1} ↔ ⊥ \end{matrix}
Or Elaboration  P:φ:(E_{1} ; E_{2}) & E ⟶ (P:φ:E_{1} & E) ; (P:φ:E_{2} & E)
Cut Elaboration P:φ:!(E_{0}, E_{1}, E_{2}) & E ⟶ !(P:φ:E_{0}, E_{1} & E, P:φ:E_{2} & E)
Cut Failure  !(⊥, E, C) ⟶ C
Cut Success  !((P:φ:⊤; C_{1}), E, C_{2}) ⟶ P:φ:E
Cond Elab.  P:φ: ?(x̄, φ_{0}, E_{1}, E_{2}) & E ⟶ P ∧?(x̄, φ_{0}, E_{1}, E_{2}):φ:E
Cond Success  P ∧?(x̄, φ_{1}, E_{1}, E_{2}):φ:E ⟶ P:φ:∃x̄(φ_{1} & E_{1}) & E
if Δ ⊧ ∃x̄φ_{1}
Cond Failure  P ∧?(x̄, ⊥, E_{1}, E_{2}):φ:E ⟶ P:φ:E_{2} & E
Control  Cond Success and Cond Failure have priority.

CONGRUENCE LAWS

Sequential And  ({Expressions}, & , ⊤) is a monoid.
Sequential Or  ({Configurations}, ; , ⊥) is a monoid.
Parallel And  ({P ools}, ∧, ⊤) is a commutative monoid.
Simplification  φ_{1} ≡ φ_{2} if Δ ⊧ φ_{1} ↔ φ_{2}.
Relative Simp.  ?(x̄, φ_{1}, E_{1}, E_{2}):φ:E ≡ ?(x̄, φ_{2}, E_{1}, E_{2}):φ:E
if Δ ⊧ φ_{1} ∧ φ ↔ φ_{2} ∧ φ.
Quantifier Elab. P:φ:∃xE_{1} & E_{2} ≡ ∃x(P:φ:E_{1} & E_{2}) if x ∉ V(P:φ:E_{2})
Q. Exchange  ∃x∃yE ≡ ∃y∃xE, ∃x∃yC ≡ ∃y∃xC
Q. Renaming  C_{1} ≡ C_{2} if C_{1} and C_{2} equal up to α-renaming.
Q. Mobility  ∃x(P:φ:E; C) ≡ P:∃xφ:E; ∃xC if x ∉ V(P) ∪ V(E)

Figure 5: The Complete Semantics ments.

15

References

[1] H. Aït-Kaci, B. Dumant, R. Meyer, A. Podelski and P. Van Roy. Wild LIFE: A User Manual. Digital Equipment Corporation, Paris Research Laboratory. Rueil-Malmaison, France, April 1993.

[2] Hassan Aït-Kaci, Andreas Podelski, and Gert Smolka. A feature-based constraint system for logic programming with entailment. Theoretical Computer Science, 122(1–2):263–283, January 1994. (Also appeared in Fifth Generation Computing Systems, Tokyo, 1992.)

[3] E. Börger and P. Schmitt. A formal operational semantics for languages of type Prolog III. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, CSL’90, 4th Workshop on Computer Science Logic, LNCS 533, pages 67–79, 1991.

[4] M. Carlsson, J. Widèn, J. Andersson, S. Andersson, K. Boortz, H. Nilsson, and T. Sjöland. SICStus Prolog User’s Manual. SICS, Box 1263, 164 28 Kista, Sweden, 1991.

[5] A. Colmerauer, H. Kanoui, and M. V. Caneghem. Prolog, theoretical principles and current trends. Technology and Science of Informatics, 2:4, pages 255–292, 1983.

[6] J. Jaffar, M. J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming 19 & 20, 503–581, 1994.

[7] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984.

[8] M. J. Maher. Logic semantics for a class of committed-choice programs. In Fourth ICLP, pages 858–876. MIT Press, 1987.

[9] R. Milner. Functions as Processes. In Journal of Mathematical Structures in Computer Science 2:2, pages 119–141, 1992.

[10] L. Naish. MU-Prolog 3.1db Reference Manual. Computer Science Department, University of Melbourne, Melbourne, Australia, May 1984.

[11] L. Naish. Automating Control for Logic Programs. In JLP 2:3, 1985, pages 167–184, 1985.

[12] J. Niehren and G. Smolka. A Confluent Calculus for Higher-order Relational Programming. In J-P. Jounnaud, editor, 1st International Conference on Constraints in Computational Logics, LNCS 845, pages 89–104, 1994.

[13] R. A. O’Keefe. On the treatment of cuts in Prolog source-level tools. In Symposium on Logic Programming, pages 68–72, The Computer Society Press, 1985.

[14] G. Smolka. Residuation and guarded rules for constraint logic programming. In F. Benhamou and A. Colmerauer, editors, Constraint Logic Programming: Selected Research, pages 405–419, MIT Press, 1993.

[15] G. Smolka. A calculus for higher-order concurrent constraint programming with deep guards. Research report, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhlsatzenhausweg 3, D-W-6600 Saarbrücken, Germany, 1993.

[16] G. Smolka. A foundation for higher-order concurrent constraint programming, In J-P. Jounnaud, editor, 1st International Conference on Constraints in Computational Logics, LNCS 845, pages 50–72, 1994.