ATMS-based constraint programming

Vijay A. Saraswat

Johan de Kleer

Brian C. Williams

Xerox PARC, 3333 Coyote Hill Road Palo Alto, Ca 94304

October 24, 1991

Abstract

We are developing a broad and comprehensive theory of constraint programming, subsuming the paradigms of functional and logic programming [Sar89, SR90, SRP91, JSS91, SRH91]. The theory is based on a view of computation organized around the notions of constraint systems as systems of partial information, of store-as-constraint and process-as-information-transducer, and emphasizes the use of constraints for communication and control between concurrently executing processes.

Such languages offer a very simple and abstract level for specifying computations for combinatorial exploration. In prior work [JSS91, SRH91] we have shown how to smoothly integrate Prolog-style backtracking and various local consistency techniques within this framework. In this paper we develop the integration of this framework with the alternate approach to combinatorial exploration predominant in AI, truthmaintenance systems (TMSs) [Doy79, McA90, deK86a]. In particular, we give a generic mechanism for enriching any constraint system B with the notion of assumptions to obtain another constraint system A(B). To implement A(B), ATMS-implementation techniques are integrated with the constraint-solver for B. All the usual cc combinators — such as ask, tell, conjunction (parallel composition) and hiding, all closed under recursion — are immediately available on top of A(B), providing a simple and powerful constraint language. In addition, several new combinators can now be defined which take advantage of the extra structure of assumptions built into the constraint system. As before, each of these new combinators can be given a very simple mathematical characterization as closure operators over the underlying constraint system. They enable a simple and elegant expression of various previously developed programming notions on top of ATMSs, such as (various kinds of) consumers [deK86b].

1 Introduction

We take it as being self-evident that a large class of computations in AI (and knowledge representation, and natural language understanding) centrally involves the representation and manipulation of constraints. Our task is to develop the conceptual, mathematical and practical foundations of a general theory of computation based on constraints.

The concurrent constraint (cc) programming approach [Sar89, SR90, SRP91] is based on treating a constraint system as just a system of partial information a la [Sco82]: essentially, a set of objects (with unanalyzed internal structure) equipped with an entailment relation. Arising from earlier work in constraint logic programming [JL87] and concurrent logic programming [Mah87, Sar87], the basic move in this paradigm is to replace the notion of store-as-valuation central to von Neumann computing with the notion that the store is a constraint, that is, a set of pieces of partial information about the values that variables can take. The usual notions of “read” and “write” no longer make sense; instead computation progresses via the execution of ask and tell actions. An ask operations takes a constraint (say, c) and uses it to probe the structure of the store: it succeeds if the store contains enough information to entail c. Tell takes a constraint and conjoins it with the constraints already in the store. (Thus computation progresses via the monotonic accumulation of information.) Concurrency arises because any number of agents may simultaneously interact with the store. Synchronization is achieved via a blocking ask — an agent blocks on a constraint c if the store is not strong enough to entail c; it remains blocked until such time as (if ever) some other concurrently executing agents add enough information to the store for it to be strong enough to entail the query.

The very wide applicability of the underlying notion of a constraint system means that the notion of constraint programming based on it is very general (see [Sar89]) — indeed it encompasses logic programming, concurrent logic programming, data-flow and (at least first-order) functional programming. Hand-in-hand with this generality goes mathematical simplicity — (determinate) programs in this framework were shown to correspond to closure operators over the underlying constraint system E, and non-determinate programs were shown to correspond to closure operators over the Smyth power-domain of E [SRP91, JSS91]. Closure operators — operators over a partial order that are monotone, idempotent and extensive — have a very beautiful algebra summarized in Appendix A; in particular they are closed under a very natural notion of parallel composition. [Sar89, SRH91] showed how this paradigm accounts for the pre-nascent notions of constraint programming evident in the work of [dKS80] (constraint propagation techniques) and in [Ste80] (constraint posting), and how these ideas can be extended to accomodate the notion of local consistency techniques for solving networks of constraints.

1.1 Control of search.

The predominant style for combinatorial computation, embodied within Prolog, is to cast the computation as a search in an And-Or tree. Various techniques for searching such trees efficiently (perhaps in parallel) have been devised. For example, the Andorra principle, an embodiment of the least commitment principle, governs the selection of nodes to expand next at an And-phase: “determinate” nodes — those that have at most one Or-branch below them which is not known to be inconsistent — are expanded first.

A major drawback of such approaches is that there is no possibility for communication between different Or-parallel branches. For several applications, such as diagnosis, it is necessary for the problem-solver to be able to move back and forth between different Or-parallel worlds with facility. (For example, each consistent Or-parallel world corresponds to a diagnosis). Also, the techniques for controlling search available when exploring And-Or trees top-down tend to be based on controlling the forward phase of the search: the phase that determines what nodes to expand next. (Indeed, the integration of these techniques with the cc framework has been a topic of recent research and is now reasonably well-understood [Hen89, SRH91].) In general, such techniques offer a significant computational advantage over chronological backtracking (by detecting inconsistency earlier). However, they are of less use in many AI applications in which not all decisions depend on each other. For such applications, the methods and techniques of truth maintenance systems have been developed over the last decade [Doy79, deK86a, McA90].

