Courses/CS 460/Fall 2005/Concurrent logic programming in Oz
From CSWiki
Contents |
[edit] Introduction
Logic programs may be understood both procedurally and declaratively. Traditionally one offers a declarative interpretation of a logic program and then explains that since the program must be executed by a computer, one is forced to provide a procedural interpretation as well.
Our approach turns that around. We first offer a procedural interpretation of Oz programs and then show how that interpretation may be understood as a search for one or more declarative statements—each of which will be a simple conjunction of primitive statements. The procedure followed by the program guarantees that when the program terminates, each of the found conjunctions holds. For each found statement, the variable bindings that satisfy it may also be returned.
[edit] Procedural description
When run under SearchAll (or some other search meta-program) an Oz program is understood as a computation that either
- runs to completion—in which case it produces a result,
- fails, i.e., terminates prematurely—in which case it does not produce a result, or
- runs forever—and therefore does not produce a result.
In addition, an Oz computation may split into multiple independent computations, each of which may itself run to completion (and produce a result), fail (and produce no result), or run forever (and produce no result).
SearchAll is a meta-function that takes a reference to a function as an argument. When one runs {SearchAll <fun>}, where <fun> refers to some function, SearchAll returns a list of all the results produced by all the computations that run to completion when the <fun> computation is started.
Caution. As currently implemented SearchAll waits until all spawned computations either succeed or fail. Therefore if the argument to SearchAll spawns infinitely many computations, or if it spawns a computation that performs a non-terminating recursive loop, SearchAll will never return any results. It is possible to write other SearchAll-like meta-functions that behave differently.- Generating multiple computations
- When an executing computation reaches a choice statement, it splits into multiple computations, one for each branch in the choice statement.
- When such a split occurs, the entire computation state is cloned. In particular, the stack and the variables in the original computation are all copied.
- Each of the new computations then proceeds independently—as if in a separate universe—from that point onward.
- Causing a computation to fail
- A computation fails if an unhandled exception occurs. The most common unhandled exception is a failed unification, but any unhandled exception (such as division by zero) causes a computation to fail. In logic programming, an exception is understood to identify a situation in which a computation becomes either internally inconsistent (as in a failed unification) or meaningless (as in division by zero). In either case the computation cannot proceed.
- A computation fails if it encounters an explicit fail statement. A fail statement can be used to terminate a computation whose variables have values that one doesn't want to allow. For example, to terminate a computation in which X < 0, one might write:
if X < 0 then fail end
There is also a more direct (although less familiar) way to accomplish the same thing. Instead of expressing the condition under which the computation should fail, one can express the condition under which the computation should be permitted to proceed. Write:
X >= 0 = true.
If the result of the test X >= 0 does not unify with true, the computation will fail.
[edit]
The Oz choice statement splits a computation into multiple independent computations.
Caution. Variables declared outside the original call to SearchAll are not copied. The SearchAll model for interactions with external variables is fairly complex. The bottom line is that (a) values may not be directly exported to external variables, but (b) external variables (whether they have values or not) may be imported into computations.
[edit]
There are two conditions under which a computation will fail, i.e., terminate prematurely.
[edit] Declarative interpretation
To understand an Oz program declaratively, consider computations, as described above, that are each deterministic (as a function of the choices they make) and that run to completion. Once such a computation has terminated, the collection of statements that it executed—which is necessarily finite because the computation terminated—may be understood as a declarative characterization of relationships among the program's variables and values. That is, as a computation proceeds it leaves behind it a trail of true statements. Since logic variables never change values, all those true statements are consistent with each other in that they all talk about the same variable values. The conjunction of all those statements is a declarative expression of a condition that is true about the program's variables and values.
If a number of spawned computations in different spaces terminate, then each represents a simple conjunction of true statements. The overall collection may then be understood as representing the disjunction of all the conjunctions. In other words, the final result is a disjunctive normal form expression that characterizes various ways in which the program's variables and values may be related to each other.
A very small example is worked out here.
[edit] Consequences and comments
According to the view presented here, an Oz program is not primarily intended to be understood declaratively. It is explicitly intended to be understood procedurally. The intent of the program as a procedure is to generate statement conjunctions as described above. (Each terminating computation does just that.) One can think of an Oz program as a guided search—a search for a set of true statement conjunctions, guided by the program written by the programmer.
This perspective provides a rationale for constructs, such as the cut in Prolog, for which no good declarative semantics is available. If the procedural purpose of a logic program is to generate a conjunction of base statements, the cut is just one more tool that the programmer has at his disposal to guide the search. Excluding potential paths in the search is simply the prerogative of the programmer. The set of results that the system finds may (or may not) be more limited than the set that would have been found were a larger number of paths explored. But that decision is up to the programmer.
Furthermore, the programmer may generate true statements that have nothing to do with each other. Consider the following Oz function.
fun {f} choice {f1} [] {f2} end end
This program generates true statements for f1 and for f2 whether or not f1 has anything to do with f2. It is simply up to the programmer to determine what kinds of true statements the system should explore.
This is quite different from the traditional view of logic programming. As Van Roy says (CTM p 640),[For a program] to have a logical semantics means that execution corresponds to deduction, i.e., that execution can be seen as performing inference and the result of procedure calls give valid tuples in a simple logical model, such as a model of the predicate calculus.In the view expressed here, execution is not deduction. Execution is asking whether a statement about to be executed is consistent with the set of statements already executed. If execution succeeds, the statement is consistent, and the new statement is added to the set of executed statements. If execution fails, computation along that path fails.
Traditionally, one considers a logic program to be a collection of axioms and a computation to be a deduction based on those axioms. This is a reductive process: can one reduce a query to a collection of ground clauses through the use of the axioms.
From our perspective, a program is not a collection of axioms. It is nothing other than the what any other program is: the expression of the imagination of the programmer. As a program executes, the system checks to see if the statements that it encounters are consistent with each other. If so it continues; if not it fails. This is a creative rather than a reductive process.
As Van Roy et. al. say in Logic programming in the context of multiparadigm programming: the Oz experience,The standard Oz approach is to use search only for problems that require it. … This is unlike Prolog, where search is ubiquitous: even procedure application is defined in terms of resolution, and thus search. In Oz, the choice statement explicitly creates a choice point, and search abstractions … encapsulate and control it.
Of course the two perspectives are equivalent at some level. Both are Turing complete. Writing a set of axioms is as creative as writing a set of functions and procedures that define search paths. But the approach we are proposing has the advantage that it more closely reflects the actual practice of writing logic programs. Almost exclusively, programmers write programs from a procedural perspective, not from a declarative perspective. The approach we are proposing preserves that perspective while still providing for a declarative interpretation for the result of a computation.
[edit] What does a Prolog clause or an Oz proc mean?
To clarify the preceding, one may ask about the meaning of a clause in logic programming or a proc in Oz. How does one understand these constructs?
In logic programming a clause is an axiom. If one writes, e.g., in Prolog,
grandparent(A C) :- parent(A, B), parent(B, C).
one is defining the meaning of grandparent/2: A is C's grandparent if there is a B such that A is B's parent and B is C's parent.
Then when one finds that a is c's grandparent, one can say that we know that because- we know that there is a b such that a is b's parent and that b is c's parent and
- that's the way grandparent is defined.
The question is, how is the Oz equivalent to be understood?
proc {GrandParent A C} B in {Parent A B} {Parent B C} end
One could understand it in exactly the same way as the Prolog clause.
The alternative is to understand it as a search rule: to look for grandparent-grandchild pairs, look for two parent-child pairs in which the child in one of the pairs is the parent in the other. Interpreted this way, the Oz program is more like a hint or a rule-of-thumb for finding grandparent-grandchild pairs than a definition of the grandparent-grandchild relationship.
Then when one finds that a is c's grandparent, one can say that we know that because- we know that there is a b such that a is b's parent and that b is c's parent and
- that's the way the program was instructed to look for grandparent-grandchild relationships.
In this example, this is a meaningless distinction. It's the same program, no matter which words one puts to it. But this contrast can be extended to situations in which Prolog has no convenient declarative semantics. One can add a cut to the Prolog clause and write:
grandparent(A C) :- parent(A, B), !, parent(B, C).
This clause is no longer an axiomatic definition of the grandparent relation.
The equivalent Oz program would be something like the following:
proc {FirstParent X Y}
{SearchAll proc {$ PC} P C in PC = P#C {Parent P C} end X#Y | _}
end
proc {GrandParent X Z} Y in {FirstParent X Y} {Parent Y Z} end
/* Note that one could do the same thing in Prolog using findall/bagof/setof. */
Since Oz programs of this sort are not intended to have a declarative semantics, no damage is done by the fact that they don't. Nonetheless, one does get a declarative result from the second Oz definition of GrandParent. One still gets GrandParent-GrandChild pairs, although perhaps not all of them. Of course the same is true for the Prolog program. The difference is that one doesn't have a rationale within the Prolog framework for why that happens. That is, what one can say about the result of the Prolog program no longer holds, but what one can say about the result of the Oz program still holds.
But even comparing the pure Prolog case with the procedural Oz case, are the two situations really so different? What one is really saying in the pure Prolog case is that what one finds satisfies one's definitions. What one is saying the the Oz case is that what one finds are what the search strategy revealed. But why are definitions any more to be trusted than a search strategy. After all, they are both written by people who may or may not have known what they were doing.
[edit] Combining the two approaches to get constraint programming
The essential difference between the two approaches is as follows. Traditional declarative programming starts with the notion of declarations—usually in the form of statements in the predicate calculus—and then shows how to execute those statements procedurally. The approach sketched here starts with procedural code and then shows how execution of that code produces statements about program variables and values. (This works because the procedural code operates on logical, i.e., assign-once, variables.)
A nice combination would use both. Use procedural code to generate statements about program variables and values. Apply declarations to the resulting statements to constrain the search even further and to ensure that it doesn't go in wrong directions. This is similar to the way that one would apply assertions to executing programs. It is potentially more powerful, though, in that the declarative code (the assertions) may further instantiate the results produced by the search rules. It is also different in that assertions in traditional programming languages apply to the current state of the computation. In our search and constrain model, the constraints are applied to the collection of currently derived statements, which in some reasonable sense is the state of the computation.
This seems to be a nice way of describing the Oz approach to constraint programming. The search rules are the distribution rules; the declarative code consists of the propagators. In this context the term propagator seems misleading. Propagators are really declarations (the assertions or constraints) that describe the required relationships among program variables and values. They are applied to the statements that the search code has produced to that point.
An Oz computation space is what we have been calling the collection of statements relating program variables and values produced by the search rules. The propagators are repeatedly applied to those statements (that computation space) until no more changes occur, i.e., no further instantiations (or narrowings as we will discuss below) occur. At that point the search rules (usually only one) extend the set of statements, usually by splitting the search into multiple paths.
To make this work effectively, Oz has developed a way to represent special kinds of relationships among program variables and values, in particular, that a variable is limited to values from a set of integers, often expressed as a range. The assertions (propagators) are implemented so that when applied to such statements, they may modify the statements (if possible) to guarantee that the assertions hold.
Oz implements this strategy by extending the notion of a logical variable to what one might call a constrained variable. When one writes something like
X :: 1#9
in an Oz program, one's intuition is that X has the range 1..9 as a value. As the program proceeds, X's range may shrink until X has a definite value. However, that intuitive picture is not consistent with the notion of logical (assign-once) variables. If X has the range 1#9 as a value, then that value should never change. The correct intuition is that X has no value, but its range of possible values has been narrowed from <anything> to the range 1..9.
Assertions, such as the propagator
X >: Y
are implemented so that they can both check to see that the required relationship holds and also narrow the ranges of constrained variables to make them hold. Narrowing ranges is similar to but more general than what traditional declarative statements do when they instantiate variables by assigning them values.
Oz has implemented constrained logical variables for integer variables only. A next step would be to expand the kinds of types to which constrained logical variables may be limited, e.g., sets of atoms, lists, etc.
The most important issue in doing this is to define the possible constraints to be implemented for each type. For example,
{Precedes: X1 X2 Xs) % Is the colon (:) the standard Oz convention for a constraint?
might be defined as a constraint on a list. It would require that X1 precedes X2 in the list of Xs.
The constraints to be applied to the integers are in some sense easy. We already know that they should include the basic arithmetic and ordering relations. The constraints to be defined for other range types need more thought—although by now we probably know what kinds of constraints one wants on most basic data types.
Stepping back, it's clear that application of constraints is much more efficient than search. This is so because every search step creates multiple computations whereas each constraint is a potential narrowing of the possible values in a given computation. So the larger challenge is to move as much of the work as possible from the search rules to the constraints. One way to do that is to define new constrained domain types as new problem domains appear. Thus it would be desirable to allow users to define data types and the constraining operations on them rather than hard-wiring them into the language.
[edit] Propagators
It's one thing to declare a constraint, say X <: Y. It's another entirely to use such a constraint to constrain. A propagator is a bit of procedural code that applies a constraint to a computation space.
Assume one has the following computation space.
{X::3#8; Y::2#6 X <:Y}
This is interpreted to mean X is in the range 3 .. 8; Y is in the range 2#6; X is required to be less than Y.
We can reason about constraints as follows.
- If X is required to be less than Y, X must be less than the maximum possible Y value. So X must be in the range 3 .. 5.
- If X is required to be less than Y, Y must be greater than the least possible X value. So Y must be in the range 4 .. 6.
So we now have the following.
{X::3#5; Y::4#6 X <:Y}
Notice that in both cases, we further restricted the ranges of X and Y. We are not allowed to expand ranges since once a variables has been constrained, a constraint cannot be relaxed. This is similar to but somewhat more general than the notion of an assign-once variable.
The steps taken by the two bullets above are taken by propagators that are associated with the X <: Y constraint. One might right such propagators as follows. (This is an invented notation and does not necessarily correspond to an Oz notation.)
proc ($) A::La#Ha B::Lb#Hb A <: B Ha >= Hb A::La#(Hb-1) end
This propagator is to be read as follows. If the computation state includes variables A and B with ranges as indicated; and if it also includes the constraint A <: B; and if Ha >=Hb, then execute the statement A::La#(Hb-1), i.e., add that statement to the computational state.
This propagator does not actually remove the statement A::La#Ha, it simply adds the new statement A::La#(Hb-1) that subsumes it.
Similarly the second propagator might be written as follows.
proc ($) A::La#Ha B::Lb#Hb A <: B La =< Lb B::(La+1)#Hb end
In our example, the result of executing these two propagators would add X::3#5 and Y::4#6 to our computational state. The old constraints on X and Y would not, strictly speaking be removed. But since the new constraints subsume the old ones, the old ones need no longer by considered.
A reasonable way to think about propagators is as forward chaining rules. They apply when certain conditions hold, in which case they add new statements to the computational store.
A question for which I don't have an answer is: what guarantees that the new statements are consistent with the existing statements—especially if the new statements restate constraints on existing variables? In our example, the rules clearly are consistent. But what's to prevent someone from writing inconsistent rules?
