Fully Distributed, AND/OR Parallel Execution of Logic Programs

Prabhakaran Raman Eugene W. Stark ^{∗}

TR-88/02 Department of Computer Science State University of New York at Stony Brook Stony Brook, NY 11794 USA E-mail : raman@sbcs.sunysb.edu

February 13, 1988

Abstract

We consider a distributed model for the execution of logic programs, in which a process is assigned to each node of the AND/OR tree for a program, and in which each process communicates directly only with its immediate neighbors in the tree. We derive an interpreter, or execution method, for this model, in which each node process maintains in its state a set of substitutions that represents a current local approximation to the set of answer substitutions. Execution consists of each process repeatedly sending its current state to its neighbors, and updating its state using information it receives. Eventually, “exact” answer substitutions accumulate at the root node, and are output. The interpreter supports both AND- and OR-parallelism in a completely unrestricted fashion. In particular, bidirectional communication can occur between two children of the same AND-node, a feature not present in previous work. We prove that our interpreter is sound and complete. The proof, which is nontrivial, hinges on an interesting property of information flow in the AND/OR-tree.

∗This research was supported in part by NSF Grant CCR-8702247.

1 Introduction

A logic program consists of a finite, nonempty set of definite Horn clauses, which are closed formulas of first-order logic of the form ∀x_{1},… x_{m}(g_{1} ∧… ∧ g_{n} ⊃ h), where g_{1},…, g_{n} and h are literals, or atomic formulas. It is customary, in the logic programming literature, to write such a formula as h ← g_{1},…, g_{n}, and to read it as “h if g_{1} and … and g_{n}.” The literal h is called the head of the clause, and the sequence of literals g_{1},… g_{n} is called its body.

Execution of a logic program begins when an input literal g, called the goal, has been specified. The objective of an interpreter, or execution method, is to solve the goal g. That is, the interpreter searches for an assignment of terms to the variables of g, such that if g′ is the instance of g obtained by substituting each occurrence of a variable by the corresponding term, then g′ is a logical consequence of the set of program clauses. Such an assignment is called an answer substitution. In general, there will be more than one, and possibly infinitely many, answer substitutions for a given program and goal, so the output of the interpreter will be a finite or infinite sequence of substitutions. An interpreter is sound if it only outputs answer substitutions, and complete if every ground answer substitution is an instance of some output substitution.

The operation of an interpreter presented with a logic program P and a goal g is conveniently described in terms of the AND/OR-tree [Kow79] for P and g. This (potentially infinite) tree contains two kinds of nodes, OR-nodes, which are labeled by literals, and AND-nodes, which are labeled by program clauses^{1}. The root of the tree is an OR-node, which is labeled by g. Each ORnode in the tree has one AND-node child for each program clause, a variant (renamed version) of which is used to label the child. Each AND-node in the tree, labeled by a clause h ← g_{1},…, g_{k}, has k OR-node children, which are labeled by variants of g_{1},…, g_{k}, respectively. Variants are selected so that the labels of distinct nodes in the tree have no variables in common. With each edge in the AND/OR-tree between a parent node m and a child node n we associate an edge equation, defined as follows: If m is an AND-node labeled by a clause h ← g_{1},…, g_{k} and n is the ith OR-node child of m, labeled by a variant g of g_{i}, then the edge equation is g_{i} = g. If m is an OR-node labeled by a literal g, and n is the AND-node child of m labeled by a clause h ← g_{1},…, g_{k}, then the edge equation is g = h.

It is a consequence of the completeness of the resolution inference rule for first-order logic in clausal form, that if an instance g′ of a goal g is a logical consequence of the clauses of program P, then there exists a proof of g′ from P whose representation in tree form is isomorphic to a subgraph of the AND/OR-tree for P and g. The subgraphs that correspond to proof trees are those finite subgraphs of the AND/OR-tree that are connected, conjunctive in the sense that each OR-node in the subgraph has exactly one child in the subgraph, and maximal in the sense that they are not properly contained in any other connected, conjunctive subgraph. We use the term neighborhood to refer to a connected subgraph of an AND/OR-tree, and we call maximal conjunctive neighborhoods prime. A prime neighborhood determines a proof tree once we have specified a substitution σ that solves the neighborhood, which means that it solves (unifies) the equation associated with each of the edges in the neighborhood.

The task of an interpreter presented with a logic program P and goal g can therefore be thought of as a search for substitutions that solve finite prime neighborhoods of the AND/OR-tree for P and g. Sequential interpreters for logic programs use a deterministic strategy to enumerate and solve finite prime neighborhoods. For example, the Prolog interpreter traverses the AND/OR-tree in a depth-first fashion. At each OR-node, one child is chosen for search, and the choice is recorded on stack. No choice is made at AND-nodes; rather, all children are searched in sequence. The choice information on the stack at any time determines a finite, conjunctive neighborhood of the AND/OR-tree. Also computed by the interpreter is a substitution that solves this neighborhood. This substitution is updated incrementally as the neighborhood is extended by the search procedure.

1Authors differ on which nodes are called “AND-nodes,” and which are called “OR-nodes.” Our usage agrees with [CK85] and is the opposite of [LM86].

Extension of the current conjunctive neighborhood can be interrupted in two ways: either the neighborhood is maximal, or else the addition of a new edge to the neighborhood results in a neighborhood having no solution. In the first case, the search is said to succeed, the neighborhood that has been searched is prime, and the substitution that has been computed is output as an answer. In the second case, the search is said to fail, and no answer is produced. In either case, the interpreter then backtracks to the most recent choice point (if any) on the stack, and restarts the search with the next untried choice. Such an interpreter, though sound, is obviously not complete since the presence of infinite branches in the AND/OR-tree can prevent some prime neighborhoods from being discovered.

The AND/OR-tree paradigm also suggests methods for exploiting parallelism in the execution of logic programs. For example, a Prolog-like interpreter may search all children of an OR-node in parallel, rather than choosing one and recording the choice for later backtracking. This kind of parallelism, called OR-parallelism, is particularly easy to exploit, since the search of each child of an OR-node can be carried out completely independently of the others, and the answers produced by all of them simply collected together. In AND-parallelism, the search of the children of an AND-node is carried out in parallel. This kind of parallelism is more difficult to exploit, since the presence of variables shared between the literals in the body of a clause implies that the answers produced by the searches of each of the children cannot merely be collected together, but must be merged in such a way that the semantics of shared variables is respected. The merging can be done either after the answers are produced, or it can be done during the search by having the child processes communicate with each other. The latter approach is attractive, since information provided by one child of an AND-node can be used to prune the search space of another, resulting in increased efficiency.

In this paper, we consider a model for parallel execution of logic programs in which a process is assigned to each node of the AND/OR-tree. Each process in our model executes asynchronously and independently of the others; thus the model supports unrestricted AND- and OR-parallelism. Processes obey a simple program, in which they repeatedly transmit their current state to their neighbors in the tree, and incorporate state information received from neighbors into their own state. Processes communicate directly only with their neighbors in the tree. From time to time, answer substitutions are output by the root process.

We consider the question of whether there exists a sound and complete interpreter for logic programs, based on this model, in which each node process maintains in its state a certain set of substitutions. Roughly, we would like this set of substitutions to represent an approximation to the set of answer substitutions for the subtree rooted at that node, based on information collected from other processes so far during execution. We would like processes to retain only substitutions that are in some sense relevant to the computation of answer substitutions at the root. Information arriving during execution could then be used to prune irrelevant substitutions. Also, we would like the substitutions maintained by a process to include only information about the bindings of variables that are “local” to the corresponding node, in the sense that they occur in the literal or clause labeling that node.

We show that such an interpreter does exist. Our interpreter has the following characteristics:

• The interpreter is fully distributed and asynchronous. No restriction is placed on the pattern of communication between nodes, except that a minimal “bottom-up fairness” assumption must be satisfied.

• The interpreter supports both AND- and OR-parallelism. In particular, information arriving from one child of an AND-node can propagate to another child, causing pruning of the search space for the latter. This bidirectional communication between AND-parallel processes is a feature not present in previous work.

• State information at a node is completely local to that node. In particular, no system-wide unique variable names are required.

• The interpreter is provably sound and complete.

The soundness and completeness proof, which is nontrivial, involves establishing an invariant relationship, between the state of a given node at any point during execution, and the “neighborhood” of all nodes from which the given node has received information so far. The proof hinges on an interesting property of information flow in the AND/OR-tree, which says that if m and n are adjacent nodes in the tree, then m always “knows more” than n about the state of the tree in the direction away from n.

In the form presented here, our interpreter is not suitable for direct implementation, since we ignore a number of issues of practical importance. For example, we assume that all processes (potentially infinitely many of them) exist from the start of execution, and do not consider how a practical interpreter would construct the AND/OR tree and allocate processes to its nodes. We also make no attempt to minimize communication costs between processes or to show how a process can efficiently update its state with information received in a message. Nevertheless, we feel the interpreter has great potential for the incorporation of various performance-improving optimizations and heuristics, which would ultimately lead to a practical algorithm. We are currently investigating possibilities here, some of which are sketched at the end of the paper.

Irrespective of the practical potential of our interpreter, we feel that its derivation and correctness proof represents an interesting exercise in distributing an algorithm over a number of processors. It should be pointed out that we did not originally discover the algorithm in the final form presented here, and subsequently prove its correctness. Rather, we began by looking for algorithms of the same general form, and then were guided to the final algorithm by solving problems that arose in the correctness proof. Although the idea underlying the the algorithm is not particularly difficult, to see why it works, and to deal correctly with the various special cases that arise, demands the construction of a careful correctness argument.