Truth Maintenance Systems offer an attractive and conceptually very different computation model from the And-Or trees underlying Prolog-like languages. Within the standard view of constraint programming, non-determinism is reflected by splitting: at a branch-point, conceptually, copies of the state of the world (the store, other conjunctive agents) are made, and these copies are kept strictly insulated from each other. In the TMS viewpoint, no splitting is done, even conceptually: instead an assumption is associated with each branch, and all the information on that branch is made conditional on that assumption. To give a simple example, Prolog-like languages treat a formula ϕ ∧ (ψ_{1} ∨ ψ_{2}) as the (equivalent) formula (ϕ ∧ ψ_{1}) ∨ (ϕ ∧ ψ_{2}); TMSs treat it as the (equivalent) formula ϕ ∧ (A → ψ_{1}) ∧ (¬A → ψ_{2}) (for A some new Boolean variable). In addition, in assumption-based TMSs [deK86a, deK86b, deK86c], each formula is associated with a label which records the set of conditions (conjunctions of assumptions) under which the formula has been asserted.

The fundamental idea in this paper is to extend the structure of tokens underlying the constraint programming language by building in the notion of assumptions and a restricted form of implication. Assume given a constraint system with vocabulary D. In the new constraint system, tokens of the form ({A_{0}, …, A_{n−1}}, c) are allowed, where the A_{i} are propositional variables, and c is a token in D or (a conjunction of) other propositional variables. Intuitively, such a token expresses the idea that the piece of information c is known to hold — but only if the assumptions A_{0}, …, A_{n−1} are in force.

We should emphasize that our approach yields not just a programming language on top of an ATMS, but an infinite family of languages, depending upon the particular constraint system employed. Most ATMS-based languages in the past can be thought of as having a very simple built-in constraint system — we shall present such a constraint system in detail later in this paper.

2 Assumptive constraint systems

In this section we briefly review the notion of a simple constraint system, and discuss how to generate from an arbitrary constraint system B (the “base” constraint system), and assumptive constraint system A(B), given some underlying set of “nodes” (Definition 2.3). A simple characterization theorem for such constraint systems is also given.

In the following, for any set D, we shall let P (D) (p(D)) stand for the set of all (finite) subsets of D. Also, we use the symbol ⊆_{f} for the “is a finite subset of” relationship between two sets.

Definition 2.1 A simple constraint system A is a structure ⟨D_{A}, ⊢_{A}⟩ where ⊢_{A} is an entailment relation on D_{A}, that is, a relation ⊢_{A} ⊆ p(D_{A})×D_{A} satisfying:

A1 u ⊢_{A} c for every c ∈ u.

A2 if u ⊢_{A} c for every c ∈ v, and v ⊢_{A} d, then u ⊢_{A} d.

Together these properties imply monotonicity: if u ⊢_{A} d and v ⊇ u then v ⊢_{A} d.

In the following, we shall overload the entailment symbol, letting u ⊢ u′ (for u, u′ finite sets of tokens) stand for the conjunction of assertions u ⊢ d′ for all d′ ∈ u′. Finally, we take ≈ to be the equivalence relation on p(D) induced by the pre-order ⊢.

Example 2.1 For any set of tokens D, the generic constraint system over D, G(D) is given by ⟨D, {(u, d) | d ∈ u}⟩, It is easy to check that (A1) and (A2) are satisfied and that u ⊢_{G(D)} v iff u ⊇ v.

Let ⊥ ∈ D be a special pre-designated token. Then the generic constraint system over D with falsehood ⊥, G_{⊥}(D) is ⟨D, {(u, d) | ⊥ ∈ u or d ∈ u}⟩. Again, it is easy to check that (A1) and (A2) are satisfied.

As another example, note that ⟨∅, ∅⟩ specifies a constraint system with no tokens — called the vacuous constraint system.

In the above example, a set of tokens in G(D) is nothing more than the “sum of its parts”, that is a “free” conjunction. G(D) is essentially the “strongest” constraint system on top of a token-set D — any other constraint system on D must have an entailment relation that is weaker (i.e., is larger as a set) than ⊢_{G} (D). Alternatively, ⊢_{G} (D) is the intersection of all possible entailment relations on D. G_{⊥}(D) is just like G(D) except that it has the notion of falsehood built into it: ⊥ satisfies the property that for every token d ∈ D, {⊥} ⊢_{G_{⊥}(D)} d. Shortly we shall see that for a set N of “nodes” G_{⊥}(N) can be thought of as the constraint system underlying TMSs.

