Short notes on Prolog

The following notes aim just at giving a rough (and somewhat not formal) idea of how and why the programming language Prolog works.

Prolog is a programming language based on a fragment of first-order predicate logic.

Formulas of first-order logic are formed using basic predicates (and terms), logical connectives and quantifiers.
A basic predicate is used to represent a basic statement about individual elements of the domain we are taking into account. The elements of the domain are denoted by terms.
For instance: even(2), divisible(15,3), greaterThan(5*7,1+1) etc. .
In Prolog, basic predicates are denoted by identifiers beginning with lower case letters. Terms denoting elements of the domain are formed using variables, constants and function symbols.
In Prolog, variables are represended by identifiers beginning with a upper-case letter, whereas constants and function symbols are represented by identifiers starting with lower-case letters. The following is a possible term in Prolog notation: f(Y,g(X,c)). An example of basic statement formed using the basic binary predicate pred(_,_) and the terms f(Y,g,(X,c)) and Z is pred(f(Y,g,(X,c)),Z) (basic statements are also called atomic formulas).
In first-order logic more complex formulas can be defined by means of Logical Connectives: And ( ∧ ), Or ( ∨ ), Implies (→) etc.

In the following a generic formula will be denoted by A,B, etc. We write A(X) to represent that the formula A contains a predicate which uses a variable X.

In first-order logic, formulas can be universally or existentially quantified:

• the formula ∀X.A(X) means that the formula A(X) is valid for any possible element X of the domain:
• the formula ∃X.A(X) means that there exists an element t of the domain such that A(t) is valid.

The quantifiers are binders for the quantified variables, like the 'λ' for λ-terms. So quantified formulas have to be considered modulo α-conversion (∀X.A(X) is the very same formula as ∀Y.A(Y)).

Given a formula A it is not possible, in general, to decide whether there is a proof for A (i.e. A is derivable) in first-order logic. In other words, there is no algorithm whatsoever which, given a formula A, terminates telling us if A is derivable or not (or, equivalently, if A is valid or not).

The following are some of the rules of first-order logic that can be used to prove formulas:

Modus Ponens:

∀-Elimination: ∃-Introduction: ∧-Introduction :

Even if first-order logic is undecidable, there are however fragments of it that are decidable. Other ones, even if not decidable, allow for semi-decision algorithms that are extremely efficient. One of these is the fragment where we consider only formulas with the following shape

or with the shape
where

• A₁, A₂,..., A_n, B, C are atomic formulas;
• the variables occurring in B have to be considered universally quantified in
  (A₁ ∧ A₂ ∧ .... ∧ A_n) → B and in B;
• the variables occurring in A₁, A₂,..., A_n but not in B have to be considered existentially quantified in (A₁ ∧ A₂ ∧ .... ∧ A_n).
• the variables occurring in C have to be considered universally quantified;

Formulas of these forms are called Horn Clauses.
Notice that instead of considering the above quantifications, we can consider all the variables in C and (A₁ ∧ A₂ ∧ .... ∧ A_n) → B to be universally quantified
(since in first order logic, when Y is not a free variable in Q, ∀X.( (∃Y.P)→Q ) is logically equivalent to ∀X,Y.( P→Q) ).

In Prolog, a formula (A₁ ∧ A₂ ∧ .... ∧ A_n) → B is represented as

B :- A1, A2,..., An

An example of Horn Clause in Prolog is

c(X,f(Y)) :- a(X,Y), b(g(Z),s), d(Z,Z).

(Horn Clauses in Prolog always terminate with a dot '.')

In the above formula all the variables are considered to be quantified as explained before. So the corresponding formula in logic notation would be

If one takes a set of Horn clauses H₁,..,H_n, and a formula of the form

where B is an atomic formula there exists an algorithm which, in case this formula is derivable from the hypotheses H₁,..,H_n, finds a proof for it in an efficient way (such algorithm is called Resolution Algorithm).

Even more, it can find out all the possible proofs if there is more than one.

In Prolog the formula ∃X₁,..,X_k.B is represented simply by B and it is usually written after the prompt of the interpreter '?-', as follows

?- B.

B is called Goal.

Let us see, through an example, how Prolog looks for a proof of a Goal.

The following is a program (a set of Horn Clauses) intended to produce, by means of Prolog proof search, all the possible permutations of a given list.
The predicate permutation/2 is introduced with the intended meaning that it holds whenever the second argument is a permutation of the first one (the part "/2" in "permutation/2" is used to point out that permutation is a predicate with two arguments.)

permutation([], []).                                          (1)

