| |
What's so special about Prolog?
Prolog (PROgramming in LOGic) is a logic programming language based
on Horn clause resolution theorem proving.
A program in Prolog can be thought of either declaratively or
procedurally:
-
It can be thought of as a declaration, in logic, of certain facts and rules.
-
It can be thought of as a procedure for proving a theorem.
There are many different dialects of Prolog. We use SWI-Prolog from the
University of Amsterdam.
Prolog is usually interpreted, though there are some compilers available.
Like Lisp, it can mix interpreted and compiled code.
Structure of a Prolog "program"
A Prolog "program" is constructed of facts and rules that are stored
in a database. A "program" is "executed" by posing a query to the database.
The Prolog interpreter then tries to prove the query using the facts
and the rules in the database.
Facts are facts about objects in the domain of interest. Rules allow
you to express relationships between facts.
A Prolog database might look something like the following:
likes(fred, mary).
likes(mary, chicken).
likes(fred, X) :- likes(mary, X).
This database is composed of two facts and a single rule. The facts state
that Fred likes Mary and that Mary likes chicken. The rule is used to express
the relationship that Fred likes something if Mary likes it.
There are two kinds of entities in this example:
-
atoms must begin with a lower case letter. They represent specific
objects in the world.
-
variables must begin with an upper case letter. They can stand for
many things.
Rules
In general, a rule will look something like:
goal(V1, . . . , Vn)
:-
requirement1(. . . ),
requirement2(. . . ),
. . .,
requirementm(. . . ).
which means that the relationship goal
holds whenever requirement1, ..., requirementm
all hold. That is to say, goal is true
if requirement1, ..., requirementm
are true.
Functors in Prolog
Arguments to propositions in Prolog don't have to be atoms. They can
be any functor structure. Example:
loves(motherof(X), daughterof(X)) :-
wellbred(X), wellbred(daughterof(X)).
wellbred(X) :- polite(X).
wellbred(jane).
polite(daughterof(jane)).
| ?- loves(motherof(X), daughterof(X)).
X = jane ;
no
| ?- loves(X, Y).
X = motherof(jane)
Y = daughterof(jane) ;
no
| ?- loves(motherof(X), Y).
X = jane
Y = daughterof(jane) ;
no
We can use logic to represent data structures. We can think of any functor
as a tree, with function name as root, arguments as subtrees.
eats(fred, chicken).
loves(daughterof(mary, bill),
sonof(jane, sonof(ellen, james))).
| loves |
| |
| daughterof |
sonof |
| |
| mary |
|
bill |
jane |
sonof |
| |
| |
ellen |
|
james |
If we can represent trees in Horn clause logic, then we can create other
data structures by modeling them as trees.
Lists in Prolog
In Prolog, the empty list is represented by [].
The functor that two entities are related by being in a list is the dot.
This is called dot notation for lists. In Prolog implementations, the dot
is the period character.
Example: The list containing a, b, c
would be represented as
.(a, .(b, .(c, [])))
Fortunately, Prolog has a simpler method of writing lists:
[a, b, c]
Commas separate list items.
Prolog also has a way of splitting lists into the first element and
the rest of the list (like car and cdr in Lisp). The vertical bar indicates
that the next item is the rest of the list.
So the above list could be written as [a, b,
c] or [a | [b, c]], or even [a
| [ b | [c | []]]].
This form is converted into the l form
when read in by Prolog.
| ?- [user].
| good([a, b, c]).
| user consulted 104 bytes 0.0333338 sec.
yes
| ?- good(X).
X = [a,b,c] ;
no
| ?- good(.(a, .(b, .(c, [])))).
yes
| ?- good([a | [b, c]]).
yes
| ?- good([X, Y, Z]).
X = a
Y = b
Z = c ;
no
| ?- good([X | Y]).
X = a
Y = [b,c] ;
no
Unification
The heart of Prolog is unification. Unification is a way to match
Prolog structures that may contain variables. By structure we mean just
about anything, lists, trees, graphs, etc. The rules for unification
are relatively simple:
-
A constant matches itself. (If it is a functor, the arities must match
too.)
-
A variable matches any single thing --- either a constant or an arbitrarily
complex term.
-
A variable also matches another variable (or itself), or a term containing
variables. (This is a special case of rule 2.)
Examples of unification
(b,c) unifies with (b,c),
with variable bindings {}. (Anything unifies with itself.)
(b,c) unifies with (X,c),
with variable bindings {X=b}.
(b,c) does not unify with (X,X),
because X cannot be bound to both b and c at the same time.
However, (b,b) unifies with (X,X),
with variable bindings {X=b}.
(b,Y) unifies with (X,c),
with variable bindings {X=b, Y=c} (Variables
may be in either or both structures.)
(b,Y) unifies with (X,Z),
with
variable bindings {X=b, Y=Z} (Variables
may unify with other variables.)
(b(c),d) unifies with (X,Y)
with
variable bindings {X=b(c), Y=d}. (A variable
may unify with a structure.)
(b,c) does not unify with (b,c,d),
and
X(Y,Z) does not unify with
X(Y,Z,W). (Functors must have the same arity to match.)
(b(U),d) unifies with (X,Y)
with
variable bindings {X=b(U), Y=d, U=_G323}
(A
variable may unify with a structure that contains another variable. A variable
may receive no fixed binding --- if any value for it is okay.)
(b(X),d) unifies with (X,Y)
with variable bindings {X=b(X), Y=d} (A
variable may unify with a structure that contains the same variable ---
even though this leads to a recursive value for it.)
How a query is handled
A Prolog query is handled (generally speaking) in the following way:
-
Find the first rule in the database whose left hand side unifies
with the query. This step may produce some variable bindings. At this point
there may be more than one choice for the rule to use. The first option
is selected, but the other choices from this choice point are stored.
-
If the rule has no right hand side, then we have proved the query. The
list of bindings is returned to the user.
-
If the rule has a right hand side, then try to prove each of the elements
of the right hand side, using the variable bindings that were generated
in step 1.
-
If all of the elements of the right hand side succeed, then this rule succeeds,
return the list of bindings to the user.
-
If all of the elements of the right hand side do not succeed, then
backtrack to the last choice point (possibly undoing some variable bindings),
and try another option.
When the list of bindings (which is really an answer to the query) is displayed
for the user, he or she has the option of asking for more answers. In this
case, the program will backtrack to the last choice point and continue
searching for answers.
We'll do an example! Suppose you pose the following query:
employs(cleverCompany,Person).
This query works out to mean "who works for cleverCompany?" Your Prolog
database (or program, whichever way you look at it)) looks like:
1. smart(david).
2. employs(cleverCompany, donna).
3. employs(X, Y) :- worksFor(Y, X).
4. employs(X, Y) :- smart(Y), diligent(Y).
5. worksFor(johann, cleverCompany).
6. diligent(susan).
Note that the numbers have been used for ease of reference!
-
The first rule that matches the query is 2, with the binding {S=donna}.
There is no left-hand side, so the query succeeds and the bindings are
returned to the user. This is the first answer.
-
The user asks for more answers, so we backtrack to the last choice point,
which was when rule 2 was selected. We look for another rule that matches
the query and come to rule 3. We unify the query and the left hand side
of rule 3, getting the bindings {X=cleverCompany,Y=Person}.
-
There is a right hand side for this rule, so we need to prove the query
worksFor(Y,cleverCompany).
-
We look for the first rule whose left-hand side unifies with the query.
There is only one such rule, number 5. This produces the binding
{Y=johann},
and the query succeeds.
-
All of the elements of the right hand side of rule 3 have been proved,
so this rule succeeds with the bindings {X=cleverCompany,Person=johann},
which are returned to the user.
-
The user asks for more answers, so we backtrack to the last choice point,
which was our selection for a way to prove the query worksFor(Y,cleverCompany).
There are no other ways to prove this, so we backtrack to the previous
choice point - our attempt to find a rule to match the original query.
There is such a rule, namely number 4. The query and the left hand side
of 4 are unified, giving the bindings {X=cleverCompany,Person=Y}.
-
Rule 4 also has a right hand side, so we try to prove the queries smart(Y),
diligent(Y).
-
We look for the first rule whose left-hand side unifies with the query.
Rule 1 gives us a binding for {Y=david},
because
David is smart, but we have no rule that lets us match diligent(david).
The query fails to find a match.
-
The user asks for more answers, so we backtrack to the last choice point,
which was our selection for a way to prove the query employs(cleverCompany,
Y). There are no other ways to prove this, so the query fails,
and no more bindings are returned to the user.
|