Node:Procedural, Next:Occur, Previous:Declarative, Up:Prolog Intro

Procedural Semantics

Note that the declarative semantics makes no reference to the sequencing of goals within the body of a clause, nor to the sequencing of clauses within a program. This sequencing information is, however, very relevant for the procedural semantics which Prolog gives to definite clauses. The procedural semantics defines exactly how the Prolog system will execute a goal, and the sequencing information is the means by which the Prolog programmer directs the system to execute the program in a sensible way. The effect of executing a goal is to enumerate, one by one, its true instances. Here then is an informal definition of the procedural semantics. We first illustrate the semantics by the simple query

?- concatenate(X, Y, [a,b]).

We find that it matches the head of the first clause for concatenate/3, with X instantiated to [a|X1]. The new variable X1 is constrained by the new query produced, which contains a single recursive procedure call:

?- concatenate(X1, Y, [b]).

Again this goal matches the first clause, instantiating X1 to [b|X2], and yielding the new query:

?- concatenate(X2, Y, [])

Now the single goal will only match the second clause, instantiating both X2 and Y to []. Since there are no further goals to be executed, we have a solution

X = [a,b]
Y = []

i.e. a true instance of the original goal is

concatenate([a,b], [], [a,b])

If this solution is rejected, backtracking will generate the further solutions

X = [a]
Y = [b]

X = []
Y = [a,b]

in that order, by re-matching, against the second clause for concatenate, goals already solved once using the first clause.

Thus, in the procedural semantics, the set of clauses

H :- B1, ..., Bm.
H' :- B1', ..., Bm'.
...

are regarded as a procedure definition for some predicate H, and in a query

?- G1, ..., Gn.

each Gi is regarded as a procedure call. To execute a query, the system selects by its computation rule a goal, Gj say, and searches by its search rule a clause whose head matches Gj. Matching is done by the unification algorithm (see [Robinson 65] which computes the most general unifier, mgu, of Gj and H). The mgu is unique if it exists. If a match is found, the current query is reduced to a new query

?- (G1, ..., Gj-1, B1, ..., Bm, Gj+1, ..., Gn)mgu.

and a new cycle is started. The execution terminates when the empty query has been produced.

If there is no matching head for a goal, the execution backtracks to the most recent successful match in an attempt to find an alternative match. If such a match is found, an alternative new query is produced, and a new cycle is started.

In SICStus Prolog, as in other Prolog systems, the search rule is simple: "search forward from the beginning of the program".

The computation rule in traditional Prolog systems is also simple: "pick the leftmost goal of the current query". However, SICStus Prolog and other modern implementations have a somewhat more complex computation rule "pick the leftmost unblocked goal of the current query".

A goal can be blocked on one ore more uninstantiated variables, and a variable may block several goals. Thus binding a variable can cause blocked goals to become unblocked, and backtracking can cause currently unblocked goals to become blocked again. Moreover, if the current query is

?- G1, ..., Gj-1, Gj, Gj+1, ..., Gn.

where Gj is the first unblocked goal, and matching Gj against a clause head causes several blocked goals in G1, ..., Gj-1 to become unblocked, then these goals may become reordered. The internal order of any two goals that were blocked on the same variable is retained, however.

Another consequence is that a query may be derived consisting entirely of blocked goals. Such a query is said to have floundered. The top-level checks for this condition. If detected, the outstanding blocked subgoals are printed on the standard error stream along with the answer substitution, to notify the user that the answer (s)he has got is really a speculative one, since it is only valid if the blocked goals can be satisfied.

A goal is blocked if certain arguments are uninstantiated and its predicate definition is annotated with a matching block declaration (see Block Declarations). Goals of certain built-in may also be blocked if their arguments are not sufficiently instantiated.

When this mechanism is used, the control structure resembles that of coroutines, suspending and resuming different threads of control. When a computation has left blocked goals behind, the situation is analogous to spawning a new suspended thread. When a blocked goal becomes unblocked, the situation is analogous to temporarily suspending the current thread and resuming the thread to which the blocked goal belongs.