permutation(List, [Element | Permutation]) :-                 (2)

                                 select(Element, List, Rest),

                                 permutation(Rest, Permutation).

The program works correctly thanks to the predefined Prolog predicate select/3.

The predicate select/3 holds whenever the first argument is an element of the second argument (that has to be a list) and the third argument is the list without the element.

In fact, if we give the goal select(E,[1,2,3],R) to the Prolog interpreter, we are asking whether there exists an element E and a list R such that select(E,[1,2,3],R) holds.
The interpreter will tell us that there are many possibilities to prove such a statement, and for each of these possibilities it returns us the different E and R used in the different proofs. In particular, the interpreter returns us

E = 1,
R = [2, 3] ;
E = 2,
R = [1, 3] ;
E = 3,
R = [1, 2] ;

Let us see now, roughly, how the interpreter works when we give to it the following goal:

?- permutation([a,b],P).     (G)

By writing that we are asking the interpreter whether it is possible to prove that there exists a list P such that ∃P.permutation([a,b],P) is derivable from the clauses (1) and (2) that forms our program.

The interpreter first tries to use clause (1) to prove the goal (G). It is not possible, so it tries and use clause (2). Remember that in Prolog clauses, the variables (present in the left-hand side) are assumed to be universally quantified.
If one assumes ∀X.A(X) then, by using the logical rule ∀-Elimination, we can derive, for any possible term t, that A(t) holds.
So, we could get a proof of (G) from clause (2) if we managed to unify the goal (G) with the head of clause (2) and then if we can prove all the resulting subgoals. The proof of (G) would then be obtained using the rule Modus Ponens.
(Notice that we need to unify the goal with the head of the clause since we do not simply want to find a proof of the goal, but also to get the term witnessing the goal.)

permutation([a,b],P) and permutation(L1, [E1 | P1]) are unifiable by means of the following substitution

L1 = [a,b]
P  = [E1 | P1]

(we used L1, E1 and P1 since Element and Permutation are actually bound variables and we can rename them).

We need then to prove the conjunction of the following subgoals:

The subgoal sG1, that amounts to asking whether there exist E1 and R1 such that select(E1, [a,b], R1) holds, can be proved directly by the interpreter since select/3 is a predefined predicate.
In fact a proof of ∃E1,R1.select(E1, [a,b], R1) is obtained using rule ∃-Introduction, since the interpreter knows that select(a, [a,b], [b]) holds.

The interpreter now remembers that the elements E1 and R1 such that select(E1, [a,b], R1) holds are the following ones

E1 = a
R1 = [b]

Now, since we have to prove the conjunction of sG1 and sG2
(namely ∃E1,R1,P1.(select(E1, [a,b], R1) ∧ permutation(R1, P1)) ) and we have proved the subgoal

?- select(E1, [a,b], R1)

using [b] for R1, we are necessarily forced to prove also sG2 using this particular value for R1, that is we have to prove ∃P1.permutation([b], P1).

The interpreter now proceeds as it did previously: tries to use clause (1), but it does not succeeds, and hence tries clauses (2).
Clauses (2) can be used to try and prove ∃P1.permutation([b], P1) if it is possible to unify permutation([b], P1) with permutation(L2, [E2 | P2]) (again, we renamed bound variables, and we used different names in order to avoid confusion).

The unification is possible by means of the following substitution

L2 = [b]
P1 = [E2 | P2]

The conjuction of the following subgoals has now to be proved

The existence of E2 and R2 such that select(E2, [b], R2) holds can be proved by the interpreter using

E2 = b
R2 = []

We are left then to prove ∃P2.permutation([], P2), i.e. we need to prove that there exists a list P2 such that permutation([], P2) holds.
This can be done immediately, since clause (1) states that permutation([],[]) holds, and hence our subgoal ∃P2.permutation([], P2) can be proved using clause (1) and the rule ∃-Introduction.

The interpreter remembers that the element P2 such that permutation([], P2) holds is the following one

P2 = []

Since there is no other subgoal to be proved, we have a proof of the fact that ∃P.permutation([a,b],P)

Moreover, in such a proof we have used the following substitutions:

L1 = [a,b]
P  = [E1 | P1]
E1 = a
R1 = [b]
L2 = [b]
P1 = [E2 | P2]
E2 = b
R2 = []
P2 = []

This means that an element P for which permutation([a,b],P) holds is

