Logic programming is a model of computation that applies mathematical logic to problem solving.
Logic programming is declarative, not procedural. In the procedural programming paradigm, the programmer specifies data and the algorithms that should be executed on those data to reach a solution. In the logic programming paradigm, the programmer specifies relationships that hold between the data in the form of facts and rules. The programmer then specifies a goal, and the computer works out the implementation details of achieving that goal.
A relation specifies a relationship that holds between some objects. We denote
relations with the form pred(obj1, obj2, ...)
, where the name of the relation
is called the predicate.
To store relations in our system for use in proving goals, we use clauses. A clause consists of a head relation and some body relations. For example, in the clause
compatible(John, June) :- common_interests(John, June), lazy(June)
we are specifying that John and June are compatible if they have common
interests and June is lazy. The head of this clause is compatible(John, June)
and the body consists of the two relations common_interests(John, June)
and
lazy(June)
. We call clauses of this form rules, since they specify when a
relation is true. To specify a relation that is unconditionally true, we use a
clause with no body, called a fact: girl(June)
.
We can use logic variables to describe more abstract relations. Consider the following clauses:
female(June)
likes(June, running)
likes(John, running)
similar_hobbies(?x, ?y) :- likes(?x, ?z), likes(?y, ?z)
compatible(John, ?x) :- female(?x), similar_hobbies(John, ?x)
The last two rules use logic variables. The second-to-last rule specifies when two people have similar hobbies (that is, there is something they both like), and the last rule specifies the people with whom John is compatible.
Once we have some clauses, we can specify a goal, and the system will attempt to satisfy that goal. In logic programming parlance, we call this proving a goal. The goal is stated in the form of a relation.
Sometimes our goal requires a yes or no answer. The system will use the
existing clauses to determine whether the given goal can be satisfied. For
example, using the five clauses defined above, we might specify the goal
compatible(John, June)
. If we try to prove this goal, the result will simply
be "Yes." If we try to prove the goal male(June)
, the result will be "No.",
as the system is unable to prove that June is male from the specified clauses.
We can specify much more interesting goals. For instance, we might specify the
goal likes(?x, running)
. Here, we are interested in determining who is
interested in running. If we attempt to prove this goal, the system will
determine if it can be satisfied, and if so, what values of ?x
satisfy the
goal. Here, the results will be John and June, since we declared that both of
them like running. These results that, when substituted for the variables,
satisfy the goal are called the bindings of those variables.
For more examples, see the following databases of clauses:
These databases can be loaded into the provided Prolog interpreter for experimentation.
Programming in this model requires some adjustment coming from a procedural programming background; logic programming appears very mysterious at first. The implementation, however, is simple, and relies on three basic concepts:
We will see how these three concepts are implemented below.
This module provides a library that enables the use of logic programming in arbitrary Python programs. For some examples of this, see the following:
Written by Daniel Connelly. This implementation is inspired by chapter 11 of "Paradigms of Artificial Intelligence Programming" by Peter Norvig.
First, we define the types of data represented in our system. These include:
We want each instance of these types to support a few common operations that will be used throughout the system.
get_vars
: list all of the variables contained in this instance. For
example, if we call get_vars
on the relation member(?x, pair(y, ?z))
,
we should get back the list [?x, ?z]
.rename_vars
: replace variables in this instance using a dictionary that
maps old variables to replacement variables.Represents any literal (symbol, number, string, etc).
class Atom(object):
def __init__(self, atom):
self.atom = atom
def __repr__(self):
return str(self.atom)
def __eq__(self, other):
return isinstance(other, Atom) and other.atom == self.atom
These don't need to do anything for Atoms, since they don't contain Vars.
def rename_vars(self, replacements): return self
def get_vars(self): return []
Represents a logic variable.
class Var(object):
counter = 0 # for generating unused variables
Get a new, unused Var.
@staticmethod
def get_unused_var():
While proving goals we will sometimes want to create unused, temporary variables, so we do so by keeping a count of how many have been created and use it to name new ones.
v = Var('var%d' % Var.counter)
Var.counter += 1
return v
def __init__(self, var):
self.var = var
def __repr__(self):
return '?%s' % str(self.var)
def __eq__(self, other):
return isinstance(other, Var) and other.var == self.var
def __hash__(self):
return hash(self.var)
As mentioned above in the section on "Goals", variables will be bound to other values. These bindings will be tracked through dictionaries.
Find the term that self is bound to in bindings.
Tries to find a non-Var binding to return by searching transitively through the bindings dictionary.
def lookup(self, bindings):
binding = bindings.get(self)
While looking up the binding for self, we must detect:
encountered = [self, binding]
while (isinstance(binding, Var)
and binding in bindings
and bindings[binding] not in encountered):
binding = bindings.get(binding)
encountered.append(binding)
If the next binding leads to a relation, expand it.
if isinstance(binding, Relation):
return binding.bind_vars(bindings)
return binding
Rename self with its value in replacements if it appears as a key.
def rename_vars(self, replacements):
return replacements.get(self, self)
Return a list containing this var.
def get_vars(self):
return [self]
A relationship (specified by a predicate) that holds between terms.
class Relation(object):
def __init__(self, pred, args):
self.pred = pred
self.args = args
def __repr__(self):
return '%s(%s)' % (self.pred, ', '.join(map(str, self.args)))
def __eq__(self, other):
return (isinstance(other, Relation)
and self.pred == other.pred
and list(self.args) == list(other.args))
Replace each Var in this relation with its bound term.
def bind_vars(self, bindings):
bound = []
for arg in self.args:
bound.append(arg.lookup(bindings) if arg in bindings else arg)
return Relation(self.pred, bound)
Recursively rename each Var in this relation.
def rename_vars(self, replacements):
renamed = []
for arg in self.args:
renamed.append(arg.rename_vars(replacements))
return Relation(self.pred, renamed)
Return all Vars in this relation.
def get_vars(self):
vars = []
for arg in self.args:
vars.extend(v for v in arg.get_vars() if v not in vars)
return vars
A clause with a head relation and some body relations.
class Clause(object):
def __init__(self, head, body=None):
self.head = head
self.body = body or []
def __repr__(self):
if self.body:
return '%s :- %s' % (self.head, ', '.join(map(str, self.body)))
return str(self.head)
def __eq__(self, other):
return (isinstance(other, Clause)
and self.head == other.head
and list(self.body) == list(other.body))
Replace all Vars in this clause with their bound values.
def bind_vars(self, bindings):
head = self.head.bind_vars(bindings)
body = [r.bind_vars(bindings) for r in self.body]
return Clause(head, body)
Recursively rename each Var in this Clause.
def rename_vars(self, replacements):
renamed_head = self.head.rename_vars(replacements)
renamed_body = []
for term in self.body:
renamed_body.append(term.rename_vars(replacements))
return Clause(renamed_head, renamed_body)
Replace each var in self with an unused one.
def recursive_rename(self):
renames = {v: Var.get_unused_var() for v in self.get_vars()}
logging.debug('Renamed vars: %s' % renames)
return self.rename_vars(renames)
Return a list of all Vars in this Clause.
def get_vars(self):
vars = self.head.get_vars()
for rel in self.body:
vars.extend(v for v in rel.get_vars() if v not in vars)
return vars
The first important idea in our implementation of a logic programming system is that of a uniform database. We store all facts and rules in a single data structure, organized so that we can quickly retrieve all the clauses that might help prove a goal. Since our goals are relations, while proving a goal we will want to retrieve clauses whose head relations match the goal relation. Thus we will index the database on the predicates of the contained clauses' heads.
The implementation of the database is a single Python dictionary. Keys are the predicates of relations, and values are lists of clauses with identical head predicates.
Store the clause in the database, indexed on the head's predicate.
def store(db, clause):
db.setdefault(clause.head.pred, []).append(clause)
Retrieve all clauses with matching head's predicate.
def retrieve(db, pred):
return db.setdefault(pred, [])
It will be useful to store Python functions in the database so that we can induce side-effects by proving "relations".
Store a Python function in the database with the given name.
def define_procedure(db, name, proc):
db[name] = proc
The second important concept in our system is unification. Unification is a process that determines when two objects are equivalent, either by determining that they are exactly equal or by finding bindings for the undetermined variables in the objects such that the resulting objects, with their variables replaced by the bindings, can be considered equaivalent.
A few small examples:
Unification of likes(Sarah, Joe)
and likes(?y, Joe)
will succeed if
either
Unification of ?y
and ?z
will succeed if
Unfication of likes(Sarah, Joe)
and ?x
will succeed only if ?x is
already bound to likes(Sarah, Joe)
or is unbound.
Unification of likes(Sarah, Joe)
and Bob
will always fail--these are not
equal, and no bindings of variables will result in equivalence.
Unification of likes(Sarah, Joe)
and hates(Sarah, Joe)
will always fail;
these relations have different predicates, and so they can never be
considered equivalent.
Unification is very similar to pattern-matching; in fact, the algorithms for pattern matching and unification in Peter Norvig's PAIP are nearly identical, a testament to the utility of Lisp's uniform syntax.
Unify x and y, if possible. Returns updated bindings or None.
def unify(x, y, bindings):
logging.debug('Unify %s and %s (bindings=%s)' % (x, y, bindings))
False bindings means we failed in a previous step. Re-fail.
if bindings == False:
return False
Make a copy of bindings so we can backtrack if necessary.
bindings = dict(bindings)
When x and y are equal (the same Var or Atom), there's nothing to do.
if x == y:
return bindings
if isinstance(x, Var):
If x (or y) is already bound to something, dereference and try again.
if x in bindings:
return unify(bindings[x], y, bindings)
if y in bindings:
return unify(x, bindings[y], bindings)
Otherwise, bind x to y.
bindings[x] = y
return bindings
if isinstance(y, Var):
return unify(y, x, bindings)
if isinstance(x, Relation) and isinstance(y, Relation):
Two relations must have the same predicate and arity to unify.
if x.pred != y.pred:
return False
if len(x.args) != len(y.args):
return False
Unify corresponding terms in the relations.
for i, xi in enumerate(x.args):
yi = y.args[i]
bindings = unify(xi, yi, bindings)
if bindings == False:
return False
return bindings
if isinstance(x, Clause) and isinstance(y, Clause):
Clause bodies must have the same length to unify.
if len(x.body) != len(y.body):
return False
Unify head term and body terms.
bindings = unify(x.head, y.head, bindings)
if bindings == False:
return False
for i, xi in enumerate(x.body):
yi = y.body[i]
bindings = unify(xi, yi, bindings)
if bindings == False:
return False
return bindings
return False
As mentioned previously, "proving" a goal will determine whether we can satisfy a goal relation using the clauses in our database. If so, we want to see the variable bindings that satisfy the goal (if the goal involves any variables).
Given a goal relation, our general algorithm for proving a goal is as follows:
Retrieve all clauses from the database whose head relations have the same predicate as the goal relation. Each such clause might help us to prove the goal relation--we just need to ensure that the head relation matches the goal relation.
For example, if we want to prove likes(You, Me)
, we will retrieve all
clauses from the database whose head's predicate is likes
:
likes(Bob, Sue)
likes(You, ?x) :- likes(?x, StirFry), likes(?x, Swimming)
likes(Sue, ?x) :- hates(?x, Everything)
likes(?x, Me) :- likes(?x, Programmers)
For each retrieved clause, try to unify the head with the goal. If they unify, then we can prove the goal by proving the body of the retrieved clause.
In the retrieved clauses from #1, only the clauses
likes(You, ?x) :- likes(?x, StirFry), likes(?x, Swimming)
likes(?x, Me) :- likes(?x, Programmers)
have a head relation that unifies successfully with likes(You, Me)
,
with bindings of ?x
-> Me
for the first clause and ?x
-> You
for
the second clause.
For each clause whose head unifies with the goal, recurse to prove each body relation of the clause. If proving fails for any body relation, we move on to the next retrieved candidate clause.
So, continuing our example, if we can prove that likes(Me, StirFry)
and
likes(Me, Swimming)
, then we will have proved likes(You, Me)
. If we
fail to prove either of these, we will move on to the next retrieved
clause, and try to prove likes(?x, Programmers)
.
We will keep track of the goals we're proving with a stack, implemented as a Python list. In this way we can keep track of all the goals we must prove even when we recurse while proving.
Prove goal and all remaining goals using the given bindings and database.
If successful, returns the extended bindings that satisfy all the goals. Otherwise, returns False.
def prove(goal, bindings, db, remaining=None):
False bindings means we failed somewhere earlier, so re-fail.
if bindings == False:
return False
logging.debug('Prove %s (bindings=%s)' % (goal, bindings))
remaining = remaining or []
Find the clauses in the database that might help us prove goal.
query = db.get(goal.pred)
if not query:
return False
if not isinstance(query, list):
If the retrieved data from the database isn't a list of clauses, it must be a Python function--call it and return the results.
return query(goal.args, bindings, db, remaining)
logging.debug('Candidate clauses: %s' % query)
Try to use the retrieved clauses to prove the goal.
for clause in query:
logging.debug('Trying candidate clause %s for goal %s' % (clause, goal))
First, rename the variables in clause so they don't collide with those in goal.
renamed = clause.recursive_rename()
Next, we try to unify goal with the head of the candidate clause. If unification is possible, then the candidate clause might either be a rule that can prove goal or a fact that states goal is already true.
unified = unify(goal, renamed.head, bindings)
if unified == False:
continue
Make sure the candidate clause doesn't lead to an infinite loop by checking to see if its head is in its body.
renamed = renamed.bind_vars(unified)
if renamed.head in renamed.body:
continue
We need to prove the subgoals of the candidate clause before using it to prove goal. Then prove the remaining goals as well.
extended = prove_all(renamed.body + remaining, unified, db)
If we can't prove all the subgoals, or the bindings that result from proving the subgoals make it so that the remaining goals can't be proved, move on.
if extended == False:
continue
Otherwise return the bindings that satisfied the goals.
return extended
logging.debug('Failed to prove %s' % goal)
return False
Prove all the goals with the given bindings and rule database.
def prove_all(goals, bindings, db):
if bindings == False:
return False
if not goals:
return bindings
logging.debug('Proving goals: %s (bindings=%s)' % (goals, bindings))
return prove(goals[0], bindings, db, goals[1:])
There may be more than one set of bindings that satisfy a goal, and the user may not be interested in the first solution we find. The number of solutions is potentially unbounded, so we need some way to find solutions incrementally.
The third important idea in our system is automatic backtracking, and is the solution to the this problem. As outlined in step 3 above, if we fail to prove a goal using a particular retrieved clause, we will move on and try the next one. The default behavior when a solution is found is to return the bindings to the user; we need a mechanism to force the system to fail before it returns if the user doesn't like the bindings that were found.
We accomplish this task with a built-in function called display_bindings
.
This function is stored in the database so that it looks like a clause, and
before we ask the system to prove a goal we add the goal "display_bindings"
to the list of goals to prove. When the system tries to prove it, the
retrieved value from the database will be the function display_bindings
instead of a list of clauses. Our prove
function will detect that this
is not a list of clauses, call display_bindings
with the current state of
the system, and return the return value of that function call. We will let
display_bindings
decide how to handle finding more solutions.
Prove each goal in goals using the rules and facts in db.
def prolog_prove(goals, db):
if goals:
vars = []
for goal in goals:
vars.extend(goal.get_vars())
db['display_bindings'] = display_bindings
prove_all(goals + [Relation('display_bindings', vars)], {}, db)
print 'No.'
Displays bindings to the user and determines if more solutions are needed.
If the user wants to see another solution, returns False, causing the proving process to fail and try another path. Otherwise, continues proving the remaining goals.
def display_bindings(vars, bindings, db, remaining):
if not vars:
print 'Yes.'
for var in vars:
print var, ':', var.lookup(bindings)
if raw_input('Continue? ').strip().lower() in ('yes', 'y'):
return False
return prove_all(remaining, bindings, db)
That's all there is to it. See the examples mentioned earlier for some interesting applications of logic programming.
import logging
__author__ = 'Daniel Connelly (dhconnelly@gmail.com)'