Logic programming: Prolog, unification and resolution

Logic programming writes a program with logical propositions: you say what is true, and the system tries to prove the asked question from these propositions. That is why it is a declarative approach: you describe what the result is, not how to compute it. The language of this course is Prolog (1972, Colmerauer and Roussel). What comes up on exams: a database and rules are given, and you are asked to write all the answers to a query in order and to find the results of unifications.

Golden rules:

1. Clauses are tried from top to bottom, subgoals from left to right.
2. On failure, go back to the most recent choice point (backtracking).
3. What starts with a capital letter is a variable, what starts with a lowercase letter is an atom.
4. is computes, = only unifies.
5. Cut prevents other clauses from being tried.

From logic to Prolog

A proposition is a logical statement that can be true or false. Predicate calculus writes propositions with compound terms: parent(ayse, can), a functor (parent) and arguments. For propositions with variables there are quantifiers: $\forall X$ (for every X), $\exists X$ (there exists an X).

For automatic proof, propositions are converted to a standard form: clausal form. Prolog uses a restricted version of this too: the Horn clause. A Horn clause has at most one term on its left side (the conclusion part):

$\text{grandparent}(X, Z) \leftarrow \text{parent}(X, Y) \wedge \text{parent}(Y, Z)$

Reading: “If parent(X, Y) and parent(Y, Z) are true, then grandparent(X, Z) is true.” Horn clauses with a non-empty left side are Prolog’s facts and rules.

Prolog’s three constructs

% fact: unconditionally true
parent(ayse, can).
parent(ayse, deniz).
parent(mehmet, can).
parent(can, elif).
parent(deniz, kerem).
parent(deniz, lale).
male(mehmet). male(can). male(kerem).

% rule: head :- body.   comma = AND
father(X, Y) :- parent(X, Y), male(X).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

?- parent(X, can).           % query (goal)
X = ayse ;
X = mehmet.

A variable “taking a value” is not an assignment; instantiation is temporary during a search for a proof and is undone on backtracking. Variables with the same name inside a clause refer to the same thing; those in different clauses are independent.

Unification

The process of finding the variable bindings that make two terms the same. Rules:

• An atom or a number matches only itself.
• An unbound variable matches any term and is bound to it.
• Two structures match if their functors and number of arguments are the same and their arguments match in order.

?- f(X, b) = f(a, Y).          X = a, Y = b
?- f(X, X) = f(a, b).          false          (X cannot be both a and b)
?- g(X, h(Y)) = g(k, h(X)).    X = k, Y = k
?- [H|T] = [1, 2, 3].          H = 1, T = [2,3]
?- [A, B|C] = [x, y, z, w].    A = x, B = y, C = [z,w]

Resolution and search order

Resolution means proving a goal by finding a clause that unifies with that goal and taking the clause’s body as new goals. When the goal list is empty, the proof is complete. Prolog does backward chaining: it starts at the goal and goes backward toward the facts (starting from the facts and deriving new facts is forward chaining; if the goals are few and the facts are many, backward is more efficient).

Prolog’s decisions:

• Depth-first: it does not move on to the next subgoal before finishing the proof of one. Cheap in terms of memory.
• Clause order: in the order written in the database, from top to bottom.
• Subgoal order: from left to right.
• Backtracking: when a subgoal fails, it returns to the subgoal where the last choice was made and tries its next alternative.

Trace: ?- grandparent(ayse, G).

grandparent(ayse, G) :- parent(ayse, Y), parent(Y, G).

parent(ayse, Y)   1st solution Y = can
  parent(can, G)  G = elif               → ANSWER 1: G = elif
  no other parent(can, _) → backtrack
parent(ayse, Y)   2nd solution Y = deniz
  parent(deniz, G)  G = kerem            → ANSWER 2
                    G = lale             → ANSWER 3
parent(ayse, Y)   no other solution → done

?- grandparent(ayse, G).
G = elif ; G = kerem ; G = lale.
?- father(F, can).
F = mehmet.

For father(F, can): first parent(F, can) → F = ayse; male(ayse) fails → backtrack; F = mehmet, male(mehmet) ✔.