P = [E1|P1] = [a|[E2|P2] = [a|[b|[]]] = [a,b]

The Prolog interpreter (if asked to) can look for ALL the possible proofs of ∃P.permutation([a,b],P).
In order to do so, it can backtrack to sG3, looking for an alternate proof of ∃E2,R2.select(E2, [b], R2) different from the one we have just found.

Now, since there is no other proof of ∃E2,R2.select(E2, [b], R2), there is also no other proof for ∃P1.permutation([b], P1).
Hence the interpreter backtracks to sG1, looking for another proof for ∃E1,R1.select(E1, [a,b], R1) different form the one we already used.

There is such a proof, in particular the proof that uses

E1 = b
R1 = [a]

Using such a different proof of sG1, we can find a different proof of our goal, but in order to obtain that we need a proof of permutation(R1, P1) using [a] as R1.

We have to prove then ∃P1.permutation([a], P1)

The interpreter proceeds as it did before, finding a proof for the conjunction of the following subgoals

and hence for the statement ∃P2.permutation([],P2) using clause (1).

We have then found another proof for our goal, this time using the following substitutions:

L1 = [a,b]
P  = [E1 | P1]
E1 = b
R1 = [a]
L2 = [a]
P1 = [E2 | P2]
E2 = a
R2 = []
P2 = []

This means that another P for which permutation([a,b],P) holds is

P = [E1|P1] = [b|[E2|P2] = [b|[a|[]]] = [b,a]

In order to find such a proof we backtracked to sG1.
Now there is no other possible proof for sG1 and there is no possibility to backtrack anymore. We are done and we have found all the possible permutations (just 2 in such a simple case).

We can give a summary of how Prolog has proceeded as follows:

G    permutation([a,b],P)     
         |                   |--> (First backtrack)
sG1  select(E1, [a,b], R1)   |sG1 select(E1, [a,b], R1) 
     E1 = a                  |    E1 = b       
     R1 = [b]                |    R1 = [a]
         |                   |        |
sG2  permutation([b],P1)     |sG2 permutation([a],P1)   
         |                   |        |
         |                   |        |
         |                   |        |
sG3  select(E2,[b],R2)       |sG5 select(E2,[a],R2)
     E2 = b                  |    E2 = a
     R2 = []                 |    R2 = []
         |                   |        |
sG4  permutation([],P2)      |sG6 permutation([],P2)  
     P2 = []                 |    P2 = []
                             |
     OK-First proof!! -------|    OK-Second proof!!
                                        |  
                                        |---| No other possible backtrack! 

Let us present a different viewpoint for how the interpreter looks for the first proof of our goal:
In the following we use s for select, p for permutation, L for List, R for Rest and P for Permutation.
So, the first clause of the program is
(1): p([],[])
and the second one is
(2): ∀E,L,R,P. s(E,L,R) ∧ p(R,P) → p(L,[E|P]) (as discussed previously, we are considering all the variables in a clause to be universally quantified).

• look for P s.t. p([a,b],P)
• unify p([a,b],P1) p(L1,[E1|P1]) =
  = L1⇒[a,b], P⇒[E|P1]
• look for E1,R1,P1 s.t. s(E,[a,b],R) ∧ p(R1,|P1)
• interpreter knows that s(a,[a,b],[b]),
  so E1⇒a, R1⇒[b]
• look for P1 s.t. p([b],|P1)
• unify p([b],|P1) p(L2,[E2|P2]) =
  = L2⇒[b], P1⇒[E2|P2]
• look for E2,R2,P2 s.t. s(E2,[b],R2) ∧ p(R2,|P2)
• interpreter knows that s(b,[b],[]), so E2⇒b, R2⇒[]
• look for P2 s.t. p([],|P2)
we have the clause p([],[]),
• found! P2⇒[]
• found! E2=b, R2=[], P2=[]
• found! P1=[b|[]]
• found! E1=a,R1=[b],P1=[b|[]]
• found! P=[a,[b|[]]

The formal logical derivation that it is possible to get from what we described above is THIS.

The following is a Prolog program that looks apparently correct but does not work.

The predicate h(_,_) is intended to hold whenever the second argument is the height of the first argument, which is an unlabelled binary tree :

h(emptyBT,0).

h(join(T1,T2),M+1) :- h(T1,N1), h(T2,N2), max(N1,N2,M).


max(N1,N2,N1) :- N1>N2.

max(N1,N2,N2) :- N2>=N1.

If we ask

?- h(join(join(emptyBT,emptyBT),emptyBT),H).

the interpreter returns

H = 0+1+1 ;

We would have expected 2.

This is because M+1 is treated as a normal term, with + considered as an uninterpreted function symbol. If we wish M to be associated to a number, we need to modify the program as follows:

h(emptyBT,0).

h(join(T1,T2),N) :- h(T1,N1), h(T2,N2), max(N1,N2,M), N is M+1.

See [PL] for the meaning of the clause N is M+1.