1.1 Informal Description of the Interpreter

To motivate the subsequent formal development, we give here a slightly more detailed description of our interpreter.

As mentioned above, our interpreter assigns a process to each node of the AND/OR tree. Each process maintains in its state a finite set of substitutions, which we call alternatives. At any point during execution, the set of alternatives for node n represents an approximation, based on the information received so far at node n, to a set of answer substitutions for the subtree rooted at n. Not all substitutions that are answers for the subtree rooted at n are necessarily covered by the set of alternatives. Rather, only those that are relevant to the computation of answers at the root need be retained. Processes refine their approximations by exchanging state information with their neighbors in the tree. Eventually, “exact” approximations accumulate at the root, where they are output.

Various complications arise when one attempts to elaborate the above ideas into an algorithm. First, we find it necessary to maintain slightly different state information at OR-nodes than at ANDnodes. The state of an AND-node contains a finite set of alternatives as described above. However, the state of an OR-node contains not just a single set of alternatives, but rather a vector of such sets, with one component for each of its children in the tree. Second, we must make sure that the state of each node contains information about which alternatives represent exact approximations. Ultimately, this information would be used by the root process to determine whether an alternative can be output as an answer.

The third difficulty we face is to discover the proper “update functions” which a node uses to incorporate information about its neighbors’ states into its own. We did not find the solution particularly obvious. In the end, there are four different kinds of update functions, to cover the four cases defined by whether an AND- or an OR-node is receiving state information from a parent or child. To give an idea of how the update functions work, we consider the case in which an AND-node n receives state information from its OR-node parent m. The other cases use similar ideas. Let g be the literal labeling the OR-node, and let h be the head of the clause labeling the AND-node. To compute its new set of approximate answer substitutions, the AND-node takes the vector of sets maintained by its parent OR-node, and selects out the component corresponding to itself. Call the old set of approximations for the AND-node Σ and the selected component of the state of the OR-node Σ_{n}. The AND-node then proceeds as follows: For each substitution σ in Σ and τ in Σ_{n}, renamings are applied to obtain variants σ′ and τ′ having no range variables in common. Then σ′ is applied to g to obtain gσ′, and τ′ is applied to h to obtain hτ′. A most general unifier μ (if it exists) of gσ′ and hτ′ is computed, and is composed with τ′ to obtain a substitution ρ = τ′μ. The set of all ρ obtained in this way from substitutions in Σ and Σ_{n} is collected, and subsumption is applied to reduce its size. The resulting set is the new set of alternatives for the AND-node.

1.2 Related Work

We classify previous work in parallel interpreters for logic programs on the basis of the ANDparallelism each supports. In [CK85, LM86, Kal86] AND-parallelism is restricted to independent goals (those that do not share variables). In [Wis86, KL87] AND-goals are evaluated bottom-up without any exchange of information between the AND-parallel goals. The “committed choice” languages of [CG86, Sha83] evaluate AND-goals in parallel with bidirectional exchange of information through shared variables, but eliminate OR-parallelism by having each OR-node “commit” to only one child. There are several proposals for purely OR-parallel interpreters that evaluate AND-goals sequentially. We note that no previous interpreters feature the full OR-parallelism coupled with bidirectional communication between AND-processes, which ours supports.

The AND/OR process model of Conery [CK83, CK85], was one of the first suggested models for parallel evaluation of logic programs. In this message-passing model, the AND/OR tree is developed dynamically, and processes are assigned to each node. Each OR-node develops all its children in parallel, thus the method supports OR-parallelism. However, AND-parallelism is restricted to independent goals. Independence is ensured by dynamically maintaining a dependency graph between literals in the body of a clause, and solving literals in parallel only when they can be determined to be independent. The method of [CK85] produces only one answer at a time, with alternative answers produced on demand by backtracking. Distributed backtracking is complex and expensive, and in [LM86] it is eliminated in favor of a multiple-answer data-driven model in which solutions to literals in the body of a clause are piped between AND-parallel processes in accordance with the dependency graph. Kale [Kal87] has pointed out that both methods [CK85] and [LM86] are incomplete, the authors’ claims to the contrary notwithstanding. In [Kal86], Kale has given a modified version, which is apparently complete. In [CDD85, Her86] it is shown how the expense of maintaining the dependency graphs can be reduced by compile-time preprocessing.

In [Wis86] and [KL87], AND-parallelism is supported by computing answers in a bottom-up fashion, and merging answer sets for separate conjuncts to resolve conflicting bindings for shared variables. Whereas [KL87] merges the answers incrementally, [Wis86] does not merge the answers until one of the conjuncts has produced all answers, and his method fails to be complete for this reason [Kal87]. In both methods, the bottom-up approach means that it is impossible for the answers produced by one conjunct to affect the computation of answers by a parallel conjunct.

The “committed-choice” languages of [CG86] and [Sha83] evaluate AND-goals in parallel with bidirectional exchange of information through shared variables. However, OR-parallelism is eliminated by “committing” to only one child of each OR-node. At the other extreme are the fully OR-parallel interpreters [YN84, UT83, WADK84, CH83, GTM84, LP84] which evaluate AND-goals sequentially. Other approaches are taken by Pollard [Pol81], who proposes a rather complex sharedmemory AND/OR parallel model, and in [CJ87], where we find a theorem-proving-style model that does not attempt to use AND- or OR-parallelism but rather distributes work between processors based on locality of data.

1.3 Outline of the Paper

The remainder of the paper is organized as follows: In Section 2, we introduce some preliminary material, leading up to a formal definition of an “interpreter.” In Section 3 we present our interpreter, which we call the “basis sets interpreter.” In Section 4 we prove that the basis sets interpreter is correct. The proof is accomplished by using “simulations” to compare the basis sets interpreter to an abstract interpreter whose correctness is obvious. Finally, in Section 5, we summarize what has been achieved and point out possibilities for future work.

2 Logic Programs and Interpreters

Let a countably infinite set V of variables be fixed. If S is a first-order signature, then let T_{S}, A_{S} and C_{S} denote, respectively, the set of all terms, literals (atomic formulas), and clauses constructed from variables in V and symbols in S. We write vars(e) to denote the set of all variables occurring in an expression (term, literal, or clause) e.

A logic program P is a pair (S, C), where S is a first-order signature, and C ⊆ C_{S} is a nonempty, finite set of definite Horn clauses. We use the customary notation h ← g_{1},…, g_{k} to denote a clause in C.

2.1 Substitutions

Since our results depend heavily on properties of substitutions, we require a careful development of the pertinent definitions. We shall always speak of substitutions under the assumption that a first-order signature S has been specified in advance.

A substitution is a function σ : V → T_{S}, where V is a subset of V, called the domain of σ and denoted dom(σ). The set {v ∈ dom(σ) : σ(v) ≠ v} is called the support of σ and is denoted supp(σ). The range variables rvars(σ) of σ is the set ⋃{vars(σ(v)) : v ∈ dom(σ)}. We say that σ is ground if rvars(σ) = ∅. Substitutions σ and σ′ are called range-disjoint if rvars(σ) ∩ rvars(σ′) = ∅. If e is an expression, and σ is a substitution with vars(e) ⊆ dom(σ), then define the application of σ to e to be the result of replacing each occurrence of a variable v in e by the term σ(v), in the usual way. We write eσ to denote the application of σ to e.

We distinguish two special kinds of substitutions, “global” and “local.” A substitution σ is called global if dom(σ) = V and local if dom(σ) is a finite subset of V. If σ is a substitution, and τ is a global substitution, then the composition of σ and τ is the substitution στ, with dom(στ) = dom(σ), such that x(στ) = (xσ)τ for all x ∈ dom(σ). Note that στ is defined when, and only when, τ is global. In particular, the composition of arbitrary global substitutions is defined.

If σ is a substitution and V ⊆ V, then the restriction of σ to V is the substitution σ V such that dom(σ V) = dom(σ) ∩ V, and (σ V)(v) = σ(v) for all v ∈ dom(σ) ∩ V. Note that for all substitutions σ, all global substitutions ρ, and all sets of variables V, we have (σρ) V = (σ V)ρ. If supp(σ) ∩ supp(τ) = ∅, then the union of σ and τ is the substitution σ ∪ τ such that dom(σ ∪ τ) = dom(σ) ∪ dom(τ) and

