Searching

The query

?- pet(X).

returns the following answers:

X = spot
X = barry

How is this achieved? The CLP system performs a search using all the possibilities offered by having several clauses for the predicates. This is best depicted by a search tree which represents all possible paths in the program. Without entering into details, every time a predicate with more than a clause is called, a choice point is made at that execution point: this choice points keeps information about the state of the execution at that moment, so that, if more solutions are needed, the engine can backtrack up to that point, and resume the search with the next untried clause of that predicate.

  

Figure 2.1: A tree

The search process, automatically triggered by a failure in the resolution, allows logic programming based languages to return all possible solutions to a query: after having reached a solution, if the user requests for more answers, the toplevel just causes a failure and the backtracking process is (re)started^2.1. The order of backtracking is as follows:

• Clauses within a predicate are tried from top to bottom; backtracking on a predicate will cause the next untried clause to be executed. The order in which clauses are executed is defined by the search rule.
• Atoms within a clause body are executed from left to right, and so backtracking is attempted right to left. This is called the selection rule.

Other strategies to select which clause and which atom to try are possible, and those different search and selection rules give raise to different operational semantics for logic languages.

Example 2.8   The following query has been executed using the program in Example 2.6:

?- pet(X), animal(Y).
   X = spot, Y = spot ;
   X = spot, Y = barry ;
   X = spot, Y = hobbes ;
   X = barry, Y = spot ;
   X = barry, Y = barry ;
   X = barry, Y = hobbes

Solutions for the clauses of animal/1 are generated first, in the order in which the clauses are written. After that, a new solution for pet/1 is generated, following the rules for atoms and clauses stated above. $\blacksquare$