We now show how to generate an assumptive constraint systems A(B) from a given base constraint system B. We first fix a (possibly infinite) set N of propositional variables (called nodes). For simplicity, we shall assume that N is chosen to be disjoint from D_{B}. We identify a (possibly infinite) subset A ⊂ N of assumptions. We require that there be a special symbol, conventionally written ⊥ to signify falsehood, in N but not in A. Now we shall obtain the assumptive constraint system A(B) = ⟨D_{A(B)}, ⊢_{A(B)}⟩ by combining B with G_{⊥}(N) in a particular way.

Defining D_{A(B)}. Let D = D_{B} ∪ D_{G_{⊥}(N)}^{1}. A d ∈ D is called a datum; a datum is a node (if it comes from D_{G_{⊥}(N)}, i.e., N) xor a base constraint (if it comes from D_{B}).^{2}

Now we can define D_{A(B)}: it is just the set of pairs (e, d), where e is a finite subset of N, and d ∈ D. Intuitively, a token (e, d) asserts that d must hold whenever each of the nodes in e hold. In such a pair, we shall call e the antecedent and d the consequent. Conventionally, tokens whose consequents are nodes (rather than base constraints) are called justifications. Each justification ({n_{1}, …, n_{k}}, n) can be thought of as the propositional Horn clause n_{1} ∧ … ∧ n_{k} → n. Also, a token of the form (e, ⊥) is called a nogood (since it represents the assertion that not all of a set of nodes can hold simultaneously).

Note that we do not allow basic constraints d ∈ D_{B} to occur in antecedents of tokens, since the ATMS is just a propositional engine. This effect can be obtained by means of a user program as shown in Section 3.

In the following, whenever a datum d occurs in a context where an element of D_{A(B)} is expected, we should think of d as shorthand for (∅, d). Similarly, for u ⊆ D, whenever (e, u) appears in a context where a subset of D is expected, we should take it to be the set {(e, d) | d ∈ u}, and for z ⊆ D_{A(B)} whenever (e, z) appears in a context where a subset of D_{A(B)} is expected, we should take it to be the set {(e ∪ e′, d′) | (e′, d′) ∈ z}. Finally, for any set Q ⊆ D_{A(B)}, we let J(Q) denote its subset of justifications. (Thus, the set of justifications is just J(D_{A(B)}).)

1Note, of course, that D_{G_{⊥}(N)} = N; we chose the more cumersome expression to emphasize the symmetric nature of the construction.

2Just a word of warning: those familiar with the TMS literature will find this terminology slightly non-standard.

Defining ⊢_{A(B)}. We define ⊢_{A(B)} in three steps. First we define an entailment relation on justifications, then we define an entailment relation on the data-set D, and finally we use these two relations to define ⊢_{A(B)}.

The relation ⊢_{J} on the set of justifications is defined by: u ⊢_{J} r iff the conjunction of each token in u (viewed as a propositional formula) propositionally entails r (viewed as a propositional formula). Note that for a conjunction of nodes e and node n, e ⊢_{G_{⊥}(N)} n iff e ⊢_{J} n.^{3}

The relation ⊢_{D} is obtained by extending ⊢_{B} and ⊢_{G_{⊥}(N)} to D = D_{B} ∪ D_{G_{⊥}(N)}) in the obvious way: roughly, u ⊢_{D} d if u entails d in the base constraint system B or u entails d in the “TMS constraint system” G_{⊥}(N). The only interesting aspect of the definition is that inconsistency must be handled correctly.

Definition 2.2 Define ⊢_{D}⊆ p(D) × D by: u ⊢_{D} d iff one of the following conditions holds:

• u is inconsistent; that is, u ∩ D_{G_{⊥}(N)} ⊢_{G_{⊥}(N)} ⊥ or u ∩ D_{B} ⊢ d′ for all d′ ∈ D_{B},

• u entails d considering only the tokens in u of the same type as d; that is, d ∈ D_{B} and u ∩ D_{B} ⊢_{B} d, or d ∈ D_{G_{⊥}(N)} and u ∩ D_{G_{⊥}(N)} ⊢_{G_{⊥}(N)} d).

It is easy to check that this relation satisfies (A1) and (A2).

Given a conjunction of nodes e and a finite set of tokens u, the e-context of u, denoted u_{e}, is just the set

{d | (e′, d) ∈ u, J(u) ∪ e ⊢_{J} e′}

of all data that “hold” in e. We are now ready to give the main definition:

Definition 2.3 (Assumptive constraint systems) For a constraint system B, and an underlying set of nodes N and assumptions A, the assumptive constraint system A(B) is the structure ⟨D_{A(B)}, ⊢_{A(B)}⟩ where ⊢_{A(B)} is given by:

u ⊢_{A(B)} (e, d) iff u_{e} ⊢_{D} d

