4.2.4 Declarative and Procedural Semantics

The semantics of definite clauses should be fairly clear from the informal interpretations already given. However, it is useful to have a precise definition. The declarative semantics of definite clauses tells us which goals can be considered true according to a given program, and is defined recursively as follows:

A goal is true if it is the head of some clause instance and each of the goals (if any) in the body of that clause instance is true, where an instance of a clause (or term) is obtained by substituting, for each of zero or more of its variables, a new term for all occurrences of the variable.

For example, if a program contains the procedure for concatenate/3, declared in ref-sem-pro, then the declarative semantics tells us that (A) is true, because this goal is the head of a certain instance of the second clause (K) for concatenate/3, namely (B), and we know that the only goal in the body of this clause instance is true, because it is an instance of the unit clause that is the first clause for concatenate/3.

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

concatenate([a], [b], [a,b]):-
   concatenate([], [b], [b]).

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 that 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 his program in a sensible way. The effect of executing a goal is to enumerate, one by one, its true instances. Here is an informal definition of the procedural semantics.

To execute a goal, the system searches forwards from the beginning of the program for the first clause whose head matches or unifies with the goal. The unification process [Robinson 65] finds the most general common instance of the two terms, which is unique if it exists. If a match is found, then the matching clause instance is then activated by executing in turn, from left to right, each of the goals (if any) in its body. If at any time the system fails to find a match for a goal, then it backtracks; that is, it rejects the most recently activated clause, undoing any substitutions made by the match with the head of the clause. Next it reconsiders the original goal that activated the rejected clause, and tries to find a subsequent clause that also matches the goal.

For example, if we execute the goal expressed by the query (A), then we find that it matches the head of the second clause for concatenate/3, with X instantiated to [a|X1]. The new variable X1 is constrained by the new goal produced, which is the recursive procedure call (B) and this goal matches the second clause, instantiating X1 to [b|X2], and yielding the new goal (C).

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

concatenate(X1, Y, [b])  (B)

concatenate(X2, Y, [])  (C)

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

X = [a,b]
Y = []

That is, the following is a true instance of the original goal:

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

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

X = [a]
Y = [b]

X = []
Y = [a,b]

in that order, by re-matching goals already solved once using the first clause of concatenate/3, against the second 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, then 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, then the execution backtracks to the most recent successful match in an attempt to find an alternative match. If such a match is found, then 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.

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, then 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 predicates 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. Please note that a stretch of unifications is treated as atomic with respect to unblocking goals. Also, if such a stretch is followed by an explicit failure (fail/0, false/0), any unblocked goal is not run.