v(σ ∪ τ) = \{ \begin{matrix}vσ, & if v ∈ supp(σ), \\ vτ, & if v ∈ supp(τ), \\ v, & for all other v ∈ dom(σ) ∪ dom(τ). \end{matrix}

A renaming is a global substitution that is an injection from V to V. A particularly important renaming is the identity global substitution id. An expression e′ is a variant of e iff e′ = eρ for some renaming ρ. Similarly, a substitution σ′ is a variant of σ if σ′ = σρ for some renaming ρ. We shall need to obtain variants of expressions and substitutions in a standardized fashion. Therefore, let us fix a range-disjoint pair of renamings ω and ω′ (such a pair exists because V is infinite).

A substitution σ subsumes a substitution τ, and we write σ ∼ τ, if there exists a global substitution ρ such that τ = σρ. The relation ∼ is easily seen to be reflexive and transitive, moreover if σ ∼ τ and τ ∼ σ, then τ is a variant of σ.

Expressions e and e′ are are called unifiable if there exists a global substitution τ, called a unifier, such that eτ = e′τ. Similarly, substitutions σ and σ′ are unifiable if there exists a global substitution τ such that στ = σ′τ. A unifier μ of a pair of expressions or substitutions is called most general if μ ∼ τ for any other unifier τ of that pair of expressions or substitutions. We have the following standard result:

Proposition 2.1 (Unification Theorem) If a pair of expressions or local substitutions has a unifier, then it has a most general unifier.

Let mgu denote a function that maps each unifiable pair of expression or local substitutions to a most general unifier.

2.2 AND/OR Trees

Suppose P = (S, C) is a logic program, and g is a literal, which we call the goal. An AND/OR tree for P and g is a (potentially infinite) node-labeled, bipartite tree T = (A, O, r, E, L), where

• A ∪ O is the set of nodes, with A the set of AND nodes and O the set of OR nodes,

• r ∈ O is the root node,

• E ⊆ (A × O) ∪ (O × A) is the set of directed edges,

• L is the labeling map, which assigns a literal to each OR node, and a clause from C to each AND node,

such that the following conditions hold:

1. L(r) = g.

2. For each OR node o, there is exactly one child a of o for each clause h ← g_{1},…, g_{k} in C, and L(a) is a variant of that clause.

3. For each AND node a, if L(a) = h ← g_{1},…, g_{k}, then a has exactly k children, o_{1},…, o_{k}, and L(o_{i}) is a variant of g_{i}, for 1 ≤ i ≤ k.

4. If m and n are distinct nodes, then L(m) and L(n) have no variables in common.

It follows from these conditions that two AND/OR trees for P and g are variants of each other in the sense that the underlying trees are isomorphic, and corresponding node labels are variants. Since nothing we shall say depends in any way on a particular choice of variables in the node labels, we shall henceforth speak of the AND/OR tree for P and g as if it were unique.

When considering an AND/OR tree T, we write m ≺ n or m = parent(n) if node m is the parent of node n, m ≺^{∗} n if m is an ancestor of n, and m ∧ n for the least common ancestor of m and n. We write LV_{n} for the set of local variables of node n; that is, for the set vars(L(n)). We write LV for ⋃_{n∈A∪O} LV_{n}.

A set U of nodes of T is conjunctive if for each m, n ∈ U, either m ∧ n is an AND node, or else one of m, n is an ancestor of the other. We say that nodes m, n are conjunctive if the set {m, n} is conjunctive, and that node m is conjunctive with a set of nodes U if {m} ∪ U is conjunctive. A connected set U of nodes of T is called a neighborhood in T. If U is a neighborhood, and n ∈ U then U is called a neighborhood of n. A neighborhood is prime if it is maximal conjunctive; that is, if it is conjunctive and is not a proper subset of any conjunctive neighborhood. Clearly, every conjunctive neighborhood (in particular, a neighborhood consisting of a single node) is contained in a prime neighborhood.

To each pair of nodes (m, n) in T, with m ≺ n, we define the associated edge equation to be the pair of literals (l, l′) defined as follows:

• If m ∈ A, L(m) = h ← g_{1},…, g_{k}, node n ∈ O is the child of m corresponding to g_{i}, and L(n) = g, then l = g_{i} and l′ = g.

• If m ∈ O, L(m) = g, and L(n) = h ← g_{1},…, g_{k}, then l = g and l′ = h.

A substitution σ solves neighborhood U if LV_{n} ⊆ dom(σ) for all n ∈ U and if for all edges (m, n) in U, with associated edge equation (l, l′), we have lσ = l′σ. We say σ solves edge (m, n) if σ solves the neighborhood {m, n}. Clearly, if τ solves some finite prime neighborhood P (of r) in the AND/OR tree for P and g, then application of τ to P yields a proof tree for gτ from axioms C. Conversely, if an instance g′ of g is provable from axioms C, then there exists a substitution τ and a finite prime neighborhood P in the AND/OR tree for P and g, such that τ solves P and such that g′ = gτ. Thus, we say that a substitution σ is an answer for program P and goal g if σ = τ LV_{r}, where τ solves some finite prime neighborhood P (of r) in the AND/OR tree for P and g.

2.3 Interpreters

In general, an “interpreter” for logic programs is an algorithm, which accepts as input a logic program P and a goal g, and produces as output a (possibly infinite) sequence of substitutions σ_{0}, σ_{1},… with common domain LV_{r}. An interpreter is “sound” if each σ_{i} is an answer for P and g, and “complete” if whenever σ is a ground answer for P and g, then σ_{i} ∼ σ for some i ≥ 0.

In this paper, we are concerned with interpreters of a specific form: namely, those in which a program P with goal g is executed by a distributed algorithm in which one process is assigned to each node of the AND/OR tree for P and g. Each process executes a simple program, in which it repeatedly transmits its entire current state to its neighbors in the tree, and incorporates into its state the information it receives from its neighbors.

Formally, we define an interpreter to be a function I that takes an AND/OR tree, and annotates it with the following information:

• To each node n is assigned:

– A set Q_{n}^{I} of states.

– A distinguished element ι_{n}^{I} ∈ Q_{n}^{I}, called the initial state.

• To the root r is assigned an output function O^{I} that maps Q_{r}^{I} to sets of substitutions with domain LV_{r}.

• To each directed edge (m, n), with m ≺ n, is assigned a pair of update functions:

δ_{mn}^{I} : Q_{m}^{I} × Q_{n}^{I} → Q_{n}^{I}, δ_{nm}^{I} : Q_{n}^{I} × Q_{m}^{I} → Q_{m}^{I}.

The update function δ_{mn}^{I} (δ_{nm}^{I}) is used by node n (node m) to compute its new state after receiving a message from node m (node n).

If T is an AND/OR tree and I is an interpreter, then I(T) denotes the annotated tree obtained by applying I to T.

A global state for an annotated tree is a vector q̄ = (q_{n} : n ∈ A ∪ O), where q_{n} ∈ Q_{n} for all n ∈ A ∪ O. We write q̄^{n} to denote the component q_{n} of q̄. A transition is an expression of the form q̄⟶^{mn}r̄, where q̄, r̄ are global states and m, n are adjacent nodes, such that for all p ∈ A ∪ O,

r̄^{p} = \{ \begin{matrix}δ_{mn}(q̄^{m}, q̄^{n}), & if p = n, \\ q̄^{p}, & otherwise. \end{matrix}

A schedule for an annotated tree is an infinite sequence of ordered pairs

(m_{0}, n_{0}), (m_{1}, n_{1}),…,

where for each i ≥ 0, the nodes m_{i} and n_{i} are adjacent. A schedule is bottom-up-fair if it contains as a subsequence a bottom-up traversal of a neighborhood P, whenever P is finite and prime. For example, every schedule that contains infinitely often each edge (n, m) with m ≺ n, is bottomup-fair. Each schedule for an annotated tree determines a corresponding computation, which is a sequence of transitions of the form:

q̄_{0} ⟶^{m_{0}n_{0}}q̄_{1} ⟶^{m_{1}n_{1}} …,

where q̄_{0} = (ι_{n} : n ∈ A ∪ O) is the initial global state.

A global state q̄ is reachable if it appears in some computation. A property of global states is called invariant if it holds for all reachable global states, and inevitable if it holds for some state in every computation corresponding to a bottom-up-fair schedule. A property P of global states is inductive if P holds of the initial global state, and whenever q̄⟶^{mn}r̄, if P holds of q̄, then P holds of r̄.

Proposition 2.2 (Computational Induction) If a property of global states is inductive, then it is invariant.

An interpreter I is sound if for every AND/OR tree T corresponding to a logic program P and goal g, it is invariant for global states q̄ of the annotated tree I, that every element of O(q̄^{r}) is an answer for P and g. An interpreter I is complete if for every AND/OR tree T corresponding to P and g, and every ground answer σ for P and g, it is inevitable for global states q̄ of I(T) that there exists τ ∈ O(q̄^{r}) with τ ∼ σ. We say that an interpreter is correct if it is both sound and complete.

3 The Basis Sets Interpreter

In this section we define our interpreter, which we call the basis sets interpreter. Each process in the basis sets interpreter maintains in its state a finite set of substitutions, which we shall call alternatives. At any time during execution, the set of alternatives at node n represents an approximation, based on the information received so far at node n, to a set of answer substitutions for the subtree rooted at n. The state of each node must also contain information about which alternatives represent exact approximations. Ultimately, this information is used by the root process to determine which alternatives can be output as answers. Thus, nodes actually maintain two sets of alternatives, “upper bound” alternatives, which approximate all possible answers, and “lower bound” alternatives, which are those approximations that are known to be exact.

3.1 Preliminary Definitions

Suppose an AND/OR tree T has been given and n is a non-root node in T. We first define operations ⇐_{n} and ⇒_{n} on sets of substitutions. Suppose m ≺ n in T, and (l, l′) is the equation associated with the edge (m, n). Suppose τ and τ′ are substitutions, with LV_{m} ⊆ dom(τ) and LV_{n} ⊆ dom(τ′). Recall that we had fixed a range-disjoint pair of renamings ω and ω′. If lτω and l′τ′ω′ are unifiable, with μ = mgu(lτω, l′τ′ω′), then define

τ ⇐_{n} τ′ = (τωμ) LV_{m}, τ ⇒_{n} τ′ = (τ′ω′μ) LV_{n}.

Extend this definition to sets of substitutions Σ, Σ′ as follows:

Σ ⇐_{n} Σ′ = {τ ⇐_{n} τ′ : τ ∈ Σ, τ′ ∈ Σ′, lτω and l′τ′ω′ are unifiable}
Σ ⇒_{n} Σ′ = {τ ⇒_{n} τ′ : τ ∈ Σ, τ′ ∈ Σ′, lτω and l′τ′ω′ are unifiable}.

Next, we define operations ⋁ and ⋀ on sets of substitutions. If Σ is a set of substitutions, then define the span [Σ] of Σ to be the set of all τ such that σ ∼ τ for some σ ∈ Σ. We say that a set of substitutions Σ is independent if it is pairwise incomparable under ∼. A basis for Σ is an independent subset Ξ of Σ such that [Ξ] = [Σ]. Since the strict part of ∼ is well-founded on local substitutions, every set of such substitutions Σ contains a basis, and it is not difficult to see that two bases for the same set differ only up to renamings applied to their elements. Define a join of a collection {Σ_{i} : i ∈ I} of sets of local substitutions to be a basis for the set ⋃_{i∈I}[Σ_{i}]. Similarly, if I is nonempty, then define a meet of {Σ_{i} : i ∈ I} to be a basis for the set ⋂_{i∈I}[Σ_{i}]. Let ⋁ be an arbitrary function that maps each collection of local substitutions {Σ_{i} : i ∈ I} to a join ⋁_{i∈I} Σ_{i}, and let ⋀ map each nonempty collection of local substitutions {Σ_{i} : i ∈ I} to a meet ⋀_{i∈I} Σ_{i}.

Lemma 3.1 Suppose {Σ_{i} : i ∈ I} is a finite collection of sets of local substitutions, where each Σ_{i} has a finite basis. Then

1. ⋁_{i∈I} Σ_{i} is finite.

2. ⋀_{i∈I} Σ_{i} is finite, if I is nonempty.

Proof – For each i ∈ I, let Ξ_{i} be a finite basis for Σ_{i}.

(1) It suffices to show that there is a finite set Σ such that [Σ] = ⋃_{i∈I}[Σ_{i}]. Clearly, Σ = ⋃_{i∈I} Ξ_{i} is such a set.

(2) It suffices to show that there is a finite set Σ such that [Σ] = ⋂_{i∈I}[Σ_{i}]. We construct Σ by induction on the number of elements |I| of I. If |I| = 1, let i be the single element of I, then clearly Σ = Ξ_{i} has the required properties. If |I| = n + 1, then I = {i} ∪ I′, where I′ has n elements. Let Σ′ = ⋀_{i∈I′} Σ_{i}, which is finite by induction hypothesis. Define

Σ = {σωμ : σ ∈ Σ′, ξ ∈ Ξ_{i}, μ = mgu(σω, ξω′)}.

Clearly, Σ is finite. That [Σ] = ⋂_{i∈I}[Σ_{i}] follows easily by the properties of most general unifiers.

We note in passing that the proof of Lemma 3.1 can be refined to give an algorithm for computing ⋁_{i∈I} Σ_{i} and ⋀_{i∈I} Σ_{i}, when I and each Σ_{i} are finite.

Finally, some vector notation will significantly shorten our definitions. If n is a node, then we write (Ῡ^{p} : n ≺ p), (or just Ῡ when n is clear) to denote a vector of sets of substitutions, one for each child p of node n. The notation ⋁ Ῡ abbreviates ⋁_{n≺p} Ῡ^{p}. The notation ⋀ Ῡ is used similarly, when n is not a leaf. The notation Ῡ{p/Σ} stands for the vector Ῡ with its pth component replaced by Σ. We write Σ ⇒_{n} Ῡ as an abbreviation for (Σ ⇒_{n} Ῡ^{p} : n ≺ p), and similarly for ⇐_{n}.

3.2 The Interpreter

For the basis sets interpreter B,

• The state sets are defined as follows:

1. If n is an AND-node, then the set Q_{n}^{B} consists of all pairs (Υ, Λ̄), where Υ is a finite set of substitutions with domain LV_{n}, and Λ̄ = (Λ̄^{p} : n ≺ p) is a vector of finite sets of substitutions with domain LV_{n}.

2. If n is an OR-node, then the set Q_{n}^{B} consists of all pairs (Ῡ, Λ̄), where Ῡ = (Ῡ^{p} : n ≺ p) and Λ̄ = (Λ̄^{p} : n ≺ p) are vectors of finite sets of substitutions with domain LV_{n}.

The first (i.e. Υ) component of the state of a node represents the “upper bound” information, and the second (i.e. Λ) component represents “lower bound” information.

• The initial states are defined as follows:

1. If n is an AND-node, then ι_{n}^{B} = ({id LV_{n}}, ({} : n ≺ p)).

2. If n is an OR-node, then ι_{n}^{B} = (({id LV_{n}} : n ≺ p), ({} : n ≺ p)).

The symbol “id” denotes the identity global substitution.

• The output function O^{B} maps a state (Ῡ, Λ̄) ∈ Q_{r}^{B} to the set ⋁ Λ̄.

• The update functions for edge (m, n), with m ≺ n, are defined as follows:

1. If m is an AND-node and n is an OR-node,

δ_{mn}^{B}((Υ_{m}, Λ̄_{m}), (Ῡ_{n}, Λ̄_{n})) = (Υ_{m} ⇒_{n} Ῡ_{n}, Υ_{m} ⇒_{n} Λ̄_{n})
δ_{nm}^{B}((Ῡ_{n}, Λ̄_{n}), (Υ_{m}, Λ̄_{m})) = (Υ_{m} ⇐_{n} ⋁ Ῡ_{n}, (Λ̄_{m} ⇐_{n} ⋁ Ῡ_{n}){n/Υ_{m} ⇐_{n} ⋁ Λ̄_{n}}).

2. If m is an OR-node and n is an AND-node,

δ_{mn}^{B}((Ῡ_{m}, Λ̄_{m}), (Υ_{n}, Λ̄_{n})) = (Ῡ_{m}^{n} ⇒_{n} Υ_{n}, Ῡ_{m}^{n} ⇒_{n} Λ̄_{n})

δ_{nm}^{B}((Υ_{n}, Λ̄_{n}), (Ῡ_{m}, Λ̄_{m}))

= \{ \begin{matrix}(Ῡ_{m}\{n/Ῡ_{m}^{n} ⇐_{n} Υ_{n}\}, Λ̄_{m}\{n/Ῡ_{m}^{n} ⇐_{n} ⋀ Λ̄_{n}\}), & if n is not a leaf, \\ (Ῡ_{m}\{n/Ῡ_{m}^{n} ⇐_{n} Υ_{n}\}, Λ̄_{m}\{n/Ῡ_{m}^{n} ⇐_{n} Υ_{n}\}), & if n is a leaf. \end{matrix}

4 Correctness Proof

In this section, we prove the correctness of the basis sets interpreter. The technique we use is to relate this interpreter to a known correct interpreter through the use of “simulations,” which are mappings between interpreters that preserve and reflect correctness. To get started with this proof technique, we introduce the “neighborhoods interpreter,” in which the state of a process at any time is simply the neighborhood in the tree from which information has been received so far. Although the neighborhoods interpreter would not be useful in practice, it has the advantage of being obviously correct. Next, we refine this interpreter to obtain the “solution sets interpreter,” in which each process maintains sets of substitutions called “solution sets.” At any time during execution, the solution set maintained by node n is the set of all substitutions that are restrictions, to the local variables for node n, of solutions to intersections of prime neighborhoods with the neighborhood from which information has been received so far. We prove the correctness of the solution sets interpreter by exhibiting a simulation to it from the neighborhoods interpreter.

The solution sets interpreter has the same form as the basis sets interpreter, except that solution sets are infinite, whereas basis sets are finite. In fact, at any time during execution, the infinite solution set maintained by a process in the solution sets interpreter is the set of all instances of substitutions in the set maintained by the corresponding process in the basis sets interpreter. We use this fact to exhibit a simulation from the basis sets interpreter to the solution sets interpreter. Since simulations preserve and reflect correctness, the correctness of the basis sets interpreter follows.

4.1 Simulations

Suppose I and J are interpreters. If T = (A, O, r, E, L) is an AND/OR tree, then a simulation from I(T) to J (T) is a pair (R, F), where R is a property of global states of I(T) and F = {F_{n} : n ∈ A ∪ O} is a collection of functions with F_{n} : Q_{n}^{I} → Q_{n}^{J}, such that

1. R is inductive for I(T).

2. F(ι_{n}^{I}) = ι_{n}^{J} for all n ∈ A ∪ O.

3. F_{n}(δ_{mn}^{I}(q̄^{m}, q̄^{n})) = δ_{mn}^{J}(F_{m}(q̄^{m}), F_{n}(q̄^{n})) for all adjacent nodes m, n ∈ A ∪ O and all global states q̄ for I(T) that satisfy R.

4. O^{J} (F_{r}(q̄^{r})) = O^{I}(q̄^{r}) for all global states q̄ for I(T) that satisfy R.

Lemma 4.1 Suppose I and J are interpreters, such that for all AND/OR trees T, there exists a simulation from I(T) to J (T). Then I is correct iff J is correct.

Proof – The conditions in the definition of a simulation imply that, if a computation of I(T) and a computation of J (T) are determined by the same schedule, then each state in the computation of J (T) is the image under the simulation mapping of the corresponding state in the computation of I(T). Moreover, the output maps of I(T) and J (T) yield identical values on corresponding states. Since correctness is a property only of the set of output sequences of bottom-up-fair computations, it follows that I is correct iff J is correct.

4.2 The Neighborhoods Interpreter

The neighborhoods interpreter N is defined as follows: Given an AND/OR tree T,

• For each node n,

– The state set Q_{n}^{N} is the set of all finite neighborhoods of n.

– The initial state ι_{n}^{N} is the singleton neighborhood {n}.

• The output map O^{N} takes a finite neighborhood U of r to the set of all τ LV_{r}, where τ solves some prime neighborhood of r contained in U.

• For all edges (m, n), with m ≺ n, and all states q_{m} ∈ Q_{m}^{N}, q_{n} ∈ Q_{n}^{N},

δ_{mn}(q_{m}, q_{n}) = δ_{nm}(q_{n}, q_{m}) = q_{m} ∪ q_{n}.

It is easily checked that if m and n are adjacent nodes, q_{m} is a finite neighborhood of m, and q_{n} is a finite neighborhood of n, then q_{m} ∪ q_{n} is a finite neighborhood of both m and n; thus the update functions are well-defined.

Theorem 1 The neighborhoods interpreter N is correct.

Proof – Soundness is a direct consequence of the definition of the output function. To show completeness, suppose σ is an answer for T. Then σ = τ LV_{r}, where τ solves some finite prime neighborhood P of the root. By definition, every bottom-up-fair schedule for T embeds a bottomup traversal of P, and in any state subsequent to the completion of such a traversal, the set P is a subset of the state of the root. Thus, it is inevitably the case that σ is an output.

We now present an important property of information flow between nodes, upon which all our subsequent results depend. Intuitively, this property says that if m and n are adjacent nodes in the tree, then m always “knows more” than n about the state of the tree in the direction towards m. To state this formally, we need some additional notation.

If U is a neighborhood, and n is a node, then define

U ↓ n = {m ∈ U : m ∧ n = n}, U ↑ n = {m ∈ U : m ∧ n ≠ n}

The expressions U ↓ n and U ↑ n are read as “U below n,” and “U above n,” respectively.

If n is a node, and U, U′ are neighborhoods, then define INC_{n}(U, U′) to be true exactly when n is not the root node, U is a finite neighborhood of parent(n), U′ is a finite neighborhood of n, and the following inclusions hold:

U ↑ n ⊇ U′ ↑ n, U ↓ n ⊆ U′ ↓ n.

Lemma 4.2 Suppose T is an AND/OR tree. Let INC be the property of global states q̄ of N (T) which is true iff INC_{n}(q̄^{m}, q̄^{n}) holds for all nodes m, n with m ≺ n. Then INC is inductive.

Proof – Straightforward.

4.3 The Solution Sets Interpreter

In this section, we refine the neighborhoods interpreter to obtain the solution sets interpreter. This is done in several steps: First, we define functions primes_{n} and cprimes_{n} that map a neighborhood U of node n to certain “relatively prime” sub-neighborhoods of U. We then establish some homomorphic properties of these functions with respect to the operation ∪ on sets, used in the definition of the update functions for the neighborhoods interpreter. In particular, we show that under conditions that are invariant for the neighborhoods interpreter, the maps primes_{n} and cprimes_{n} translate ∪ to an operation ⋈_{n} on neighborhoods.

Second, we define a map solns, which takes a set of neighborhoods to the set of all substitutions that solve one of its elements. We show that, under certain conditions, the map solns is homomorphic with respect to ⋈_{n} and that it translates this operation to a related operation, which we also denote by ⋈_{n}, on sets of substitutions.

Third, we show that restriction of substitutions to variables local to a node is homomorphic with respect to ⋈_{n} on sets of substitutions, and that restriction translates ⋈_{n} into one of two operations, which we denote ←_{n} and →_{n}, on sets of substitutions. Finally, we combine all our results and obtain both the definition of the solution sets interpreter and a proof of its correctness.

4.3.1 Prime Neighborhoods

Suppose n is a node. For neighborhoods V and V′, and sets of neighborhoods Γ and Γ′, define

V ⋈_{n} V′ = (V ↑ n) ∪ (V′ ↓ n), Γ ⋈_{n} Γ′ = {V ⋈_{n} V′ : V ∈ Γ, V′ ∈ Γ′}.

The importance of ⋈_{n} is established by the following result.

Lemma 4.3 Suppose n is a node, and P, P′ are prime neighborhoods of n. Then P ⋈_{n} P′ is also a prime neighborhood of n.

Proof – To show that P ⋈_{n} P′ is conjunctive, suppose m, m′ ∈ P ⋈_{n} P′. Then either both m and m′ are in P ↑ n, or both m and m′ are in P′ ↓ n, or one of m, m′ is in P ↑ n and the other is in P′ ↓ n. In the first two cases, m and m′ are conjunctive because P and P′ are conjunctive. For the third case, suppose without loss of generality that m ∈ P ↑ n and m′ ∈ P′ ↓ n. Then m ∧ m′ = m ∧ n, which is either m or an AND node, by the fact that P is conjunctive and n ∈ P. Finally, suppose P ⋈_{n} P′ were not prime. There there would exist m, conjunctive with P ⋈_{n} P′, but not in P ⋈_{n} P′. There are two cases, either m ∧ n = n or m ∧ n ≠ n. If m ∧ n = n, then m would be conjunctive with P′ but not in P′, a contradiction with the fact that P′ is prime. Similarly, if m ∧ n ≠ n, then m would be conjunctive with P but not in P, contradicting the fact that P is prime.

Lemma 4.4 Suppose INC_{n}(U, U′). Then for all neighborhoods V, V′

(V ∩ U) ⋈_{n} (V′ ∩ U′) = (V ⋈_{n} V′) ∩ (U ∪ U′).

Proof –

(V ⋈_{n} V′) ∩ (U ∪ U′) = (V ↑ n ∪ V′ ↓ n) ∩ (U ∪ U′)
= (V ∩ U) ↑ n ∪ (V ∩ U′) ↑ n ∪ (V′ ∩ U) ↓ n ∪ (V′ ∩ U′) ↓ n
= (V ∩ U) ↑ n ∪ (V′ ∩ U′) ↓ n
= (V ∩ U) ⋈_{n} (V′ ∩ U′).

where the third equality uses the hypothesized inclusions.

Suppose n is a node and U is a finite neighborhood. Define primes_{n}(U), the set of prime neighborhoods of n, relative to U, by

primes_{n}(U) = {P ∩ U : P prime, n ∈ P }.

Define cprimes_{n}(U), the set of complete prime neighborhoods of n, relative to U, by

cprimes_{n}(U) = {P ∩ U : P prime, n ∈ P, P ↓ n ⊆ U}.

Intuitively, if the process for node n has heard from nodes in a neighborhood U, then primes_{n}(U) represents what node n knows about the prime neighborhoods in the AND/OR tree, and cprimes_{n}(U) consists of those elements of primes_{n}(U), which are “complete” in the sense that they correspond to proof trees rooted at n.

Lemma 4.5 Suppose n is a node and U is a finite neighborhood of n.

1. If n is an AND-node, then

(a) primes_{n}(U) = primes_{p}(U), if n ≺ p.

(b) cprimes_{n}(U) = \{ \begin{matrix}⋂_{n≺p} cprimes_{p}(U), & if n is not a leaf, \\ primes_{n}(U), & if n is a leaf. \end{matrix}

2. If n is an OR-node, then

(a) primes_{n}(U) = ⋃_{n≺p} primes_{p}(U).

(b) cprimes_{n}(U) = ⋃_{n≺p} cprimes_{p}(U).

Proof – Obvious.

Lemma 4.6 Suppose INC_{n}(U, U′) and n ≺^{∗} p. Then for all neighborhoods V ⊆ U ∪ U′, the following are equivalent:

1. V ∈ primes_{p}(U ∪ U′).

2. V ∩ U ∈ primes_{n}(U) and V ∩ U′ ∈ primes_{p}(U′).

3. V = W ⋈_{n} W′ for some W ∈ primes_{n}(U) and W′ ∈ primes_{p}(U′).

Proof – (1) implies (2): Suppose V ∈ primes_{p}(U ∪ U′). Then there exists a prime neighborhood P of p, such that V = P ∩ (U ∪ U′). Since n ≺^{∗} p, we know that P is also a prime neighborhood of n. Then V ∩U = P ∩U, and V ∩U′ = P ∩U′, hence V ∩U ∈ primes_{n}(U) and V ∩U′ ∈ primes_{p}(U′).

(2) implies (3): Suppose V ∩ U ∈ primes_{n}(U) and V ∩ U′ ∈ primes_{p}(U′). Let W = V ∩ U and W′ = V ∩U′. Then W ⋈_{n} W′ = ((V ∩U) ↑ n)∪((V ∩U′) ↓ n), which by the hypothesized inclusions is just (V ∩ U) ∪ (V ∩ U′) = V.

(3) implies (1): Suppose W ∈ primes_{n}(U) and W′ ∈ primes_{p}(U′) are such that V = W ⋈_{n} W′. Then there exist a prime neighborhood P of n and a prime neighborhood P′ of p such that W = P ∩ U and W′ = P′ ∩ U′. Let R = P ⋈_{n} P′, then clearly we have p ∈ R. By Lemma 4.4, R ∩ (U ∪ U′) = V. By Lemma 4.3, R is prime, thus showing that V ∈ primes_{p}(U ∪ U′).

Lemma 4.7 Suppose INC_{n}(U, U′) and n ≺^{∗} p. Then for all neighborhoods V ⊆ U ∪ U′, the following are equivalent:

1. V ∈ cprimes_{p}(U ∪ U′).

2. V ∩ U ∈ primes_{n}(U) and V ∩ U′ ∈ cprimes_{p}(U′).

3. V = W ⋈_{n} W′ for some W ∈ primes_{n}(U) and W′ ∈ cprimes_{p}(U′).

Proof – Similar to Lemma 4.6.

Lemma 4.8 Suppose n is an OR-node and INC_{n}(U, U′) holds. If m ≺ n and m ≺ l ≠ n, then the following are equivalent :

1. V ∈ cprimes_{l}(U ∪ U′).

2. V ∩ U ∈ cprimes_{l}(U) and V ∩ U′ ∈ primes_{n}(U′).

3. V = W ⋈_{n} W′ for some W ∈ cprimes_{l}(U) and W′ ∈ primes_{n}(U′). Proof – Similar to Lemma 4.6.

Lemma 4.9 Suppose INC_{n}(U, U′), m ≺ n ≺^{∗} p and m ≺ l ≠ n. Then 1. primes_{p}(U ∪ U′) = primes_{n}(U) ⋈_{n} primes_{p}(U′).

2. cprimes_{p}(U ∪ U′) = primes_{n}(U) ⋈_{n} cprimes_{p}(U′).

3. cprimes_{l}(U ∪ U′) = cprimes_{l}(U) ⋈_{n} primes_{n}(U′), if n is an OR-node. Proof – Immediate from Lemma 4.6, 4.7, 4.8.

The following is the main technical lemma upon which our correctness proof is based. It shows how information about prime sets relative to U ∪ U′ can be characterized in terms of information about prime sets relative to U and U′ separately. Lemma 4.10 Suppose INC_{n}(U, U′) and m ≺ n.

1. If m is an AND-node and n is an OR-node, then

(a) For all p with n ≺ p, i. primes_{p}(U ∪ U′) = primes_{m}(U) ⋈_{n} primes_{p}(U′). ii. cprimes_{p}(U ∪ U′) = primes_{m}(U) ⋈_{n} cprimes_{p}(U′).

(b) For all l with m ≺ l, i. primes_{m}(U ∪ U′) = primes_{m}(U) ⋈_{n} ⋃_{n≺p} primes_{p}(U′).

ii. cprimes_{l}(U ∪ U′) = \{ \begin{matrix}primes_{m}(U) ⋈_{n} ⋃_{n≺p} cprimes_{p}(U′), & if l = n, \\ cprimes_{l}(U) ⋈_{n} ⋃_{n≺p} primes_{p}(U′), & if l ≠ n. \end{matrix}

2. If m is an OR-node and n is an AND-node, then

(a) For all p with n ≺ p, i. primes_{n}(U ∪ U′) = primes_{n}(U) ⋈_{n} primes_{n}(U′). ii. cprimes_{p}(U ∪ U′) = primes_{n}(U) ⋈_{n} cprimes_{p}(U′).

(b) For all l with m ≺ l, i. primes_{l}(U ∪ U′) = \{ \begin{matrix}primes_{n}(U) ⋈_{n} primes_{n}(U′), & if l = n, \\ primes_{l}(U), & if l ≠ n. \end{matrix}

ii. cprimes_{l}(U ∪ U′) = \{ \begin{matrix}primes_{n}(U) ⋈_{n} ⋂_{n≺p} cprimes_{p}(U′), & if l = n, n not a leaf, \\ primes_{n}(U) ⋈_{n} primes_{n}(U′), & if l = n, n a leaf, \\ cprimes_{l}(U), & if l ≠ n. \end{matrix} Proof – All cases except (2bi) and (2bii) for l ≠ n are proved by straightforward applications of Lemma 4.9, and applying Lemma 4.5 to make use of the assumptions about m and n. We now argue the remaining cases.

(2bi) If l ≠ n, then primes_{l}(U ∪ U′) = primes_{l}(U) holds because the fact that m is an OR node and l ≠ n means that if P is a prime neighborhood of l, then P ↓ n = ∅, hence P ∩(U ∪U′) = P ∩U by INC_{n}(U, U′).

(2bii) Same argument as (2bi).

Suppose Γ and Γ′ are sets of neighborhoods. We say that Γ ⋈_{n} Γ′ is union-representable if each V ∈ Γ ⋈_{n} Γ′ is W ∪ W′ for some W ∈ Γ and W′ ∈ Γ′. The next technical property is required as a hypothesis by Lemma 4.12.

Lemma 4.11 Suppose INC_{n}(U, U′). Then each set defined by ⋈_{n} in Lemma 4.10 is union-repre-sentable.

Proof – It suffices to show that the following three sets are union-representable. Then each of the sets defined by ⋈_{n} in Lemma 4.10 can be shown to be union-representable by making use of Lemma 4.5.

If m ≺ n ≺^{∗} p and m ≺ l ≠ n. Then the following sets are union-representable :

1. primes_{n}(U) ⋈_{n} primes_{p}(U′).

2. primes_{n}(U) ⋈_{n} cprimes_{p}(U′).

3. cprimes_{l}(U) ⋈_{n} primes_{n}(U′), if n is an OR-node.

The proof of (1), (2), and (3) are immediate from Lemma 4.6, 4.7, and 4.8 respectively.

4.3.2 Solution Sets

If U is a neighborhood and n is a node, then the solution set solns(U) of U is the set of all substitutions σ, with dom(σ) = LV, such that σ solves U. We extend this definition to sets Γ of neighborhoods by: solns(Γ) = ⋃{solns(U) : U ∈ Γ}.

If σ is a substitution and n is a node, then define

σ ↑ n = σ (LV ↑ n), σ ↓ n = σ (LV ↓ n)

where

LV ↑ n = ⋃{LV_{m} : m ∈ (A ∪ O) ↑ n}, LV ↓ n = ⋃{LV_{m} : m ∈ (A ∪ O) ↓ n}.

Suppose m ≺ n, and (l, l′) is the equation associated with the edge (m, n). Suppose τ and τ′ are substitutions, with LV_{m} ⊆ dom(τ) and LV_{n} ⊆ dom(τ′). If ρ is a unifier of lτ and l′τ′, then define

τ ⋈_{n}^{ρ} τ′ = (τρ ↑ n) ∪ (τ′ρ ↓ n).

If n is a node and Σ, Σ′ are sets of substitutions, such that LV_{m} ⊆ dom(τ) for each τ ∈ Σ and LV_{n} ⊆ dom(τ′) for each τ′ ∈ Σ′, then define

Σ ⋈_{n} Σ′ = {τ ⋈_{n}^{ρ} τ′ : τ ∈ Σ, τ′ ∈ Σ′, ρ is a unifier of lτ, l′τ′}.

Lemma 4.12 Suppose m ≺ n, Γ is a set of neighborhoods of m, and Γ′ is a set of neighborhoods of n, such that Γ ⋈_{n} Γ′ is union-representable. Then

solns(Γ ⋈_{n} Γ′) = solns(Γ) ⋈_{n} solns(Γ′).

Proof – Suppose σ ∈ solns(Γ ⋈_{n} Γ′). Then σ solves some V ∈ Γ ⋈_{n} Γ′, so by hypothesis there exist W ∈ Γ and W′ ∈ Γ′ with V = W ∪ W′. Now, if σ solves V, then it solves W, W′ and edge (m, n). Thus, σ = σ ⋈_{n}^{ρ} σ ∈ solns(Γ) ⋈_{n} solns(Γ′), where ρ = id.

Conversely, suppose σ ∈ solns(Γ) ⋈_{n} solns(Γ′). Then σ = τ ⋈_{n}^{ρ} τ′, where τ ∈ solns(Γ) and τ′ ∈ solns(Γ′). Thus, there exist W ∈ Γ and W′ ∈ Γ′ such that τ solves W and τ′ solves W′. Now, σ solves W ⋈_{n} W′, because σ ↑ n = τρ ↑ n and τ solves W, σ ↓ n = τ′ρ ↓ n and τ′ solves W′, and lσ = lτρ = l′τ′ρ = l′σ. Hence σ ∈ solns(Γ ⋈_{n} Γ′).

4.3.3 Local Variables

Suppose m ≺ n, and (l, l′) is the equation associated with the edge (m, n). Suppose τ and τ′ are substitutions, with LV_{m} ⊆ dom(τ) and LV_{n} ⊆ dom(τ′). If ρ is a unifier of lτ and l′τ′, then define

τ ←_{n}^{ρ} τ′ = τρ LV_{m}, τ →_{n}^{ρ} τ′ = τ′ρ LV_{n}.

If n is a node and Σ, Σ′ are sets of substitutions, such that LV_{m} ⊆ dom(τ) for all τ ∈ Σ and LV_{n} ⊆ dom(τ′) for all τ′ ∈ Σ′, then define

Σ ←_{n} Σ′ = {τ ←_{n}^{ρ} τ′ : τ ∈ Σ, τ′ ∈ Σ′, ρ is a unifier of lτ and l′τ′}
Σ →_{n} Σ′ = {τ →_{n}^{ρ} τ′ : τ ∈ Σ, τ′ ∈ Σ′, ρ is a unifier of lτ and l′τ′}.

Lemma 4.13 Suppose m ≺ n, and Σ, Σ′ are sets of substitutions, such that LV_{m} ⊆ dom(τ) for all τ ∈ Σ and LV_{n} ⊆ dom(τ′) for all τ′ ∈ Σ′. Then

(Σ ⋈_{n} Σ′) LV_{m} = (Σ LV_{m}) ←_{n} (Σ′ LV_{n}), (Σ ⋈_{n} Σ′) LV_{n} = (Σ LV_{m}) →_{n} (Σ′ LV_{n})

Proof – We consider only the first equality, the other is similar. Let (l, l′) be the equation associated with the edge (m, n). First note that if τ and τ′ are substitutions, then a substitution ρ is a unifier of lτ and l′τ′ iff it is a unifier of l(τ LV_{m}) and l′(τ′ LV_{n}). Moreover, if ρ is a unifier of lτ and l′τ′, then

(τ ⋈_{n}^{ρ} τ′) LV_{m} = ((τρ ↑ n) ∪ (τ′ρ ↓ n)) LV_{m},  by definition
= τρ LV_{m},  LV_{m} ⊆ LV ↑ n
= (τ LV_{m})ρ LV_{m},  property of restriction
= (τ LV_{m}) ←_{n}^{ρ} (τ′ LV_{n}),  by definition.

The asserted equality now follows easily from this fact and the pointwise definitions of ⋈_{n} and ←_{n} on sets of substitutions.

4.3.4 The Solution Sets Interpreter We now define the solution sets interpreter S. The interpreter has the same form as the basis sets interpreter, except that solutions sets are infinite whereas basis sets are finite. It will be clear in Section 4.4 that the solution set maintained by a process in this interpreter is the set of all instances of substitutions in the set maintained by the corresponding process in the basis sets interpreter.

• The state sets are defined as follows:

1. If n is an AND-node, then the set Q_{n}^{S} consists of all pairs (Σ, Ῡ), where Σ is a set of substitutions with domain LV_{n}, and Ῡ = (Ῡ^{p} : n ≺ p) is a vector of sets of substitutions with domain LV_{n}.

2. If n is an OR-node, then the set Q_{n}^{S} consists of all pairs (Σ̄, Ῡ), where Σ̄ = (Σ̄^{p} : n ≺ p)

and Ῡ = (Ῡ^{p} : n ≺ p) are vectors of sets of substitutions with domain LV_{n}.

• The initial states are defined as follows:

1. If n is an AND-node, then ι_{n}^{S} = (Sub(LV_{n}), ({} : n ≺ p)).

2. If n is an OR-node, then ι_{n}^{S} = ((Sub(LV_{n}) : n ≺ p), ({} : n ≺ p)). Here Sub(LV_{n}) denotes the set of all substitutions with domain LV_{n}.

• The update functions for edge (m, n), with m ≺ n, are defined as follows:

1. If m is an AND-node and n is an OR-node,

δ_{mn}^{S}((Σ_{m}, Ῡ_{m}), (Σ̄_{n}, Ῡ_{n})) = (Σ_{m} →_{n} Σ̄_{n}, Σ_{m} →_{n} Ῡ_{n})
δ_{nm}^{S}((Σ̄_{n}, Ῡ_{n}), (Σ_{m}, Ῡ_{m})) = (Σ_{m} ←_{n} ⋃ Σ̄_{n}, (Ῡ_{m} ←_{n} ⋃ Σ̄_{n}){n/Σ_{m} ←_{n} ⋃ Ῡ_{n}})

2. If m is an OR-node and n is an AND-node,

δ_{mn}^{S}((Σ̄_{m}, Ῡ_{m}), (Σ_{n}, Ῡ_{m})) = (Σ̄_{m}^{n} →_{n} Σ_{n}, Σ̄_{m}^{n} →_{n} Ῡ_{n})

δ_{nm}^{S}((Σ_{n}, Ῡ_{n}), (Σ̄_{m}, Ῡ_{m}))

= \{ \begin{matrix}(Σ̄_{m}\{n/Σ̄_{m}^{n} ←_{n} Σ_{n}\}, Ῡ_{m}\{n/Σ̄_{m}^{n} ←_{n} ⋂ Ῡ_{n}\}), & n not a leaf, \\ (Σ̄_{m}\{n/Σ̄_{m}^{n} ←_{n} Σ_{n}\}, Ῡ_{m}\{n/Σ̄_{m}^{n} ←_{n} Σ_{n}\}), & n a leaf. \end{matrix}

In the above definitions we have used several abbreviations similar to those in the definition of the basis sets interpreter (see Section 3.1).

• The output function O^{S} maps a state (Σ̄, Ῡ) ∈ Q_{r}^{S} to the set ⋃ Ῡ. 4.3.5 Correctness of the Interpreter If n is a node and U is a finite neighborhood, then define

solns_{n}(U) = solns(primes_{n}(U)), csolns_{n}(U) = solns(cprimes_{n}(U)).

Lemma 4.14 Suppose m ≺ n and INC_{n}(U, U′).

1. If m is an AND-node and n is an OR-node, then

(a) For all p with n ≺ p, i. solns_{p}(U ∪ U′) LV_{n} = solns_{m}(U) LV_{m} →_{n} solns_{p}(U′) LV_{n}. ii. csolns_{p}(U ∪ U′) LV_{n} = solns_{m}(U) LV_{m} →_{n} csolns_{p}(U′) LV_{n}.

(b) For all l with m ≺ l, i. solns_{m}(U ∪ U′) LV_{m} = solns_{m}(U) LV_{m} ←_{n} ⋃_{n≺p} solns_{p}(U′) LV_{n}.

ii. csolns_{l}(U ∪ U′) LV_{m} = \{ \begin{matrix}solns_{m}(U) LV_{m} ←_{n} ⋃_{n≺p} csolns_{p}(U′) LV_{n}, & if l = n, \\ csolns_{l}(U) LV_{m} ←_{n} ⋃_{n≺p} solns_{p}(U′) LV_{n}, & if l ≠ n. \end{matrix}

2. If m is an OR-node and n is an AND-node, then

(a) For all p with n ≺ p, i. solns_{n}(U ∪ U′) LV_{n} = solns_{n}(U) LV_{m} →_{n} solns_{n}(U′) LV_{n}. ii. csolns_{p}(U ∪ U′) LV_{n} = solns_{n}(U) LV_{m} →_{n} csolns_{p}(U′) LV_{n}.

(b) For all l with m ≺ l,

i. solns_{l}(U ∪ U′) LV_{m} = \{ \begin{matrix}solns_{n}(U) LV_{m} ←_{n} solns_{n}(U′) LV_{n}, & if l = n, \\ solns_{l}(U) LV_{m}, & if l ≠ n. \end{matrix}

ii. csolns_{l}(U ∪ U′) LV_{m}

= \{ \begin{matrix}solns_{n}(U) LV_{m} ←_{n} ⋂_{n≺p} csolns_{p}(U′) LV_{n}, & if l = n, n not a leaf, \\ solns_{n}(U) LV_{m} ←_{n} solns_{n}(U′) LV_{n}, & if l = n, n a leaf, \\ csolns_{l}(U) LV_{m}, & if l ≠ n. \end{matrix}

Proof – The result follows immediately from Lemmas 4.10, 4.11, 4.12, and 4.13.

Theorem 2 Suppose T is an AND/OR tree. For each node n in T, define a map N S_{n} : Q_{n}^{N} → Q_{n}^{S} as follows:

1. If n is an AND-node, then define N S_{n}(U) = (solns_{n}(U) LV_{n}, (csolns_{p}(U) LV_{n} : n ≺ p)).

2. If n is an OR-node, then define

N S_{n}(U) = ((solns_{p}(U) LV_{n} : n ≺ p), (csolns_{p}(U) LV_{n} : n ≺ p)).

Then the pair (INC, N S) is a simulation from N (T) to S(T).

Proof – We must verify the conditions in the definition of a simulation. The output function condition is obvious. The initial state conditions follow directly from the fact that primes_{n}({n}) = {{n}}, and if n ≺ p, then primes_{p}({n}) = {{n}} and cprimes_{p}({n}) = {}.

To verify the update function conditions, we use Lemma 4.14. There are two cases, each with two subcases:

1. If m is an AND-node, n is an OR-node, and INC_{n}(U_{m}, U_{n}) holds, then

(a) N S(δ_{mn}^{N}(U_{m}, U_{n})) = δ_{mn}^{S}(N S(U_{m}), N S(U_{n})).

(b) N S(δ_{nm}^{N}(U_{n}, U_{m})) = δ_{nm}^{S}(N S(U_{n}), N S(U_{m})).

2. If m is an OR-node and n is an AND-node, and INC_{n}(U_{m}, U_{n}) holds, then

(a) N S(δ_{mn}^{N}(U_{m}, U_{n})) = δ_{mn}^{S}(N S(U_{m}), N S(U_{n})).

(b) N S(δ_{nm}^{N}(U_{n}, U_{m})) = δ_{nm}^{S}(N S(U_{n}), N S(U_{m})).

Each subcase is established by using the definitions of N S, δ_{mn}^{P}, and δ_{mn}^{S}, and then applying the corresponding part of Lemma 4.14. The details are straightforward, and are omitted.

Corollary 4.15 The solution sets interpreter is correct.

4.4 Correctness of Basis Sets Interpreter

We now establish the correctness of the basis sets interpreter by exhibiting a simulation from it to the solution sets interpreter. The simulation mapping is in fact the span mapping that was defined in Section 3.1. We use the following “lifting lemma” to show that span has the required properties.

Lemma 4.16 (Lifting Lemma) Suppose η and η′ are range-disjoint substitutions. Suppose substitutions τ and τ′ are such that η ∼ τ and η′ ∼ τ′. Let l, l′ be literals with vars(l) ⊆ dom(η) and vars(l′) ⊆ dom(η′). If lτ and l′τ′ have a unifier ρ, then lη and l′η′ are unifiable. Moreover, if μ = mgu(lη, l′η′), then there exists λ such that ημλ = τρ and η′μλ = τ′ρ.

Proof – Since η, η′ are range-disjoint, we may choose κ, κ′, with disjoint supports, such that ηκ = τ and η′κ′ = τ′. Let the substitution θ be defined as follows:

θ(v) = \{ \begin{matrix}vκρ, & if v ∈ supp(κ), \\ vκ′ρ, & if v ∈ supp(κ′), \\ vρ, & otherwise. \end{matrix}

Now, ρ is a unifier of lτ and lτ′, so θ is a unifier of lη and l′η′. Let μ = mgu(lη, l′η′), then μ ∼ θ, so there exists λ such that μλ = θ. Then ημλ = ηθ = τρ and η′μλ = η′θ = τ′ρ.

Lemma 4.17 Suppose m ≺ n, and Σ, Σ′ are sets of substitutions, such that LV_{m} ⊆ dom(τ) for all τ ∈ Σ and LV_{n} ⊆ dom(τ′) for all τ′ ∈ Σ′. Then

[Σ ⇒_{n} Σ′] = [Σ] →_{n} [Σ′], [Σ ⇐_{n} Σ′] = [Σ] ←_{n} [Σ′].

Proof – (1) and (2) are similar; we prove only (1).

Suppose σ ∈ [Σ ⇒_{n} Σ′]. Then there exists η ∈ Σ and η′ ∈ Σ′ such that lηω and l′η′ω′ are unifiable, and if μ = mgu(lηω, l′η′ω′), then there exists κ such that σ = (η′ω′μκ) LV_{n}. Let τ = ηωμκ and τ′ = η′ω′μκ, then σ = τ →_{n}^{ρ} τ′, where ρ = id. Since τ ∈ [Σ] and τ′ ∈ [Σ′], we have shown that

σ ∈ [Σ] →_{n} [Σ′].

Conversely, suppose σ ∈ [Σ] →_{n} [Σ′]. Then σ = τ →_{n}^{ρ} τ′ = (τ′ρ) LV_{n} for some τ ∈ [Σ], τ′ ∈ [Σ′], and unifier ρ of lτ and l′τ′. Let η ∈ Σ and η′ ∈ Σ′ be such that η ∼ τ and η′ ∼ τ′. It is easy to see that we also have ηω ∼ τ and η′ω′ ∼ τ′. Since ρ is a unifier of lτ and l′τ, by Lemma 4.16 lηω and l′η′ω′ are unifiable. Moreover, if μ = mgu(lηω, l′η′ω′), then there exists λ such that ηωμλ = τρ and η′ω′μλ = τ′ρ. Note that η ⇒_{n} η′ = (η′ω′μ) LV_{n} ∈ Σ ⇒_{n} Σ′. But then (η ⇒_{n} η′)λ = ((η′ω′μ) LV_{n})λ = (η′ω′μλ) LV_{n} = σ, thus showing that η ⇒_{n} η′ ∼ σ and hence that

σ ∈ [Σ ⇒_{n} Σ′].

Theorem 3 Suppose T is an AND/OR tree. For each node n in T, define a map BS_{n} : Q_{n}^{B} → Q_{n}^{B} as follows:

1. If n is an AND-node, then define BS_{n}(Ξ, Λ̄) = ([Ξ], ([Λ̄^{p}] : n ≺ p)).

2. If n is an OR-node, then define BS_{n}(Ξ̄, Λ̄) = (([Ξ̄^{p}] : n ≺ p), ([Λ̄^{p}] : n ≺ p)).

Let true denote the property that holds of all global states of B(T). Then the pair (true, BS) is a simulation from B(T) to S(T).

Proof – The proof is immediate from Theorem 2, Lemma 4.17, and the definition of ⋁ and ⋀.

Corollary 4.18 The basis sets interpreter B is correct.

5 Discussion

We have described a simple distributed interpreter for logic programs that exploits both AND- and OR-parallelism, and we have proved its soundness and completeness. A feature of our interpreter is that it supports bidirectional communication between AND-parallel goals. This feature is important because such communication can result in increased efficiency through pruning of irrelevant alternatives. A good example of an application in which such pruning would seem to be useful is alpha-beta minimax search.

There are several issues that must be addressed before a practical interpreter can be based on our results. Clearly, data and communication requirements of our interpreter must be optimized. For example, it is not necessary for processes to maintain the set of lower-bound alternatives separately from the upper-bound set. Rather, tags can be used to identify those elements of the upper-bound set that are also members of the lower-bound set. It is also unnecessary for processes to repeatedly send their entire state to their neighbors, since this state will mostly consist of information already known to the neighbor. We believe it is possible, though, to design a highly efficient protocol for the incremental communication of state information between nodes. Such a protocol would require the design of data structures with which sets of substitutions can be recorded, and the incremental updates efficiently computed. We can optimize the data structures by observing that the substitutions in a state are some instances of substitutions in the previous state and so on up to the initial state, and hence two substitutions in the current state can share the structure of their common ancestor substitutions.

The design of an interpreter to run on a particular parallel or distributed architecture must address the problems of how to dynamically construct the AND/OR tree, assign processes to processors and schedule processes assigned to the same processor. Solution to these problems will obviously depend on the particular architecture, and probably also on the properties of application programs to be run. It seems clear that a fully distributed implementation of the interpreter described here will probably not be desirable in most circumstances. Rather, it will probably be necessary for efficiency reasons to combine the tasks of a number of node processes into one. This can be done statically, for example by assigning one processor to handle the tasks of all AND-nodes labeled by the same program clause, or dynamically, for example by assigning one processor to handle the tasks of all nodes in some neighborhood of the AND/OR tree. The results of this paper will be useful in showing what must be accomplished by the processors to ensure soundness and completeness. It also seems clear that not all application programs will benefit from the completely unrestricted communication patterns supported by our model. However, as our model does not impose any restrictions other than a minimal bottom-up fairness on the pattern of communication between processes, we feel that it is easy to introduce performance-improving heuristics for scheduling communication between processes.

An important issue in the design of distributed interpreters is the problem of detection of duplicate goals and the elimination of such redundant computations. Ullman [Ull84] has proposed a method in which the states of all processes are sorted at fixed intervals, so that two or more processes with identical states (these correspond to duplicate goals in his method) can be detected. In such cases, only one of the processes is allowed to proceed while others wait for answers from that process. However, his method is not directly applicable to our interpreter because in our interpreter a goal can be affected by other goals conjunctive with it, and hence identical goals may not generate the same set of answers. The extension of Ullmans’ method to our interpreter merits further investigation.

References

[CDD85] Jung-Herng Chang, Alvin M. Despain, and Doug DeGroot. AND-parallelism of logic programs based on a static data dependency analysis. In Digest of Papers, Compcon85, pages 218–225, February 1985.

[CG86] Keith Clark and Steve Gregory. PARLOG : parallel programming in logic. ACM Transactions on Programming Languages and Systems, 8(1):1–49, January 1986.

[CH83] Andrzej Ciepielewski and Seif Haridi. A formal model for OR-parallel execution of logic programs. In R.E.A Mason, editor, Information Processing 83, pages 299–305, North-Holland, September 1983.

[CJ87] P. Daniel Cheng and J.Y. Juang. A parallel resolution procedure based on connection graph. In Sixth National Conference on Artificial Intelligence, pages 13–17, AAAI87, July 1987.

[CK83] J.S Conery and D.F. Kibler. AND parallelism in logic programs. Proceedings of 8th IJCAI, 539–543, August 1983.

[CK85] J.S Conery and D.F. Kibler. AND parallelism and nondeterminism in logic programs. New Generation Computing, 3:43–70, 1985.

[GTM84] A. Goto, H. Tanaka, and T. Moto-Oka. Highly parallel inference engine PIE—goal rewriting model and machine architecture. New Generation Computing, 2:37–58, 1984.

[Her86] M.V. Hermenegildo. An abstract machine for restricted AND-parallel execution of logic programs. In Lecture Notes in Computer Science, Vol 225, pages 25–39, Third International Conference on Logic Programming, Springer-Verlag, July 1986.

[Kal86] L.V. Kale. Parallel Architectures for Problem Solving. PhD thesis, SUNY Stony Brook, 1986.

[Kal87] L.V. Kale. ‘completeness’ and ‘full parallelism’ of parallel logic programming schemes. In Proceedings 1987 Symposium on Logic Programming, pages 125–133, August 1987.

[KL87] Michael Kifer and E. Lozinskii. Implementing logic programs as a database system. In Third International Conference on Data Engineering, February 1987.

[Kow79] R.A. Kowalski. Logic for Problem Solving. Elsevier North-Holland, 1979.

[LM86] Peyyun Peggy Li and Alain J. Martin. The SYNC model: a parallel execution method for logic programming. In Proceedings 1986 Symposium on Logic Programming, pages 223–234, IEEE, September 1986.

[LP84] Gary Lindstrom and Prakash Pananagaden. Stream-based execution of logic programs. In International Symposium on Logic Programming, pages 168–176, February 1984.

[Pol81] George H. Pollard. Parallel Execution of Horn Clause Programs. PhD thesis, Dept. of Computing, Imperial College, London, 1981.

[Sha83] Ehud Y. Shapiro. A subset of Concurrent Prolog and its Interpreter. Technical Report, ICOT Tokyo, 1983.

[Ull84] Jeffrey D. Ullman. Flux, sorting, and supercomputer organization for ai applications. Journal of Parallel and Distributed Computing, 133–151, 1984.

[UT83] Shinji Umeyama and Koichiro Tamura. A parallel execution model of logic programs. In Tenth International Symposium on Computer Architecture, pages 349–355, June 1983.

[WADK84] D.S. Warren, M. Ahamad, S.K. Debray, and L.V. Kale. Executing distributed prolog programs on a broadcast network. In Proceedings of the 1984 Logic Programming Symposium, February 1984.

[Wis86] Michael J. Wise. Prolog Multiprocessors. Prentice-Hall, 1986.

[YN84] Hiroshi Yasuhara and Kazuhiko Nitadori. ORBIT: a parallel computing model of prolog. New Generation Computing, 277–288, 1984.