As usual, the elements of the constraint system, denoted |A(B)| are the ⊢_{A(B)}-closed subsets of D_{A(B)}. For every set u ⊆ D_{A(B)} we denote by \overline{u} the smallest ⊢_{A(B)}-closed set containing u. We define a conjunction of nodes e to be inconsistent in u iff u ⊢_{A(B)} (e, ⊥).

Example 2.2 The simplest example of an assumptive constraint system is obtained by taking B to be the vacuous constraint system. In such a case, the tokens of A(B) are just of the form (e, n), and ⊢_{A(B)} is propositional entailment. Such an assumptive constraint system can be implemented directly with an ATMS.

3Note that by our notational conventions, e ⊢_{J} n should be read as: {(∅, x) | x ∈ e} ⊢_{J} (∅, n).

The central property of the implication inherent in tokens (e, z) is that it can be regarded as adjoint to conjunction in the following precise sense familiar from logic:

Theorem 2.1 For any set u, z ⊆ D_{A(B)}, and e ⊆_{f} A:

u ⊢_{A(B)} (e, z) iff u ∪ e ⊢_{A(B)} z

Several observations can readily be made. Since u∪e ⊢_{A(B)} u, it follows that u ⊢_{A(B)} (e, u). Also, we get e ∪ (e, z) ⊢_{A(B)} z, and e ∪ (e, z) ⊢_{A(B)} e ∪ z, since (e, z) ⊢_{A(B)} (e, z). From the last statement, employing the adjunction again we get (e, z) ≈_{A(B)} (e, e ∪ z).

Note also that e ∪ u_{e} = (e ∪ u)_{∅} — that is, given a store u, a datum is in the context labelled by e iff it is in the context labelled by ∅, provided that the nodes e are asserted as being true.

2.1 Canonical representations of conditional constraints

In ATMS terminology, an environment is a conjunction of assumptions, a label for a node n is the set of environments s such that (s, n) is derivable from the given justifications. An environment s for n is said to be sound if (s, n) is entailed by the store, and consistent if (s, ⊥) is not entailed by the store. A label l = {s_{0}, …, s_{k−1}} for n is said to be sound if each s_{i} is sound for n, consistent if each s_{i} is consistent for n, complete if for any sound environment s for n, there is an i such that s ⊇ s_{i} and minimal if for all i < k, if s_{i} ⊆ s and s is a sound environment for n, then s ⊆ s_{i}. The basic ATMS algorithm maintains sound, consistent, complete and minimal labels for each node. We note below some consequences of our definitions which justisfy the label propagation algorithm in the ATMS.

For any two conjunctions of nodes e, e′, recall that e ⊢_{G_{⊥}(N)} e′ iff e ⊇ e′ or ⊥ ∈ e.

Proposition 2.2 For e, e′ ∈ p(A) and d ∈ (D + A), {(e, d)} ⊢_{A(B)} (e′, d) whenever e′ ⊢_{G_{⊥}(N)} e. Further, e ⊇ e′ implies u_{e} ⊇ u_{e′}.

As a special case, this proposition says that if a datum is in (the context of) a given environment, then it is also in (the context of) every superset environment.

Proposition 2.3 For any e ∈ p(D_{G_{⊥}(N)}) {(e, ⊥)} ⊢_{A(B)} (e, d) for all d ∈ D.

As a special case, this proposition says that every datum holds in an inconsistent environment (an environment in the label of ⊥).

These two propositions are used internally in the ATMS implementation of the generic constraint system over an arbitrary token-set D. We can think of the canonical form maintained internally by the ATMS as being obtained by deleting from (the closure of) any finite set of tokens u:

• tokens (s, d) (for d ≠ ⊥) if (s, ⊥) ∈ u (elimination of nogood environments from labels).

• tokens (s′, d) if (s, d) ∈ u, for s ⊂ s′ (eliminating non-minimal environments).

If these two rules are followed, the label for each token d ∈ D will be consistent, sound, complete and minimal.

3 A simple programming language

The notion of computation on top of an assumptive constraint system is no different from that on top of any constraint system. The store consists of a set of tokens, and computation progresses via a number of (possibly recursively defined) agents running in parallel, checking for the presence of certain tokens in the store (ask), and adding some other tokens to the store (tell). The role of the “problem-solver” in the usual TMS-architecture is played here by the user program, and the role of the ATMS is played by the constraint-solver implementing the entailment relation on which the given constraint system is based. In the case of an assumptive constraint system, this constraint solver can conceptually be thought of as consisting of two parts — a part which deals with managing environments (the TMS) and the part which deals with performing the entailment operations in the underlying constraint system. (In usual TMS/problem-solver architectures, the latter is thought of as part of the problem-solver: thus the “usual” TMS architecture is obtained by taking as built-in the vacuous constraint system.)