The sibling rule and \=

sibling(X, Y) :- parent(P, X), parent(P, Y), X \= Y.

?- sibling(can, S).
S = deniz.
?- sibling(kerem, S).
S = lale.

Without \= everyone would also come out as their own sibling.

Arithmetic

?- X is 2 + 3 * 4.          X = 14
?- X = 2 + 3.               X = 2+3        (a structure term, not computed)
?- X = 2 + 3, Y is X * 2.   X = 2+3, Y = 10
?- X is Y + 1.              instantiation error
?- 6 =:= 2 * 3.             true           (=:= computes both sides and compares)

is evaluates the right side and unifies it with the left side. All variables on the right must be bound beforehand. That is why the order of subgoals matters in rules containing arithmetic:

len([], 0).
len([_|T], N) :- len(T, N1), N is N1 + 1.

fact(0, 1).
fact(N, F) :- N > 0, N1 is N - 1, fact(N1, F1), F is N * F1.

speed(ford, 100).  time(ford, 2).
distance(C, D) :- speed(C, S), time(C, T), D is S * T.

?- len([a, b, c], N).      N = 3
?- fact(4, F).             F = 24
?- distance(ford, D).      D = 200

Lists

The notation [a, b, c] and [H|T]. Classic relations:

member(X, [X|_]).
member(X, [_|T]) :- member(X, T).

append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

?- member(X, [p, q]).          X = p ; X = q
?- append([1], [2, 3], L).     L = [1,2,3]
?- append(X, Y, [1, 2]).       X = [], Y = [1,2] ;
                               X = [1], Y = [2] ;
                               X = [1,2], Y = []

Predicates are relations, not functions: the same append joins, splits, looks for a prefix or a suffix. The query determines which argument is input and which is output.

Cut and negation

The cut (!) is a goal that always succeeds; but backtracking cannot pass back through it. The moment it is passed, the choices made for this predicate (both the earlier subgoals and the remaining clauses) are frozen.

max(X, Y, X) :- X >= Y, !.
max(_, Y, Y).

maxbad(X, Y, X) :- X >= Y.
maxbad(_, Y, Y).

?- max(7, 3, M).       M = 7.
?- maxbad(7, 3, M).    M = 7 ; M = 3.     (the second answer is wrong)

The cut gains efficiency but ties the meaning of the program to the clause order; it moves away from pure logic.

Negation as failure: \+ G succeeds if G cannot be proved. This relies on Prolog’s closed-world assumption: everything that cannot be proved from the database is false.

?- \+ parent(elif, _).    true      (elif's child is not recorded)
?- \+ parent(can, _).     false

It is not the same as logical “not”: \+ does not bind a variable and there is no “unknown” state.

Prolog’s shortcomings

bad_anc(X, Y) :- bad_anc(Z, Y), parent(X, Z).   % left recursion, first
bad_anc(X, Y) :- parent(X, Y).

ancestor(X, Y) :- parent(X, Y).                 % base first
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

?- bad_anc(ayse, elif).    infinite recursion (the stack overflows)
?- ancestor(ayse, D).      D = can ; D = deniz ; D = elif ; D = kerem ; D = lale

Application areas: relational database queries, expert systems, natural language processing, proof systems.

Common mistakes

parent(ayse, can).
parent(ayse, deniz).
parent(mehmet, can).
parent(can, elif).
parent(deniz, kerem).
parent(deniz, lale).

grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

sibling(X, Y) :- parent(P, X), parent(P, Y), X \= Y.

append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

len([], 0).
len([_|T], N) :- len(T, N1), N is N1 + 1.

fact(0, 1).
fact(N, F) :- N > 0, N1 is N - 1, fact(N1, F1), F is N * F1.

max(X, Y, X) :- X >= Y, !.
max(_, Y, Y).
maxbad(X, Y, X) :- X >= Y.
maxbad(_, Y, Y).

bad_anc(X, Y) :- bad_anc(Z, Y), parent(X, Z).
bad_anc(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).