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 (see "A Machine-Oriented Logic Based on the Resolution Principle" by J.A. Robinson, Journal of the ACM 12:23-44, January 1965) finds the most general common instance of the two terms, which is unique if it exists. If a match is found, 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, 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) 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, 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.