In addition to ask, tell and parallel composition operations — which were first defined in the form below in [SRP91] — a number of other combinators can be defined which exploit the extra structure of tokens and provide extra control over execution. In the following we shall follow the strategy of defining the new combinators by giving their mathematical denotations and then describing informally how such combinators can be implemented. This allows a far simpler and more precise description than is possible if one were to rely purely on implementational notions. As before, the denotation of each agent will continue to be a closure operator over the set of elements of the underlying constraint system, in this case |A(B)|. We shall represent each closure operator by the set of its fixed-points.

Tell actions Given any finite set of tokens c, the agent c⋆^{4} adds the tokens in c to the current store. Using lambda-notation, the tell combinator c⋆ is λz.\overline{z ∪ c}. The set of fixed-points of such an operator are exactly those elements of |D_{a}|

4When there is no risk of confusion, we write a c⋆ as c.

Syntax.

P::= D.A  Programs
D::= ϵ | p(X) :: A | D.D Declarations
A::=  Agents
c⋆  Tell
| c → A  Ask
| A ∧ A  Conjunction (parallel composition)
| in e do A  Focussing
| all A  ??
| ∃X.A  Hiding
| p(X)  Procedure Call

Semantic Equations.

A(c)e = {d ∈ |D_{a}| | d ≥ c} A(c → A)e = {d ∈ |D_{a}| | d ⊇ c ⇒ d ∈ A(A)e} A(A ∧ B)e = A(A)e ∩ A(B)e A(∃X.A)e = {c ∈ |D_{a}| | ∃_{X}c = ∃_{X}d for some d ∈ A(A)e} A(in e′ do A)e = \{d ∈ |D_{a}| | \overline{d ∪ e} ∈ A(A)e\} A(all A′)e = ∩_{e∈p(A)}A(in e do A′)(e) A(p(X))e = S_{[X/α]}e(p)) D(ϵ)e = e D(p(X) :: A.D) = D(D)e[p ↦ S_{[α/X]}A(A)e)] P(D.A) = A(A)fix(D(D))

Above, α is some variable in the underlying constraint system which is not allowed to occur in user programs. (It is used as a dummy variable during parameter passing.)

Table 1: Denotational semantics for the ATMS-based cc languages which contain all the tokens in c:

c⋆ = {d ∈ |D_{a}| | c ⊆ d}

Example 3.1 Execution of the tell agent ({A_{1}, A_{2}}, X = 1) causes the token ({A_{1}, A_{2}}, X = 1) to be added to the store. In operational terms, this causes the label for X = 1 to be updated to reflect the fact that the conjunctions of assumptions A_{1} and A_{2} is sufficient to cause X = 1 to hold.

More generally, telling the store the (justification) token ({n_{1}, …, n_{k}}, n) corresponds to the TMS notion of “installing” the justification n_{1} ∧ … ∧ n_{k} → n. In particular, telling the token ({n_{1}, …, n_{k}}, ⊥) is asserting that the set {n_{1}, …, n_{k}} is a nogood.

Ask For any finite set of tokens c and agent A, the “ask” agent c → A (read: “c then A”) is defined as follows: on any input z, examine if z has enough information to entail (each token in) c. If so, then return the result of running A in z; else return z unchanged. Using lambda-notation, the function is: c → A = λz. if c ⊆ z then A(z) else z. It is easy to see that this defines a closure operator (if A is a closure operator). In terms of fixed-points:

c → A = {z ∈ |D_{a}| | c ⊆ z ⇒ z ∈ A}

