Alex
Alex

Reputation: 43

How does unification algorithm actually work?

I have this Prolog code:

bar(b).
bar(c).
baz(c).

This query:

bar(X), baz(X).

returns X = c

If I have this program, which is a little bit different:

bar(c).
bar(b).
baz(c).

On the same query

bar(X), baz(X).

why does it return

X = c;
false

Upvotes: 1

Views: 266

Answers (1)

slago
slago

Reputation: 5509

The computation performed by Prolog to answer a query can be represented as a tree. Prolog searches this tree using a depth-first strategy, automatically backtracking when it encounters a failure node (or when the user presses the key ';' to get an alternate answer).

During the search, clauses are used in the order they are declared in the program (from the first to the last).

At the end of the search, Prolog displays false only if the last node visited in the tree is a failure node.

So, to understand why Prolog behaves differently in the two indicated cases, you can compare the search trees that Prolog explores in each of them:

  • First case:

enter image description here

  • Second case:

enter image description here

Upvotes: 4

Related Questions