Example 3.2 The agent (({A_{1}}, X ≥ 3), ({A_{2}}, Y = 4)) → ({B}, Z = 1) suspends until there are enough constraints in the contexts u_{e} (for environments e that entail {A_{1}}) to entail X ≥ 3, (this is what it means for the store u to entail the token (A_{1}, X ≥ 3)), and similarly for ({A_{2}}, Y = 4); and if and when these conditions are satisfied the agent fires and adds the token ({B}, Z = 1) to the store. (Note that the antecedent of the token added does not have to be related to the antecedents of the tokens in the ask-part of the agent.

Relationship with consumers. Given a set of tokens u, the ask action (e, e′) succeeds iff the conjunction of the nodes in e implies each of the nodes in e′, given u. (In ATMS-terminology, a node a is said to imply a node b if every environment in the label for a is a subset of an environment in the label for b.) This notion is the basic building block of the inclusive implication consumers of [deK86c], which can therefore be expressed as particular kinds of such ask-and-tell agents.

Similarly, the contradiction consumers of [FdK88] are also a special case of such ask-and-tell agents. Suppose we want an agent A to be executed whenever it is discovered that a particular environment e is inconsistent. This is expressed by running the agent

(e, ⊥) → A

which asks whether the token (e, ⊥) can be entailed in the current store, and if so, runs A.

More generally, ask and tell combinators provide capabilities that are not available in the usual consumer architecture. Consumers do not explicitly reference node labels, whereas both ask and tell operations work on tokens of the form (e, d), for e an environment and d a basic token or an assumption.

Parallel composition For any agents A_{1} and A_{2}, their parallel composition, written (A_{1}, A_{2}), is the agent which on an input store z alternately applies A_{1} and A_{2} (in any order), until no progress can be made (that is, a value is reached which is a fixed-point of both). It is not hard, though a bit tedious, to show that as long as both A_{1} and A_{2} are executed “fairly” the resulting store does not depend on the order of application of the agents.^{5} In terms of fixed-points, parallel composition has a startlingly simple denotation:

(A_{1}, A_{2}) = A_{1} ∩ A_{2}

That is, the set of fixed-points of (A_{1}, A_{2}) is exactly the intersection of the set of fixed-points of A_{1} and A_{2}.

Parallel composition is the fundamental combinator for treating a collection of agents as a single agent; in TMS-terminology, for treating a collection of consumers as a single consumer.

With and All combinators We now introduce a combinator which exploit the structure of tokens in D_{A(B)}. The in combinator is of the form:

                             in e do A

Intuitively, the idea is to isolate just the constraints in the store which are in force given the assumptions e, and to execute A in such a store. More operationally, to run in e do A in the store u, the system isolates just the constraints u′ that hold in the environment e, (logically, e′ is just the (⊢_{A(B)}- closure) of the set e ∪ u), runs A in u′, and then adds to u the constraint (e, A(u′)). More precisely, the definition is:^{6}

in e do A = λz.\overline{z ∪ (e, A(\overline{e ∪ z}))}

Theorem 3.1 In terms of fixed-points:

in e do A = \{z ∈ |D_{a}| | \overline{z ∪ e} ∈ A\}

The calculation above is routine and easy.

5An execution sequence is fair if there is no agent which is infinitely often enabled in the sequence but never executed. The possibility of infinite execution sequences arises in the presence of recursion.

6Recall that for any u ⊆ D_{a}, \overline{u} is the smallest set containing u closed under the entailment relation ⊢_{a}.

Example 3.3 The agent:

in {A_{1}, A_{2}} do (X = 1 → Y > 3)

is identical to the simple ask-tell agent:

({A_{1}, A_{2}}, X = 1) → ({A_{1}, A_{2}}, Y > 3)

In fact, as the next theorem demonstrates, for every finite (recursion-free) program containing the in combinator, there is an equivalent program without the in combinator. But the whole point of the (in e do A) construction is that A can in general be a very complex (perhaps even recursively defined agent) and the translation may not be as straightforward as above. Besides this gives a conceptually simple way of separating the context from the agent which it is desired to run in that context.

Theorem 3.2 This combinator satisfies the following laws:

in e do c = (e, c)
in e do (in e′ do A) = in (e ∪ e′) do A
in e do (c → A) = (e, c) → (in e do A)
in e do (A_{1}, A_{2}) = (in e do A_{1}, in e do A_{2})

               in ∅ do A = A

The proofs of all these assertions are straightforward from their definitions.

Relationship with consumers. The “in ” combinator corresponds to the “implied-by” strategy for executing consumers [FdK88], as illustrated by the following example.

Consider the agent in {A, B} do (N → M). Suppose the current store has the label {{A}, {C}} for N and the label {} for M. To execute the agent, the environments of N in the “focus” {A, B} are selected; others are ignored. (In this case, only the environment {A} is selected.) For each such environment the corresponding tell action is performed. Thus, the net result of executing the above agent is to update the label for M to be {{A}}. Note that the same result would be obtained by expanding the agent, using the above theorem, to: ({A, B}, N) → ({A, B}, M).

all combinator. Using in , we can define the “all ” combinator: the agent

                              all A

is equivalent to the (infinite) conjunction of the agents (in e do A) for all sets of assumptions e. It should be clear that the same result is obtained if the conjunction above is limited to environments that are consistent in the current store. (There is no point in firing an agent in an inconsistent environment since no more information can be added in that environment.)

Example 3.4 The agent

all (N → M)

is the agent which checks for every context whether N holds in that context, and, if it does, adds M to that context.

Relationship with consumers. all A behaves very much like a basic consumer in the ATMS-architecture. In fact, the agent all (N → M) can be executed by installing a justification with antecedent N and consequent M: the usual ATMS-propagation algorithm will ensure that in each minimal, consistent environment in which N holds, M will also hold, thus providing a simple, finitary implementation.

Conditional constraint consumers can now readily be translated, as illustrated by the following example:

Example 3.5 Consider the following model of an AND-gate:

and(X, A, B) ::

(A = 0 → X = 0), (B = 0 → X = 0),

(A = 1 → X = B), (B = 1 → X = A),
(X = 1 → (A = 1, B = 1)).

and gate(M, X, A, B) ::
    M = ok → and(X, A, B),
    M = stuck at zero → X = 0,
    M = stuck at one → X = 1.

A typical invocation of such a device would be:

                       alland gate(M, X, A, B)

Operationally, such an agent checks for every environment e whether one of the constraints M = ok, M = stuck at zero, M = stuck at one holds in e. If so, the corresponding action is taken — in the first case, the agent and(X,A,B) is executed (under the assumption e), and in the latter two cases, the corresponding constraint is added to the store, contingent on e.

As discussed earlier, antecedents to justifications can only consist of nodes, not basic constraints. We can obtain the effect of basic constraints in antecedents, however, using ask operations. Suppose it is desired to use the basic constraint d in an antecedent. The effect can be achieved by introducing a node n_{d} corresponding to d, running the agent all (d → n_{d}) (recall that this is shorthand for all (∅, d) → (∅, n_{d})) and using n_{d} wherever it is desired to use d in an antecedent. As a result, in any context in which d can be shown to hold, the node n_{d} will be labelled “in”, as desired.

4 Conclusion

Above, we have discussed the notion of a general determinate cc language on top of an ATMS, given a precise description of the combinators, and shown how various “consumer-based” programming idioms in ATMS-based languages can be expressed in this set-up.

The addition of disjunctive agents to the above set-up does not present any new problems — it is straightforward to consider the denotation of every agent to be a closure operator over the Smyth-powerdomain and extend the two new combinators (all and in ) to that setting. Indeed, disjunctive agents are needed in order to capture the “choose” construct of ATMS-based languages, and hence account for “interpretation-construction” in this framework.

Similarly, the addition of existential quantification is straightforward. Semantically, this requires us to move from simple constraint systems to first-order constraint systems (which are sets of tokens equipped with an entailment relation and also a notion of substitution and existential quantifiers). Operationally, existential quantifiers provide a simple and elegant way to create new nodes.

Several tasks remain to be done. Conceptually, there does not seem to be any difficulty in generalizing to a first-order ATMS, that is, to a setting where assumptions are first-order constraints rather than just propositional variables. For example, we may want to consider each of Mode = ok, Mode = stuck at zero, Mode = stuck at one as different assumptions, and allow them to be appear in labels. Implementationally, we will have to allow the possibility that an environment may be inconsistent not because it subsumes a no-good but because it is internally inconsistent. For example, the environment {Mode = stuck at zero, Mode = ok} is internally inconsistent (because it is an unsatifiable constraint). As another example, we could allow assumptions to be positive or negative propositional literals, thus requiring the implementation to have a full-scale Clause Management System (CMS) [RdK87]. Further practical exploration of these possibilities is warranted.

Practical implementations of such languages — over a non-trivial constraint system — need to be developed. Perhaps the simplest non-trivial example would be to consider a first-order constraint language with constants and equality; the next step would be to allow constructors, thus getting the constraint system Herbrand. We hope to report on such implementations in future work.

Acknowledgements. Conversations with Philippe Codognet have been very helpful.

References

[deK86a] J. deKleer. An assumption based TMS. Artifical Intelligence, 28:127–162, 1986.

[deK86b] J. deKleer. Extending the ATMS. Artifical Intelligence, 28:163–196, 1986.

[deK86c] J. deKleer. Problem solving with the ATMS. Artifical Intelligence, 28:197–224, 1986.

[dKS80] Johan de Kleer and Gerald Jay Sussman. Propagation of constraints applied to circuit synthesis. Circuit Theory and Applications, 8:127 – 144, 1980.

[Doy79] Jon Doyle. A truth maintenance system. Artificial Intelligence, 12:231–272, 1979.

[FdK88] Kenneth D. Forbus and Johan de Kleer. Focusing the ATMS. In AAAI 88, 1988.

[GKK^{+}80] G.Gierz, K.H.Hoffman, K.Keimel, J.D.Lawson, M.Mislove, and D.S.Scott, editors. A compendium of continuous lattices. Springer-Verlag Berlin Heidelberg New York, 1980.

[Hen89] Pascal Van Hentenryck. Constraint satisfaction in logic programming. Logic Programming Series. MIT Press, 1989.

[JL87] Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In Proceedings of the SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 111–119. ACM, January 1987.

[JSS91] R. Jagadeesan, V. Shanbhogue, and V. Saraswat. Angelic nondeterminism in concurrent constraint programming. Technical report, System Sciences Laboratory, Xerox PARC, January 1991.

[Mah87] Michael Maher. Logic semantics for a class of committed-choice programs. In 4th International Conference on Logic Programming. MIT Press, May 1987.

[McA90] David McAllester. Truth maintenance. In Proceedings of AAAI, pages 1109–1116, July 1990.

[RdK87] Raymond Reiter and Johan de Kleer. Foundations of assumptionbased truth maintenance systems: a preliminary report. In Proceedings of AAAI-87, pages 183 – 188, August 1987.

[Sar87] Vijay A. Saraswat. The concurrent logic programming language cp: definition and operational semantics. In Proceedings of the SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 49–62. ACM, January 1987.

[Sar89] Vijay A. Saraswat. Concurrent Constraint Programming Languages. PhD thesis, Carnegie-Mellon University, January 1989. To appear, Doctoral Dissertation Award and Logic Programming Series, MIT Press, 1990.

[Sco76] Dana S. Scott. Data types as lattices. SIAM, 5(3):522–587, 1976.

[Sco82] Dana S. Scott. Domains for denotational semantics. In Proceedings of ICALP, 1982.

[SR90] Vijay A. Saraswat and Martin Rinard. Concurrent constraint programming. In Proceedings of Seventeenth ACM Symposium on Principles of Programming Languages, San Fransisco, January 1990.

[SRH91] Vijay A. Saraswat, Fransesca Rossi, and Pascal Van Hentenryck. Towards a general framework for constraint programming. Technical report, System Sciences Laboratory, Xerox PARC, February 1991.

[SRP91] Vijay A. Saraswat, Martin Rinard, and Prakash Panangaden. Semantic foundations of concurrent constraint programming. In Proceedings of Eighteenth ACM Symposium on Principles of Programming Languages, Orlando, January 1991.

[Ste80] Mark Jeffrey Stefik. Planning with constraints. PhD thesis, Stanford University, January 1980.

[Tar56] A. Tarski. Logics, semantics and meta-mathematics. Oxford University Press, 1956. Translated by J.H. Woodger.

A Closure operators

An operator over a partial order that is extensive, idempotent and monotone is called a closure operator (or, more classicaly, a consequence operator, [Tar56]). Closure operators are extensively studied in [GKK^{+}80]; continuous closure operators have been used in [Sco76] to characterize data-types.

We list here some basic properties. Every closure operator can be uniquely represented by its range (which is the same as its set of fixed points); the function can be recovered by mapping each input to the least element in the range above it. (In the following, we shall often confuse a closure operator with its range, writing x ∈ f to mean f(x) = x.) In fact, a subset of |D| is the range of a closure operator iff it is closed under glbs of arbitrary subsets. (Thus, the range of every closure operator is non-empty, since it must contain ⊤_{|D|} = ⊔∅.) This condition — which we shall call the determinacy condition in what follows — corresponds to the requirement that for any input there should be a unique least fixed-point of the given function above that input.

Also, it can be shown that a closure operator is continuous iff its range is closed under the lubs of directed subsets. The extensional partial order on closure operators (f ≤ g iff for all x, f(x) ≤ g(x)) translates into reverseinclusion on the set of fixed points: f ≤ g iff f ⊇ g. The identity operator I (with range |D|) is the bottom element; the operator which maps every element to ⊤ (and hence has range {⊤}) is the top element. In fact it is easy to see that the set of closure operators over |D| ordered by ⊇ is a complete (algebraic) lattice, with meets given by P ⊓ Q = {c ⊓ d | c, d ∈ P ∪ Q} and joins by P ⊔ Q = P ∩ Q. As we shall see, joins correspond to parallel composition, and one of the contributions of this paper is to point out that meets too have a very interesting computational interpretation.

In the presence of angelic non-determinism (disjunction), it becomes necessary to require the domain of denotations to be closed under a disjunction operation. When initiated in a store, such an operation can return multiple solutions — hence it becomes necessary to take the denotation to be some kind of mapping from |D| to sets of |D|. As discussed in [JSS91], the technically simplest solution is to take the domain of denotations to be the set of linear closure operators on the disjunctive power-domain P(|D|) (also called the Smyth powerdomain) of the underlying constraint system. Roughly, this power-domain has as elements upwards-closed subsets of |D|, ordered by reverse set-inclusion.^{7} A linear (also called distributive) closure operator over such a domain is a closure operator satisfying the property f(S) = ∪_{s∈S}f({s})^{8}. Intuitively, f(S) is the set of outputs of a process obtained by taking the union of the outputs produced by the process when started on any store s ∈ S.

For the present discussion, the crucial property of such closure operators that they too can be characterized by their “resting points” — those inputs ↑ c (for c ∈ |D|) which are fixed-points. Given such a set f_{S}, the function f can be recovered as the unique linear extension of the function λc. ↑ f_{S}∩ ↑ c. In fact, [JSS91] shows that the set of such closure operators is in one-to-one correspondence with the set of all Scott-compact subsets of |D|. The important point here is that no condition analogous to the determinacy condition (for closure operators over |D|) is required — -for instead of requiring that above any input there should be a least fixed-point, we can now take the result to be the (upwards-closure of) the set of all fixed-points above the input.

The set of linear closure operators over P(|D|) forms a distributive algebraic lattice with lubs given by intersection (of singleton fixed-point sets), and glbs by union.

7More precisely, the elements of the power-domain are required to be Scott-compact, that is, compact in the Scott-topology.

8Thus, linear functions do not combine the information present in two or more elements in the input set, but treat them separately.