This chapter first gives an example of the sort of
things that logic programming is capable of,
then gets on with the implementation by
introducing the concept of pattern matching.
Then it explores a generalization of pattern matching called
unification. Having implemented unification and other
more specialized support routines in the interpreter core,
we then proceed, with the help
of amb
from Chapter 16, to build a logic programming
system in the PScheme language itself. The advantages of doing this
in a language which has continuation-passing and backtracking
built in should become very apparent by the end of the chapter.
This implementation is based on the one given in
[eopl pp295–300], but made a little easier by
using amb
.
Logic programs consist of a database of known facts about a problem, and then typically a query or queries that interrogate this database.
Here is a very simple database of facts about a problem domain.
(define the-rules '(((mary likes wine)) ((mary likes cheese)) ((john likes beer)) ((john likes wine)) ((john likes chips)) ((person mary)) ((person john))))
Our database is called the-rules
and it is a list of
statements of various sorts. This database lists facts about what
mary
and john
like, and also the facts that
both mary
and john
are people. There is nothing
special about the structure of these individual facts, just as long
as we remain consistent in their use, and write queries that interrogate
the database appropriately. In other words it is we, the programmers,
who decide the “meaning” of ((mary likes wine))
:
the system attaches no particular significance to that structure
in itself; in particular likes
is not a keyword or an
operator of the logic programming system, it is just a symbol that
I have chosen to use.
In our logic programming implementation, we will use symbols with
initial capital letters as
pattern variables which can match parts of the database.
So given the database above, the system can respond to a query such as
(mary likes X)
with the facts
(mary likes wine)
and (mary likes cheese)
,
and can respond to the question (person X)
with the facts (person mary)
and (person john)
.
Of course there is nothing here that a simple SQL query
could not do, so let's make things more interesting by
adding a rule to the facts.
This rule states “mary likes anyone who likes chips.” This is written as:
((mary likes X) (person X) (X likes chips))
You can read this as “mary likes X
if
person X
and X likes chips
.”
Rules all have this general form. The first statement in the rule is true if all of the other statements in the rule are true or can be proved to be true. The first statement is called the head of the rule, and the remaining statements are called the body of the rule.
Looked at in this way, bare facts are just rules with no body: they are true in themselves because there is nothing left to prove. This explains the apparently redundant extra parentheses around each fact in our example database.
Given our extended database, which now looks like this:
(define the-rules '(((mary likes wine)) ((mary likes cheese)) ((john likes beer)) ((john likes wine)) ((john likes chips)) ((person mary)) ((person john)) ((mary likes X) (person X) (X likes chips)))
the system can answer the
question (mary likes john)
in the affirmative,
and furthermore, when prompted to list all the things that
mary likes with (mary likes X)
, john will be among
the results:
> (prove '((mary likes X))) > ? ((mary likes wine)) > ? ((mary likes cheese)) > ? ((mary likes john))
Also note that the statement to be proved has those apparently redundant extra braces too. This is because the system can be asked to prove any number of things at once, for example:
> (prove '((mary likes X) (X likes beer))) ((mary likes john) (john likes beer)) > ? Error: no more solutions
This can be read as “prove mary likes X
and
X likes beer
.”
The query only succeeds if all of the components succeed,
so it is just like the body of a rule in this respect.
This type of programming can also be used for recursive search. Figure 17.1 shows a small snippet of the Bach family tree, with old J. S. at the centre.
We can translate that into the following facts:
(((johann ambrosius) father-of (j s))) (((j c friedrich) father-of (w f ernst))) (((j s) (anna magdalena) parents-of (j c friedrich))) (((j s) (anna magdalena) parents-of (johann christian))) (((j s) (maria barbara) parents-of (wilhelm friedmann))) (((j s) (maria barbara) parents-of (c p e)))
Now, we have a mixture of facts about fathers alone, and parents where the mother is known. But we can rectify that with a few extra rules as follows:
((X father-of Y) (X _ parents-of Y)) ((X mother-of Y) (_ X parents-of Y)) ((X parent-of Y) (X father-of Y)) ((X parent-of Y) (X mother-of Y))
That underscore is a special pattern variable that always matches
anything. The first rule then says “X
is the father of
Y
if X
and anybody are parents of Y
”
(the parents-of
facts always list the father first.)
Likewise the second rule says “X
is the mother of Y
if anybody and X
are parents of Y
.”
The last pair of rules (actually really one rule in two parts) says that
“X
is a parent of Y
if X
is the
father of Y
or X
is the mother of Y
.”
So we have a general way of expressing both and
and or
in our rules: and
is expressed
by adjacent statements in the body of a single rule, while or
is expressed as alternative versions of the same rule.
Now that we have a general parent-of
relation, we can
add a recursive ancestor-of
relationship as follows:
((X ancestor-of Y) (X parent-of Y)) ((X ancestor-of Y) (X parent-of Z) (Z ancestor-of Y))
This says “X
is an ancestor of Y
if
X
is a parent of Y
or X
is a
parent of some Z
and Z
is an ancestor of
Y
.” Given that definition, and the rest of the facts
and rules, we can start to ask interesting questions of the system:
> (prove '((X ancestor-of (w f ernst)))) (((j c friedrich) ancestor-of (w f ernst))) > ? (((johann ambrosius) ancestor-of (w f ernst))) > ? (((j s) ancestor-of (w f ernst))) > ? (((anna magdalena) ancestor-of (w f ernst))) > ? Error: no more solutions
We can add yet more rules to this database. For example
X
and Y
are siblings if X
and Y
have the same parent:
((X sibling-of Y) (Z parent-of X) (Z parent-of Y) (require (not (eq? 'X 'Y))))
If we don't require
that X
and Y
are not equal then this rule would think that old J. S. was his own brother.
Given that, we can ask:
> (prove '(((c p e) sibling-of X))) (((c p e) sibling-of (johann christian)))
etc.
In case you're starting to think that logic programming is just some sort of glorified database lookup, here's a more meaty example. Consider the problem of appending two lists. You can write an append function in PScheme very easily^{53} as:
(define append (lambda (a b) (if a (cons (car a) (append (cdr a) b)) b)))
It walks to the end of the list a
, then at that point returns
the list b
, and as the recursion unwinds it builds a copy of
a
prepended to b
. So for example:
> (append '(a b) '(c d)) (a b c d)
This definition is useful enough in itself, but logic programming
allows a much more flexible definition of append
as
follows:
(define the-rules (list '((append () Y Y)) '((append (A . X) Y (A . Z)) (append X Y Z))))
Note that this uses the PScheme dotted pair notation introduced in
Section 8.4.1. So the expression (A . X)
refers to
a list who's car
is A
and who's cdr
is X
.
The first rule says that the result of appending something
to the empty list is just that something. The second rule says
that you can join (A . X)
and Y
to make (A . Z)
if you can join X
and Y
to make Z
.
Why is that more powerful than the PScheme append
?
Because we can ask lots of questions of it. Not only can we ask
“what do we get if we append (a b)
and (c d)
?”:
> (prove '((append (a b) (c d) X))) ((append (a b) (c d) (a b c d)))
We can also ask “what do we need to append to (a)
to get (a b c d e)
?”:
> (prove '((append (a) X (a b c d e)))) ((append (a) (b c d e) (a b c d e)))
And even “what can we append together to make (a b c d)
?”:
> (prove '((append X Y (a b c d)))) ((append () (a b c d) (a b c d))) > ? ((append (a) (b c d) (a b c d))) > ? ((append (a b) (c d) (a b c d))) > ? ((append (a b c) (d) (a b c d))) > ? ((append (a b c d) () (a b c d))) > ? Error: no more solutions
This idea is absolutely core to the concept of logic programming. A rule that states that “A and B make C” is equally capable of describing “what do I need to make C?” provided C has a value when the question is asked. It is as if the relationship described by the rule can be inspected from many different angles when seeking a solution to a problem.
Back to append
. The rules for append
can of course be made
available to other rules, for example (peeking ahead a bit)
((sentence S) (append NP VP S) (noun-phrase NP) (verb-phrase VP))
Says S
is a sentence if you can append NP
and VP
to make S
, and NP
is a
noun phrase, and VP
is a verb phrase. Rules
for noun-phrase
and verb-phrase
would be
very similar, and rules for individual words would just be
of the form ((noun (garage)))
etc.
The above examples have already demonstrated that our database of rules can be recursive, so how about the king of recursive functions, our old friend the factorial function? Here it is recast into a pair of rules:
(define the-rules (list '((factorial 0 1)) '((factorial N X) (T is (- N 1)) (factorial T U) (X is (* N U)))))
This isn't as bad as it might first look. The first rule is the bare fact
that the factorial of 0
is 1
.
The second rule says that the factorial of N
is
X
if
T
is
N - 1
and
the factorial of
T
is
U
and
X
is
N * U
. The special infix is
operator forces arithmetic
evaluation of its right hand side, then requires that its left hand
side is the same as the result of that evaluation.
given the above we can calculate factorials:
> (prove '((factorial 10 X))) ((factorial 10 3628800))
However there is a limitation here. Because of the unidirectional nature
of that is
operator, we cannot ask “what number can we apply
factorial
to to get x
”:
>(prove '((factorial X 3628800))) Error: no more solutions
So it goes.
If you're still not impressed, how about a more difficult problem? I hope you don't mind a little maths. This next example states some of the rules of symbolic differentiation then asks the system to work out the differential of an equation. The rules we'll be using are:
x
in x
is 1
.x
is 0
.x^{n}
in x
is n×x^{n-1}
.f+g
in x
is df+dg
if
the derivative of f
in x
is df
and the derivative of
g
in x
is dg
.f-g
in x
is
df-dg
if
the derivative of f
in x
is
df
and
the derivative of g
in x
is
dg
.f×g
in x
is f×dg+g×df
if the derivative of f
in x
is df
and the derivative of g
in x
is dg
.1/f
in x
is -df/f^{2}
if the derivative of f
in x
is df
.f/g
in x
is (g×df - f×dg)/f^{2}
if the derivative of f
in x
is df
and the derivative of g
in x
is dg
.If you don't remember the maths from school, just sit back and enjoy the ride. These rules can translate directly into our logic system as:
(define the-rules (list '((derivative X X 1)) '((derivative N X 0) (require (number? 'N))) '((derivative (X ^ N) X (N * (X ^ P))) (P is (- N 1))) '((derivative (F + G) X (DF + DG)) (derivative F X DF) (derivative G X DG)) '((derivative (F - G) X (DF - DG)) (derivative F X DF) (derivative G X DG)) '((derivative (F * G) X ((F * DG) + (G * DF))) (derivative F X DF) (derivative G X DG)) '((derivative (1 / F) X ((- DF) / (F * F))) (derivative F X DF)) '((derivative (F / G) X (((G * DF) - (F * DG)) / (G * G))) (derivative F X DF) (derivative G X DG))))
This is obviously way more complex than Mary and John,
but there isn't actually much that you haven't seen before.
The first and most important thing to realise is that, with
one exception, the arithmetic operators “+
”,
“-
” etc. mean nothing special to the logic
program: they are just symbols in patterns to be matched.
Having said that we do need ways to perform numeric tests
and to do arithmetic.
The body of second rule requires
that
N
is a number, and the body of third rule
evaluates (- N 1)
before “assigning” it to P
.
Rules of the form (require ‹expr›)
and (‹var› is ‹expr›)
are recognized and treated specially by the system.
Anyway, having entered these rules we can ask the system:
(prove '((derivative (((x ^ 2) + x) + 1) x X)))
That is to say “prove the differential of
x^{2} + x + 1
in x
is X
”. The system replies:
((derivative (((x ^ 2) + x) + 1) x (((2 * (x ^ 1)) + 1) + 0)))
The last line is the computed value for X
, the pattern
variable in the query. For now we will have to simplify that manually:
(((2 * (x ^ 1)) + 1) + 0) (2 * x ) + 1
You can see that the result is indeed the differential of x^{2}
+ x + 1
, namely 2x + 1
.
That should be enough to whet your appetite for what the rest
of this chapter has to offer. We next turn our attention to pattern
matching, which is the basis of unification, which along with amb
from the previous chapter is the basis of our logic programming
implementation.
The kind of pattern matching we will be discussing here has very little if anything to do with regular expressions. This sort of pattern matching is about matching a pattern against a structure, not a string, and furthermore the pattern itself is a structure.
A pattern or a structure, for the purposes of our discussion is a PScheme expression: a string, number, symbol or list. However a pattern may also contain pattern variables. These are not the normal variables of PScheme programs: any symbol is a variable in that sense; these are a special type of symbol, recognised as a variable only by the pattern matching system. As far as the rest of PScheme is concerned, they are just ordinary symbols. For our purposes a pattern variable will be any symbol that starts with a capital letter^{54}. Although I'm calling these symbols “pattern variables” here, I'll drop that convention in future and just call them “variables” when the context makes it clear what I mean.
First let's look at a few examples of pattern matching.
(a b c)
will only match the
structure (a b c)
because the pattern contains
no variables.(a b c)
will not match the
structure (a b foo)
because c
does not
equal foo
.(a X c)
will match the structure
(a b c)
because the variable X
can stand for the symbol b
.X
will match the structure
(a b c)
because X
can stand for the
entire structure.(a X c)
will match the structure
(a (1 2 3) c)
because X
can stand for
(1 2 3)
.(a (1 X 3) c)
will match the structure
(a (1 2 3) c)
because X
can stand for
2
.(a X Y)
will
match the structure (a b c)
because
X
can stand for b
and
Y
can stand for c
.(a X X)
will not
match the structure (a b c)
because
the variable X
must stand for the same thing
throughout the matching process: it cannot be both
b
and c
.I'm sure you get the idea by now.
The result of a pattern match is a set of bindings,
one for each variable that matched. For example after matching
the pattern (a X Y)
against (a (1 2 3) b)
the result is the set of bindings X => (1 2 3)
and Y => b
.
This result is much
the same as an environment, and we'll take advantage of this
equivalence later.
As I've said, pattern matching is merely a precursor to unification, which is our goal. Implementing a pattern matching system in Pscheme is fairly trivial, either in the PScheme language itself or in the underlying Perl, but we're not actually going to do that, because it isn't powerful enough for our purposes. However we need to start somewhere, so this section discusses a standalone pattern-matching implementation in Perl. It's easy enough to understand, and the subsequent section builds on that to produce a standalone unification implementation. Having arrived at a standalone unification implementation, we can wire that in to our interpreter.
But first we need to look at pattern matching. This standalone Perl pattern matcher can take patterns of the form:
['a', { b => 'X'}, 'Y']
where capitalized strings represent the pattern variables. It matches them against structures such as
['a', { b => [2, 3] }, 'c']
returning a hashref that will look like
{ X => [2, 3], Y => 'c' }
Here's a birds-eye view of how our first pattern matcher will
work. It walks both the pattern and the structure in parallel, also
passing an additional, initially empty environment around.
If it encounters a variable in the pattern then it checks to see
if the variable is already set in the environment. If it
is, then it checks that the current structure component is
the same as the value of the variable, failing if it is not.
If the variable is not set in the environment, it extends the
environment, binding the variable to the current structure component,
and continues. Of course matching will also fail if the pattern
and the structure are not otherwise identical. On success,
it returns the environment, and on failure, it die
s.
Both for the fun of it, and for completeness' sake, the pattern matcher described here can handle perl hashrefs as well as listrefs. This means it will accept patterns and structures containing mixtures of both types. However only the values of a hash in a pattern will be recognised as pattern variables, the keys will not.
Here's the top-level match()
routine:
sub match { my ($pattern, $struct, $env) = @_; $env ||= {}; if (var($pattern)) { match_var($pattern, $struct, $env); } elsif (hashes($pattern, $struct)) { match_hashes($pattern, $struct, $env); } elsif (arrays($pattern, $struct)) { match_arrays($pattern, $struct, $env); } elsif (strings($pattern, $struct)) { match_strings($pattern, $struct, $env); } else { fail(); } return $env; }
Firstly, if $env
is not passed, then match()
initializes it to an empty hashref. The pattern matching
algorithm is never required to undo any variable bindings that
it creates, so we can just pass around a hash by reference and
allow the bindings to accumulate in it.
Then we see various tests for the types of $pattern
and $struct
. The var()
check is just:
sub var { my ($thing) = @_; !ref($thing) && $thing =~ /^[A-Z]/; }
So a var is any string that starts with a capital letter.
The hashes()
check returns true if both arguments are
hashrefs:
sub hashes { my ($a, $b) = @_; hash($a) && hash($b); }
Where hash()
is just:
sub hash { my ($thing) = @_; ref($thing) eq 'HASH'; }
The other two checks, arrays()
and strings()
are defined
equivalently:
sub arrays { my ($a, $b) = @_; array($a) && array($b); } sub array { my ($thing) = @_; ref($thing) eq 'ARRAY'; } sub strings { my ($a, $b) = @_; string($a) && string($b); } sub string { my ($thing) = @_; !var($thing) && !ref($thing); }
Ok, that's the administrative support out of the way.
So the
first thing that match()
does, if its $pattern
is a var()
, is to call match_var()
on the
$pattern
and the $struct
, passing the current
environment.
Here's match_var()
:
sub match_var { my ($var, $struct, $env) = @_; if (exists($env->{$var})) { match($env->{$var}, $struct, $env); } else { $env->{$var} = $struct; } }
It checks to see if the $var
is in the environment.
If it is then it attempts to match()
the value of
the variable against the $struct
^{55}.
If the $var
is not already
in the environment then it puts it there with a value equal
to the current $struct
(an unassigned variable
will always match the current structure component,
and will be instantiated to it.)
Returning to match()
, if both the $pattern
and the $struct
are arrays()
,
match()
calls match_arrays()
on them.
match_arrays()
walks both arrays
in tandem, calling match()
on each pair of
elements.
If the arrays are not the same length then they cannot possibly
match, so this sanity check is performed first:
sub match_arrays { my ($pattern, $struct, $env) = @_; my @patterns = @$pattern; my @structs = @$struct; if (@patterns != @structs) { fail(); } while (@patterns) { match(shift @patterns, shift @structs, $env); } }
The fail()
sub die
s with a
"match failed"
message:
sub fail { die "match failed\n"; }
Back to match()
again. If the $pattern
and
the $struct
are both hashes()
, then match()
calls match_hashes()
on them:
sub match_hashes { my ($pattern, $struct, $env) = @_; check_keys_eq($pattern, $struct); foreach my $key (sort keys %$pattern) { match($pattern->{$key}, $struct->{$key}, $env); } }
Much as match_arrays()
checks that the two arrays
are the same length, match_hashes()
checks that the
two hashes have the same keys using check_keys_eq()
:
sub check_keys_eq { my ($as, $bs) = @_; my $astr = join('.', sort keys %$as); my $bstr = join('.', sort keys %$bs); fail unless $astr eq $bstr; }
This is a cheap trick and could easily be fooled, but it's good enough for our demonstration purposes.
Assuming that the hashes have equal keys (this pattern
matcher does not allow—or at least expect—hash
keys to be variables), match_hashes()
walks the keys
matching the individual components
in much the same way as match_arrays()
did.
It sorts the keys before traversing them to ensure the order
of any variable assignment is at least deterministic.
Back to match()
yet again. If both the $pattern
and the $struct
are strings()
, match()
calls
match_strings()
on them. This is the most trivial
of the matching subroutines: it just compares the strings
and fails if they are not equal:
sub match_strings { my ($pattern, $struct, $env) = @_; fail if $pattern ne $struct; }
This completes our prototype pattern matching implementation.
While very simple, this pattern matcher can be made to do useful work. Consider a “database” of facts in a Perl list:
my @facts = ( { composer => 'beethoven', initials => 'lv', lived => [1770, 1829] }, { composer => 'mozart', initials => 'wa', lived => [1756, 1791] }, { composer => 'bach', initials => 'js', lived => [1685, 1750] } );
We can use the matcher to extract information from this list:
foreach my $fact (@facts) { eval { my $result = match({ composer => 'COMPOSER', initials => 'js', lived => 'LIVED' }, $fact); print "The composer with initials 'js'", " is $result->{COMPOSER}", " who lived from $result->{LIVED}[0]", " to $result->{LIVED}[1]\n"; }; }
That's it for pattern matching. We next turn our attention to Unification, which as I've said is an extension to Pattern Matching and is much more interesting.
Unification, in a nutshell, is the matching of two patterns. It solves the problem “given two patterns, that might both contain variables, find values for those variables that will make the two patterns equal.”
Our pattern matcher from the previous section is a good jumping off point for implementing true unification. In fact it has most of the things we'll need already in place. The next section discusses the modifications we will need to make to it.
This unifier can solve a broader class of problems than a simple pattern matcher can. For example given the two patterns:
['f', ['g', 'A'], 'A']
and
['f', 'B', 'abc']
It can correctly deduce:
A => 'abc', B => ['g', 'abc']
You can see the process graphically in Figure 17.2.
The variable 'A'
unifies with the term 'abc'
while the variable 'B'
unifies with the compound term
['g', 'A']
, where 'A'
is provided with a value
'abc'
from the previous unification.
['f', ['g', 'A'], 'A']
with ['f', 'B', 'abc']
Unification is capable of even more complex resolutions, for example it can unify (ommitting quotes for brevity this time)
[F, [A, 1, B], [A, B], 2]
with
[C, [D, D, E], C, E]
To show that
A = 1
B = 2
C = [1, 2]
D = 1
E = 2
F = [1, 2]
You can see this in action in Figure 17.3 if you just follow the differently styled arrows starting from the three ringed nodes in the figure as they propogate information around.
This unifier has additional feature: the anonymous
variable “_
” (underscore) behaves
like a normal variable but will always match anything,
since it is never instantiated. This allows you to specify
a “don't care” condition. For example, going back to our
database of composers, the pattern:
{ composer => 'COMPOSER', initials => '_', lived => '_' }
will just retrieve all of the composers names
from the database, without testing or instantiating any other variables.
Not also that since “_
” always matches, and
is never instantiated, it can be reused throughout a pattern.
This unifier is a direct modification of the pattern matcher from
the previous section, so let's just concentrate on the
differences. Firstly match()
has been renamed
to unify()
, and it has an extra clause, in case the
old structure, which is now also a pattern, contains
variables. The various match_*
subs have
also been renamed unify_*
, and the variables
$pattern
and $struct
,
now both patterns, have been renamed to just
$a
and $b
:
sub unify { my ($a, $b, $env) = @_; $env ||= {}; if (var($a)) { unify_var($a, $b, $env); } elsif (var($b)) { unify_var($b, $a, $env); } elsif (hashes($a, $b)) { unify_hashes($a, $b, $env); } elsif (arrays($a, $b)) { unify_arrays($a, $b, $env); } elsif (strings($a, $b)) { unify_strings($a, $b, $env); } else { fail(); } return $env; }
The extra clause, if $b
is a var, simply reverses
the order of the arguments to unify_var()
. Note that
the single environment means that variables will share across
the two patterns. If you don't want this, simply make sure that
the two patterns don't use the same variable names.
unify_hashes()
, unify_arrays()
and unify_strings()
are identical to their match_*
equivalents, except that
unify_arrays()
and unify_hashes()
call
unify()
instead of match()
on their components.
The var()
check is slightly different, to allow for the
anonymous variable:
sub var { my ($thing) = @_; !ref($thing) && ($thing eq '_' || $thing =~ /^[A-Z]/); }
That leaves unify_var()
, where the action is.
unify_var()
is still quite similar to match_var()
, it just
has more things to watch out for:
sub unify_var { my ($var, $other, $env) = @_; if (exists($env->{$var})) { unify($env->{$var}, $other, $env); } elsif (var($other) && exists($env->{$other})) { unify($var, $env->{$other}, $env); } elsif ($var eq '_') { return; } else { $env->{$var} = $other; } }
So $struct
was renamed to $other
, and
unify_var()
calls unify()
instead of match()
.
If $var
is not set in the environment, instead of immediately
assuming it can match $other
, unify_var()
looks to
see if $other
is a var and already has a value. If so it
calls unify()
on $var
and the value of $other
.
If $other
is not a var, or has no binding, unify_var()
next checks
to see if $var
is the anonymous variable. If it is, then
because the anonymous variable always matches and is never instantiated,
it just returns. Lastly, only when all
other options have been tried, it adds a binding from the $var
to $other
and returns.
Let's walk through the actions of unify()
as it attempts to
unify the two patterns ['f', ['g', 'A'], 'A']
and
['f', 'B', 'abc']
.
unify(['f', ['g', 'A'], 'A'], ['f', 'B', 'abc'], {})
is called with the two complete patterns
and an empty environment,
and determines that both patterns are arrays, so calls
unify_arrays()
.
unify_arrays(['f', ['g', 'A'], 'A'], ['f', 'B', 'abc'], {})
simply calls unify()
on
each component.
unify('f', 'f', ())
determines that both its arguments are
strings, and calls unify_strings()
.
unify_strings('f', 'f', {}) = {}
succeeds but the environment
is unchanged.
unify(['g', 'A'], 'B', {})
determines that it's second
argument is a variable and so calls unify_var()
with the arguments reversed.
unify_var('B', ['g', 'A'], {}) = {B => ['g', 'A']}
succeeds, and unify_var()
extends the environment with 'B'
bound to ['g', 'A']
.
unify('A', 'abc', {B => ['g', 'A']})
determines that it's first argument is
a variable and so calls unify_var()
again,
passing the environment that was extended by the
previous call to unify_var()
.
unify_var('A', 'abc', {B => ['g', 'A']}) = {B => ['g', 'A'], A => 'abc'}
also succeeds, extending the
environment with a new binding of 'A'
to
'abc'
. This environment is the final result
of the entire unification.
So the final result {B => ['g', 'A'], A => 'abc'}
falls
a little short of our expectations, because the value for 'B'
still contains a reference to the variable 'A'
^{56}. However this is not a problem as such. we can
patch up the result with a separate routine called resolve()
.
sub resolve { my ($pattern, $env) = @_; while (var($pattern)) { if (exists $env->{$pattern}) { $pattern = $env->{$pattern}; } else { return $pattern; } } if (hash($pattern)) { my $ret = {}; foreach my $key (keys %$pattern) { $ret->{$key} = resolve($pattern->{$key}, $env); } return $ret; } elsif (array($pattern)) { my $ret = []; foreach my $item (@$pattern) { push @$ret, resolve($item, $env); } return $ret; } else { return $pattern; } }
resolve()
takes a pattern, and the environment that
was returned by unify()
. If and while the pattern
is a variable, it repeatedly replaces it with its value from the
environment, returning the variable if it cannot further resolve it.
Then if the result is a hash or an array reference,
resolve()
recursively calls itself on each component of the
result, also passing the environment. The final result of
resolve()
is a structure where any variables in the pattern
that have
values in the environment have been replaced by those values.
Note that resolve()
does not change the environment in
any way.
This completes our stand-alone implementation of unify()
.
Hopefully seeing it out in the open like this will make the
subsequent implementation within PScheme easier to digest.
It is a little difficult to demonstrate the utility of
unify()
at this point, since it's purpose is mostly
part of the requirements of logic programming, however
to give you some idea, consider that the result of one unification,
an environment or hash, can be passed as argument to a second
unification, thus constraining the values that the pattern
variables in the second unification can potentially take.
There is one extremely interesting and useful application
of unification outside of logic programming which makes
use of this idea. Consider that we might
want to check that the types of the variables in a PScheme
expression are correct before we eval the expression.
Assume that we know the types of the arguments and return values
from all primitives in the language. Furthermore we
can also detect the types of any
variables which are assigned constants directly.
It is therefore possible to detect
if a variable's assigned value does not match it's eventual
use, even if that eventual use is remote (through layers of
function calls) from the original assignment.
Such a language, which does not declare types but is nonetheless
capable of detecting type mismatches, is called an implicitly
typed language.
We can use unification to do this type checking, by treating PScheme
variables as pattern variables and unifying them with their
types and with each other across function calls,
accumulating types of arguments and return values for
lambda
expressions and functions in the process.
That however, is for another chapter. Next we're going to look at the implementation of unify in PScheme.
unify
in PSchemeTo get the ball rolling with the implementation
of unify
, notice that the previous implementation
of unify()
frequently tests the types of its arguments.
Obviously in an object-oriented implementation like PScheme we can
distribute a Unify()
method around the various data types
and avoid this explicit type checking for the most part.
A second point worth noting is that where the above unify()
did a die
on failure, our new Unify()
can quite
reasonably invoke backtracking instead, to try another option,
which fits in quite neatly
with our existing amb
implementation.
A third and final point. unify()
above made use of a flat
hash to keep track of variable bindings, but PScheme already has a
serviceable environment implementation and we should make use of
it. This will mean exposing the environment as a PScheme data type
since that is what is explicitly passed to and returned by
Unify()
, but this is not a concern since we have done this
once before in our classes and objects extension from Chapter 12.
We'd better start by looking at the unify
command in
action in the interpreter. The result of a call to unify
is a PScm::Env which isn't much direct use. However we can
add another PScheme command that will help us out there.
substitute takes a form and an environment, and replaces
any pattern variables in the
form with their values from the argument environment. It
also performs the resolve()
function on each value before
substitution. So for example:
> (substitute > '(f B A) > (unify '(f (g A) A) > '(f B abc))) (f (g abc) abc)
The call to unify
provides the second argument, an
environment, to substitute
, which then performs the
appropriate replacements on the expression (f B A)
to produce the result (f (g abc) abc)
. Note that in
all cases we have to quote the expressions to prevent them
from being evaluated. We do need the interpreter to evaluate the arguments
to substitute
and unify
in most cases
however, because the
actual forms being substituted and unified may be passed
in as (normal PScheme) variables or otherwise calculated.
I should probably also demonstrate that
unify
does proper backtracking if it fails:
> (unify '(a b c) '(a b d)) Error: no more solutions
It's still somewhat difficult to demonstrate the usefulness
of unify
combined with amb
at this stage however.
That will have to wait until
the next section
where we finally get to see logic programming in action.
The first thing we need to do then, is to create a new special form
PScm::SpecialForm::Unify and give it an Apply()
method. This special form will be bound to the symbol unify
in the top-level environment. unify
will take two or three
arguments. The first two arguments are the patterns to be unified. The third,
optional argument is an environment to extend. If unify
is not passed an environment, it will create a new, empty one.
We have to make unify
a special form because it needs access
to the failure continuation. Here's
PScm::SpecialForm::Unify:
504 package PScm::SpecialForm::Unify; 505 506 use base qw(PScm::SpecialForm); 507 508 use PScm::Continuation; 509 510 sub Apply { 511 my ($self, $form, $env, $cont, $fail) = @_; 512 $form->map_eval( 513 $env, 514 cont { 515 my ($evaluated_args, $fail) = @_; 516 my ($a, $b, $qenv) = $evaluated_args->value; 517 $qenv ||= new PScm::Env(); 518 $a->Unify($b, $qenv, $cont, $fail); 519 }, 520 $fail 521 ); 522 } 523 524 1;
You can see that it uses map_eval()
from Section 13.6.5
to evaluate its argument
$form
, passing it a continuation that breaks out the
patterns $a
and $b
, and the optional environment
$qenv
from the evaluated arguments. Then
it defaults $qenv
to a new, empty environment,
and calls Unify()
on $a
passing it the other pattern,
the query environment and the success and failure continuations.
Referring back to our test implementation of unify()
in
Section 17.3.1
we can see that the first thing that implementation does is to check if its first
argument is a var, and if so call unify_var()
on it.
We can replace this explicit conditional with polymorphism
by putting a Unify()
method at an appropriate place
in the PScm::Expr hierarchy. But the
PScm::Expr::Symbol class is not the best place:
not all symbols are pattern variables, only those starting
with capital letters or underscores. So here's the trick.
We create a new subclass of PScm::Expr::Symbol
called PScm::Expr::Var and put the method there.
Read()
can detect pattern variables on input and create
instances of this new class instead of PScm::Expr::Symbol.
Since the new class inherits from PScm::Expr::Symbol,
and we do not override any of that class's existing methods,
these new PScm::Expr::Var objects behave exactly
like ordinary symbols to the rest of the PScheme implementation.
Here's the change to _next_token()
from PScm::Read to make this happen.
66 sub _next_token { 67 my ($self) = @_; 68 69 while (!$self->{Line}) { 70 $self->{Line} = $self->{FileHandle}->getline(); 71 return undef unless defined $self->{Line}; 72 $self->{Line} =~ s/^\s+//s; 73 } 74 75 for ($self->{Line}) { 76 s/^\(\s*// && return PScm::Token::Open->new(); 77 s/^\)\s*// && return PScm::Token::Close->new(); 78 s/^\'\s*// && return PScm::Token::Quote->new(); 79 s/^\,\s*// && return PScm::Token::Unquote->new(); 80 s/^\.\s*// && return PScm::Token::Dot->new(); 81 s/^([-+]?\d+)\s*// 82 && return PScm::Expr::Number->new($1); 83 s/^"((?:(?:\\.)|([^"]))*)"\s*// && do { 84 my $string = $1; 85 $string =~ s/\\//g; 86 return PScm::Expr::String->new($string); 87 }; 88 s/^([A-Z_][^\s\(\)]*)\s*// 89 && return PScm::Expr::Var->new($1); 90 s/^([^\s\(\)]+)\s*// 91 && return PScm::Expr::Symbol->new($1); 92 } 93 die "can't parse: $self->{Line}"; 94 }
The only change is on
Lines 88–89
where if the token matched starts with a capital letter or underscore
then _next_token()
returns a new PScm::Expr::Var where otherwise
it would have returned a PScm::Expr::Symbol.
Now we have somewhere to hang the functionality equivalent to
unify_var()
from our test implementation, we can put it
in a method called Unify()
in PScm::Expr::Var:
378 sub Unify { 379 my ($self, $other, $qenv, $cont, $fail) = @_; 380 381 if (defined(my $value = $qenv->LookUpNoError($self))) { 382 $value->Unify($other, $qenv, $cont, $fail); 383 } elsif ($other->is_var && 384 defined (my $other_value = $qenv->LookUpNoError($other))) { 385 $other_value->Unify($self, $qenv, $cont, $fail); 386 } elsif ($self->is_anon) { 387 $cont->Cont($qenv, $fail); 388 } else { 389 $qenv->ExtendUnevaluated( 390 new PScm::Expr::List($self), 391 new PScm::Expr::List($other), 392 $cont, 393 $fail 394 ); 395 } 396 }
It's identical to the earlier unify_var()
except that it
makes use of method calls and is written in CPS. The is_var()
method is defined to be false at the root of the expression
hierarchy in PScm::Expr, but is overridden to be true in
PScm::Expr::Var alone. Equivalently is_anon()
is defined false in PScm::Expr but defined to be true
if the value of the var is “_
” in
PScm::Expr::Var^{57}:
400 sub is_anon { 401 my ($self) = @_; 402 $self->value eq '_'; 403 }
The only other occurrence of Unify()
is at the root
of the hierarchy in PScm::Expr:
49 sub Unify { 50 my ($self, $other, $qenv, $cont, $fail) = @_; 51 if ($other->is_var) { 52 $other->Unify($self, $qenv, $cont, $fail); 53 } else { 54 $self->UnifyType($other, $qenv, $cont, $fail); 55 } 56 }
This really just takes care of the case where the first pattern
is not a var but the second pattern is. If the second pattern is a var
it calls Unify()
on it, passing $self
as the argument,
reversing the order in the same way as our prototype unify()
did.
If the second pattern is not a var, then it calls a new method
UnifyType()
on $self
. UnifyType()
is just
another name for Unify()
and allows a second crack at
polymorphism since it is implemented separately in a couple of places
in the PScm::Expr hierarchy.
The first such place is in PScm::Expr itself.
58 sub UnifyType { 59 my ($self, $other, $qenv, $cont, $fail) = @_; 60 if ($self->Eq($other)) { 61 $cont->Cont($qenv, $fail); 62 } else { 63 $fail->Fail(); 64 } 65 }
This works for all atomic data types. If the two patterns are Eq()
then succeed, otherwise fail. This is the first place we've actually seen
the failure continuation invoked. Note that the equality test Eq()
implicitly deals with type equivalence for us, so we don't need the
arrays()
routines etc. from the prototype.
Now the only other place we need to
put UnifyType()
is in PScm::Expr::List::Pair
276 sub UnifyType { 277 my ($self, $other, $qenv, $cont, $fail) = @_; 278 if ($other->is_pair) { 279 $self->[FIRST]->Unify( 280 $other->[FIRST], 281 $qenv, 282 cont { 283 my ($qenv, $fail) = @_; 284 $self->[REST]->Unify( 285 $other->[REST], 286 $qenv, 287 $cont, 288 $fail 289 ); 290 }, 291 $fail 292 ); 293 } else { 294 $fail->Fail(); 295 } 296 }
This PScm::Expr::List::Pair::UnifyType()
is in fact simpler
in one sense than the unify_arrays()
from our test implementation.
First it performs a simple check that the $other
is a list.
If not it calls the failure continuation. Then,
rather than walking both lists, it only needs to call Unify()
on its first()
and rest()
, passing the $other
's
first()
or rest()
appropriately. Of course this is a
little complicated because it's in CPS, but nonetheless that is
all it has to do.
That's all for unify
itself. If you remember from the start
of this section, we will also need a substitute
builtin to
replace pattern variables with values in the environment. It is called
like (substitute ‹pattern› ‹env›)
and returns the ‹pattern›
suitably
instantiated. We can make this a primitive rather than a
special form because it has no need of an environment (other than
the one that is explicitly passed) and no need to access the failure
continuation (it always succeeds). Here's
PScm::Primitive::Substitute:
216 package PScm::Primitive::Substitute; 217 218 use base qw(PScm::Primitive); 219 220 sub _apply { 221 my ($self, $body, $qenv) = @_; 222 $body->Substitute($qenv->ResolveAll()); 223 }
It does nothing much by itself, merely calling a ResolveAll()
method on the argument environment then passing the result to the
$body
's Substitute()
method. We'll take a look at
that new PScm::Env::ResolveAll()
method first.
266 sub ResolveAll { 267 my ($self) = @_; 268 my %bindings; 269 foreach my $var ($self->Keys) { 270 $bindings{$var} = $self->Resolve(new PScm::Expr::Var($var)); 271 } 272 return $self->new(%bindings); 273 }
This ResolveAll()
loops over each key in the environment,
calling a subsidary Resolve()
method on each and saving the
result in a temporary %bindings
hash. Then it creates
and returns a new PScm::Env with those bindings.
If you refer back to our resolve()
function in the
prototype, you can see that in the first stage, if the $pattern
is a variable, it repeatedly attempts to replace it with a value
from the environment until either it is not a variable anymore or
it cannot find a value. This ResolveAll()
is effectively
pre-processing the environment so that any subsequent lookup
for a pattern variable will not need to perform that iteration.
Keys()
just collects all the keys from the environment:
275 sub Keys { 276 my ($self, $seen) = @_; 277 $seen ||= {}; 278 foreach my $key (keys %{$self->{bindings}}) { 279 $seen->{$key} = 1; 280 } 281 if ($self->{parent}) { 282 $self->{parent}->Keys($seen); 283 } 284 return (keys %$seen); 285 }
and Resolve()
does exactly what resolve()
did in
our test implementation: it repeatedly replaces the variable with
its value from the environment until the variable is not a variable
any more, or cannot be found. If it finds a non-variable value it
calls its ResolveTerm()
method on it, passing the env
$self
as argument, and returning the result.
287 sub Resolve { 288 my ($self, $term) = @_; 289 while ($term->is_var) { 290 if (my $val = $self->LookUpNoError($term)) { 291 $term = $val; 292 } else { 293 return $term; 294 } 295 } 296 return $term->ResolveTerm($self); 297 }
ResolveTerm()
gives any compound term a chance to
resolve any pattern variables it may contain. There are two
definitions of ResolveTerm()
.
The only compound terms in PScheme are lists, and pattern
variables themselves have already been resolved, so the default
ResolveTerm()
in PScm::Expr just returns
$self
:
67 sub ResolveTerm { 68 my ($self, $qenv) = @_; 69 return $self; 70 }
The second definition of ResolveTerm()
is, not
surprisingly, in PScm::Expr::List::Pair:
298 sub ResolveTerm { 299 my ($self, $qenv) = @_; 300 return $self->Cons($qenv->Resolve($self->[FIRST]), 301 $qenv->Resolve($self->[REST])); 302 }
It walks itself, calling the argument $qenv
's
Resolve()
method on each component, and returning
a new PScm::Expr::List of the results.
So we're talking about how substitute
works, and we
saw that primitive's _apply()
method called the argument
$qenv
's ResolveAll()
method to return a new environment
with any pattern variables in the values replaced, where possible.
Then _apply()
passed that
new environment to its argument $body
's Substitute()
method. We've just seen how ResolveAll()
works, now we can
look at Substitute()
itself.
Only pattern variables can be substituted, but lists
need to examine themselves to see if they contain any pattern
variables. So a default Substitute()
method
in PScm::Expr takes care of all the things that can't
be substituted, it just returns $self
:
72 sub Substitute { 73 my ($self, $qenv) = @_; 74 return $self; 75 }
The Substitute()
in PScm::Expr::Var
returns either its value from the environment or itself if it
is not in the environment:
405 sub Substitute { 406 my ($self, $qenv) = @_; 407 return $qenv->LookUpNoError($self) || $self; 408 }
Finally, the Substitute()
in PScm::Expr::List::Pair
recursively calls Substitute()
on each of its
components, constructing a new list of the results:
304 sub Substitute { 305 my ($self, $qenv) = @_; 306 return $self->Cons($self->[FIRST]->Substitute($qenv), 307 $self->[REST]->Substitute($qenv)); 308 }
And that's substitute
. To sum up, it tries as hard as
it can to replace all pattern variables in the form with values
from the environment, recursing not only into the form it is
substituting, but also into the values of the variables themselves.
There are a few more things we need to add to the interpreter before we can show off its new prowess. Firstly we will have occasion to pass an empty environment into unify (indirectly), and for that we'll need a new-env primitive. This is as simple as it gets:
258 package PScm::Primitive::NewEnv; 259 260 use base qw(PScm::Primitive); 261 262 sub _apply { 263 new PScm::Env(); 264 }
Another thing we'll need goes back to a passing comment I made a while back. It can be a problem if you try to unify two patterns that inadvertantly use the same pattern variable names. Sometimes you want the variables to share a value, and sometimes you don't. For this reason we need something that will take a pattern and replace its variable names with new variable names that are guaranteed to be unique. The same variable occurring more than once in the pattern should correspond to the same new variable occurring more than once in the result, but we should be reasonably confident that the new variable name won't appear anywhere else in the program by accident.
This new PScheme function is called instantiate.
It could be written in the PScheme language, but that would require
adding other less germane primitives for creating symbols etc. so
all in all it is probably better to build it in to the core.
It can be a primitive, but it will need a bit more than just
an _apply()
method:
267 package PScm::Primitive::Instantiate; 268 269 use base qw(PScm::Primitive); 270 271 sub new { 272 my ($class) = @_; 273 bless { 274 seen => {}, 275 counter => 0, 276 }, $class; 277 } 278 279 sub _apply { 280 my ($self, $body) = @_; 281 $self->{seen} = {}; 282 $body->Instantiate($self); 283 } 284 285 sub Replace { 286 my ($self, $var) = @_; 287 return $var if $var->is_anon; 288 unless (exists($self->{seen}{$var->value})) { 289 $self->{seen}{$var->value} = 290 new PScm::Expr::Var($self->{counter}++); 291 } 292 return $self->{seen}{$var->value}; 293 } 294 295 1;
Remember that there is only one instance of any given
primitive or special form in the PScheme environment, and that
persists for the duration of the repl. So by giving
this primitive its own new()
method we provide a
convenient place to store a singleton counter that we can
use to generate new symbols. The seen
field of the
object however, which keeps track of which variables the
instantiate
function has already encountered,
must be re-initialized to an empty hash on each separate
application of the primitive.
After (re-)initializing seen
on Line 281,
_apply()
calls its argument $body
's
Instantiate()
method passing $self
as argument.
Obviously the only PScm::Expr
type that will avail itself of the instantiate object is
PScm::Expr::Var, and that will make use
of the callback method Replace()
to find or
generate a replacement variable.
Replace()
then, first checks to see if
the variable is the anonymous variable
(Line 287).
If so then it just returns the variable, since the
anonymous variable never shares and should never be
replaced by a variable that will share. Then unless
it has already seen the variable it creates a new
alias for it by using the incrementing counter
(Lines 288–291).
This works well because the reader would never
create a PScm::Expr::Var from a number.
Just as with Unify()
and Substitute()
,
a default method Instantiate()
in PScm::Expr
handles most cases and just returns $self
:
79 sub Instantiate { 80 my ($self, $instantiator) = @_; 81 return $self; 82 }
The PScm::Expr::Var version of instantiate
calls the $instantiator
's Replace()
callback to get a new variable, passing $self
as argument because Replace()
needs to keep
track of the variables it has seen already:
412 sub Instantiate { 413 my ($self, $instantiator) = @_; 414 return $instantiator->Replace($self); 415 }
Finally PScm::Expr::List::Pair::Instantiate()
recurses on both its first()
and rest()
components, calling Instantiate()
on both
and constructing a new list on the way back out:
316 sub Instantiate { 317 my ($self, $instantiator) = @_; 318 return $self->Cons($self->[FIRST]->Instantiate($instantiator), 319 $self->[REST]->Instantiate($instantiator)); 320 }
The last thing we're going to need, for pragmatic reasons,
is a way to
check the type of various expressions from within the
PScheme language. A proper scheme implementation has a full
set of such type checking functions, but we're only going
to need pair?, number? and var?
(note the question marks.) They are all primitives, and in
fact have so much in common that we will create an abstract
parent class called PScm::Primitive::TypeCheck
and put a shared _apply()
method in there:
226 package PScm::Primitive::TypeCheck; 227 228 use base qw(PScm::Primitive); 229 230 sub _apply { 231 my ($self, $body) = @_; 232 if ($self->test($body)) { 233 return new PScm::Expr::Number(1); 234 } else { 235 return new PScm::Expr::Number(0); 236 } 237 }
You can see that it calls a test()
method which we
must subclass for each test, then it returns an appropriate
true or false value depending on the test. Here's the test
for pair?
in PScm::Primitive::TypeCheck::Pair:
240 package PScm::Primitive::TypeCheck::Pair; 241 use base qw(PScm::Primitive::TypeCheck); 242 243 sub test { $_[1]->is_pair }
We've already seen that is_pair()
is defined false in
PScm::Expr and overridden to be true in
PScm::Expr::List::Pair alone. The equivalent
number?
and var?
PScheme functions
are bound to PScm::Primitive::TypeCheck::Number
and PScm::Primitive::TypeCheck::Var, and make
use of equivalent is_number()
and is_var()
methods in PScm::Expr.
We have now implemented the four components we need to get on
with defining a logic programming language: unify
,
substitute
, new-env
and
instantiate
. Along with those we have also added
the three type tests pair?
, var?
and number?
which just check if their argument is of that type.
They are all wired in to the repl in the normal way, here's the
additions:
36 sub ReadEvalPrint { 37 my ($infh, $outfh) = @_; 38 39 $outfh ||= new FileHandle(">-"); 40 my $reader = new PScm::Read($infh); 41 my $initial_env; 42 $initial_env = new PScm::Env( 43 let => new PScm::SpecialForm::Let(), 44 '*' => new PScm::Primitive::Multiply(), 45 '-' => new PScm::Primitive::Subtract(), 46 '+' => new PScm::Primitive::Add(), 47 if => new PScm::SpecialForm::If(), 48 lambda => new PScm::SpecialForm::Lambda(), 49 list => new PScm::Primitive::List(), 50 car => new PScm::Primitive::Car(), 51 cdr => new PScm::Primitive::Cdr(), 52 cons => new PScm::Primitive::Cons(), 53 letrec => new PScm::SpecialForm::LetRec(), 54 'let*' => new PScm::SpecialForm::LetStar(), 55 eval => new PScm::SpecialForm::Eval(), 56 macro => new PScm::SpecialForm::Macro(), 57 quote => new PScm::SpecialForm::Quote(), 58 'set!' => new PScm::SpecialForm::Set(), 59 begin => new PScm::SpecialForm::Begin(), 60 define => new PScm::SpecialForm::Define(), 61 'make-class' => new PScm::SpecialForm::MakeClass(), 62 'call/cc' => new PScm::SpecialForm::CallCC(), 63 print => new PScm::SpecialForm::Print($outfh), 64 spawn => new PScm::SpecialForm::Spawn(), 65 exit => new PScm::SpecialForm::Exit(), 66 error => new PScm::SpecialForm::Error( 67 $outfh, 68 bounce { repl($initial_env, $reader, $outfh) } 69 ), 70 amb => new PScm::SpecialForm::Amb(), 71 'eq?' => new PScm::Primitive::Eq(), 72 '>' => new PScm::Primitive::Gt(), 73 '<' => new PScm::Primitive::Lt(), 74 '>=' => new PScm::Primitive::Ge(), 75 '<=' => new PScm::Primitive::Le(), 76 and => new PScm::SpecialForm::And(), 77 or => new PScm::SpecialForm::Or(), 78 unify => new PScm::SpecialForm::Unify(), 79 substitute => new PScm::Primitive::Substitute(), 80 'new-env' => new PScm::Primitive::NewEnv(), 81 instantiate => new PScm::Primitive::Instantiate(), 82 'pair?' => new PScm::Primitive::TypeCheck::Pair(), 83 'var?' => new PScm::Primitive::TypeCheck::Var(), 84 'number?' => new PScm::Primitive::TypeCheck::Number(), 85 ); 86 87 $initial_env->Define( 88 PScm::Expr::Symbol->new("root"), 89 PScm::Class::Root->new($initial_env) 90 ); 91 __PACKAGE__->new_thread(bounce { repl($initial_env, $reader, $outfh) }); 92 trampoline(); 93 }
You may want to refer back to Section 17.1 at the start of this chapter where we saw some examples of logic propgramming in action. However in order to explain how this all works, let's move away from our first examples and consider instead a very simple logic problem:
Socrates
- All men are mortal.
- Socrates is a man.
- Is socrates mortal?
While a mortal man should have no difficulty answering “yes” to the above puzzle, SQL queries might have some difficulty.
Here's a formulation of the rules in our system:
(define the-rules '( ((mortal X) (man X)) ((man socrates)) ))
The first rule on the list should be read
as (mortal X)
if (man X)
that is,
“X
is mortal if X
is a man,”
or colloquially “all men are mortal”.
The second rule is just the bare fact “Socrates is a man.”
In response to a query (mortal socrates)
the system
will respond in the affirmative. In response to a query like
(mortal aristotle)
you will just get
Error: no more solutions.
You already know what unification does, so you should
be able to start to see what is happening here.
The system is given the query ((mortal socrates))
so it scans through the-rules
looking only at the
head of each rule, trying
to unify it with the first term in the query, (mortal socrates)
.
It succeeds in unifying it with (mortal X)
.
The result of that unification is an environment where
X
is bound to socrates
.
In the context of that environment, it descends
into the body of the rule, attempting to
prove each component of the body just as if it had been
entered as a direct query, but with the variable parts
substituted for their values. In this case that means
trying to find a rule that matches (man X)
where X=socrates
.
This succeeds matching the fact (man socrates)
and so the entire query succeeds.
What about asking “Who is mortal?”
In response to the query (mortal X)
the head of
each rule is again scanned. But I haven't told you the full story
at this point.
If you remember from Section 17.3.2
we said there might be problems trying to unify two patterns
which happened to contain the same variable names, and for that
reason we implemented instantiate
to replace the variables
in a pattern with others that were equivalent, but guaranteed to be
unique. In fact when the database of rules is scanned, instantiate
is called on each rule before the unification with the head is attempted.
This has no effect on our first example query (mortal socrates)
but it does make a difference for (mortal X)
, because the
X
appears in both the query and the rule.
Thanks to instantiate
, (mortal X)
unifies with the head of a rule that looks like
((mortal ‹0›) (man ‹0›))
.
So the variable X
unifies with the variable
‹0›
rather than itself,
and it is in this environment that
the body of the rule (man ‹0›)
is investigated.
The statement (man ‹0›)
succeeds in unifying
with (man socrates)
, and in the process ‹0›
is bound to socrates
. Now the entire rule has succeeded
and the query succeeds, resulting in an environment where
X=‹0›
and ‹0›=socrates
.
substitute
is given the form (mortal X)
and that
environment, and produces the result (mortal socrates)
.
So let's see how to build this system from our “toolkit”
of unify
, substitute
, instantiate
,
and new-env
.
Before diving into the code, here is a slightly more formal
definition of what we shall be doing.
(‹term_{1}› ...
‹term_{n}›)
So you can see that the body of a rule is treated exactly the same as a top-level query, except that the current environment may contain variables that were instantiated by prior unifications. Therefore our implementation can recurse on the body of a rule, re-using the code that we shall write to process a top-level query. You should also be aware that the environment always accumulates on its way downstream to a solution, only backtracking causes bindings in the accumulating environment to be discarded on the way back upstream.
This is the first time we have really used the PScheme language to implement any serious piece of functionality. I've chosen to do it this way for two reasons. Firstly it emphasises a nice abstraction barrier between our “toolkit” of primitive Perl operations and the PScheme “glue” that binds them into a logic programming system; secondly and perhaps more importantly, it's actually easier to do in PScheme than it would have been in Perl, which I'm honestly quite pleased about. Having said all that, the code may take a little more study if you're not used to reading Scheme programs yet, but it is blissfully short and sweet.
The top-level function, as you have seen
from examples above, is called prove
, and here's its
definition:
(define prove (lambda (goals) (substitute goals (match-goals goals (new-env)))))
prove
is given a list of goals
(statements to be
proved.) It calls another function match-goals
passing
both the goals
and a new empty environment. If match-goals
succeeds, it will return an environment with appropriate variables bound,
and prove
passes that environment along with the original
goals
to substitute
, which replaces variables
in the goals
with their values then returns the result.
If match-goals
fails, control will backtrack through
prove
and we will see Error: no more solutions.
Here's match-goals
:
(define match-goals (lambda (goals env) (if goals (match-goals (cdr goals) (match-goal (car goals) env)) env)))
match-goals
walks its list of goals
, calling another
function match-goal
on each, and collecting the resulting extended
environment. If there are no goals
left to prove, then
match-goal
succeeds and returns the environment it was passed.
Incidentally this means that prove
with an empty list of
goals will always succeed and return its argument environment unchanged.
Here's match-goal
:
(define match-goal (lambda (goal env) (match-goal-to-rule goal (one-of the-rules) env)))
Here is where we start to see amb
coming in to play.
match-goal
uses the one-of
function that
we defined in Section 16.1 to pick one of the list
of rules to try to match against the goal
. It passes
the goal
, the chosen rule, and the environment
to match-goal-to-rule
, which does the
actual unification and recursion.
Here's match-goal-to-rule
:
(define match-goal-to-rule (lambda (goal rule env) (let* ((instantiated-rule (instantiate rule)) (head (car instantiated-rule)) (body (cdr instantiated-rule)) (extended-env (unify (substitute goal env) head env))) (match-goals body extended-env))))
It uses let*
to first create an instantiated
copy of the rule, and then extract the head and the body
from the instantiated-rule
.
Then it calls unify
on the (substituted) goal
and the head of the instantiated rule. If unify
succeeds, then the result is an extended environment that
match-goal-to-rule
uses to recursively
call match-goals
on the body of the rule.
This is the point of recursion discussed above, where
the body of a rule is treated as a new query.
That's all there is to it! Of course what is implicit
in the above code is the backtracking that both unify
and amb
provoke if a unification fails or the
list of rules to try is exhausted. This is most apparent
in match-goal-to-rule
above: if unify
fails, then control simply backtracks out of the function
at that point. Likewise in match-goal
, when
one-of
runs out of options, control backtracks
and match-goal-to-rule
is never called.
There are a couple of refinements we can make howver. We
would like to support require
and is
from
our examples at the start of the chapter^{58}.
Additionally, it would be useful if we could check that the
result returned by prove
does not contain any
unresolved variables. If it does, this should be considered a failure.
For that reason we make use of those two type checking functions
pair?
and var?
to write a little recursive
test called no-vars?
:
(define no-vars? (lambda (expr) (if (pair? expr) (and (no-vars? (car expr)) (no-vars? (cdr expr))) (not (var? expr)))))
We can use that to write a variant of substitite
called substitute-all
that first of all performs
the substitution then requires that the result contains no vars:
(define substitute-all (lambda (expr env) (let ((subst-expr (substitute expr env))) (begin (require (no-vars? subst-expr)) subst-expr))))
If the require
succeeds, then substitute-all
returns the substituted expression just as substitute
does. Otherwise substitute-all
backtracks. We can use this
instead of substitute
in the top-level prove
function:
(define prove (lambda (goals) (substitute-all goals (match-goals goals (new-env)))))
We will find other uses for substitute-all
.
Next up, remember I said
that the system treated (require ‹expr›)
and (‹var› is ‹expr›)
specially.
This is not difficult to achieve. The existing match-goal
just calls match-goal-to-rule
with the current goal,
one-of
the rules, and the current env. All we need to do
is to extend this to first look out for require
and
is
.
(define match-goal (lambda (goal env) (if (eq? (car (cdr goal)) 'is) (match-is goal env) (if (eq? (car goal) 'require) (match-require goal env) (match-goal-to-rule goal (one-of the-rules) env)))))
I've added two new functions match-is
and
match-require
to actually deal with those special
rules. neither of them are particularily complex. match-is
extracts the var and the expression from the rule, then it calls
substitute-all
on the expression. It will therefore
fail and backtrack if the expression contains variables that
have not been bound. This makes sense because the next
thing it does is to pass the expression to eval
(defined
in Section 9.2.3) and it makes no sense for eval
to operate on an expression which contains instantiated pattern
variables (‹0›, ‹1› etc.) that cannot
possibly have values in the normal pscheme environment.
If it gets that far, then match-is
finally unifies
the var term with the substituted and evaluated expression,
returning the new environment:
(define match-is (lambda (goal env) (let* ((var (car goal)) (value (car (cdr (cdr goal)))) (svalue (substitute-all value env))) (unify var (eval svalue) env))))
Note particularily that “is
” is not necessarilty
a test, it is a unification that will fail if the left hand expression
cannot be unified with the right, so it can be considered both an
assertion and potentially an assignment. To be clear
match-is
allows us to deal with statements like:
(N is (+ X Y))
provided X
and Y
are bound.
In this example either N
must already have a numeric
value equal to the sum of X
and Y
,
or it must be unbound, in which case it will recieve that value.
match-require
is quite similar to match-is
.
(define match-require (lambda (goal env) (let ((sgoal (substitute-all goal env))) (begin (eval sgoal) env))))
It too calls substitute-all
, this time on the entire
expression, for the same reasons match-is
did. Then it
passes the whole expression to eval
. If the require
in the substituted goal fails, control will backtrack from that
point as usual.
That concludes our implementation. Let's try it out!
In this section we look at applying logic programming to some “real world” problems, beginning with parsing.
We saw in Section 16.2.4 that amb
by itself
was very useful for parsing because of its built in backtracking
capability. However combining amb
with unification as we have
done here makes parsing an extraordinarily simple task, at least
if we are prepared to accept the accompanying inefficiencies.
Consider the following rules for parsing a set of sentences worked through in the tests from Chapter 16, Listing 32. This is a different set of sentences to those worked through in Section 16.2.4, the sentences in question are:
These are obviously more complex than the sentences we worked through
with amb
, but we can deal with them easily enough here:
(define the-rules (list '((proper-noun (john))) '((proper-noun (paul))) '((noun (car))) '((noun (garage))) '((auxilliary (will))) '((auxilliary (has))) '((verb (put))) '((article (the))) '((article (a))) '((article (his))) '((preposition (in))) '((preposition (to))) '((preposition (with))) '((degree (very))) '((degree (quite))) '((adjective (red))) '((adjective (green))) '((adjective (old))) '((adjective (new))) '((append () Y Y)) '((append (A . X) Y (A . Z)) (append X Y Z)) '((sentence S) (append NP VP S) (noun-phrase NP) (verb-phrase VP)) '((sentence S) (append _X VP S) (append NP AUX _X) (noun-phrase NP) (auxilliary AUX) (verb-phrase VP)) '((noun-phrase NP) (append ART ADJP NP) (article ART) (adj-phrase ADJP)) '((noun-phrase NP) (proper-noun NP)) '((adj-phrase ADJP) (noun ADJP)) '((adj-phrase ADJP) (append DGP ADJP2 ADJP) (degree-phrase DGP) (adj-phrase ADJP2)) '((degree-phrase DGP) (adjective DGP)) '((deg-phrase DGP) (append DEG DGP2 DGP) (degree DEG) (deg-phrase DGP2)) '((verb-phrase VP) (append _X PP VP) (append VB NP _X) (verb VB) (noun-phrase NP) (prep-phrase PP)) '((prep-phrase PP) (append PR NP PP) (preposition PR) (noun-phrase NP))))
This is little more than a declaration of the rules of the grammar. Let's look at a few of those rules a little more closely.
'((adj-phrase ADJP) (noun ADJP)) '((adj-phrase ADJP) (append DGP ADJP2 ADJP) (degree-phrase DGP) (adj-phrase ADJP2))
This rule about adjectival phrases is in two parts. The first part
says that ADJP
is an adj-phrase
if ADJP
is a noun
. The second part says ADJP
is an
adj-phrase
if some DGP
and ADJP2
append to form ADJP
, and DGP
is a
degree-phrase
, and ADJP2
is an adj-phrase
.
'((noun (car))) '((noun (garage)))
This pair of rules defines the nouns we know about. They say
(car)
is a noun
and (garage)
is a noun. The nouns themselves are in lists because the system
deals with lists: consider the adj-phrase
rules above, where ADJP
must be a list for
append
to work on it.
Given the above, we can ask the obvious question:
> (prove '((sentence (john put his car in the garage)))) ((sentence (john put his car in the garage)))
You get the desired response, eventually^{59}. Interestingly, you can also ask it “what is a sentence”:
> (prove '((sentence S))) ((sentence (john put john in the car))) > ? ((sentence (john put john in the garage))) > ? ((sentence (john put john in the red car))) > ? ((sentence (john put john in the red garage))) > ? ((sentence (john put john in the red red car))) > ? ((sentence (john put john in the red red garage))) > ? ((sentence (john put john in the red red red car)))
It gets stuck in a recursive rut after a while, but
it's exciting to see that it has the potential to generate
all sentences of a grammar if it could avoid those
traps^{60}. However that's not the real problem,
the real problem is that it is horribly inefficient. All of
those calls to append
, most of which produce
useless results, consume huge amounts of resources.
However we can take a hint from the way that we implemented
parsing with amb
in Section 16.2.4. In
that implementation, the routine parse-word
removed tokens from the front of the *unparsed*
global, effectively “directing” the progress of the
parse, since it exposed the next token and only certain
words would match that newly exposed token. We can't use
“global variables” in a logic programming
system—the concept has no meaning—but
we can nonetheless keep track of what has been parsed so
far.
We can do this by making all of our grammar rules take a second argument. For example:
(noun-phrase S R)
Will succeed if there is a noun phrase at the start
of S
, and if R
is the remainder
of S
after removing that noun phrase. Perhaps
this approach is most easily demonstrated for individual words.
Here's the new definition of noun
:
'((noun (car . S) S)) '((noun (garage . S) S))
It will match if its first argument is a list
starting with car
or garage
,
an in the process instantiate its second argument
to the remainder of the list. For example:
> (prove '((noun (garage is red) X))) ((noun (garage is red) (is red)))
If we write the other rules for single words similarily, we can start to build up more complex rules on top:
'((noun-phrase S X) (article S S1) (adj-phrase S1 X))
This says that there is a noun phrase at the start of
S
, leaving X
remaining if there is an
article at the start of S
leaving S1
remaining, and an adjectival phrase at the start of S1
,
leaving X
remaining.
Note that we no longer need to use append
to “generate and test”.
We can further build on these
intermediate rules just as with the previous grammar:
'((sentence S X) (noun-phrase S S1) (verb-phrase S1 X))
In order to use this new parser, we must remember to
pass an empty list as the second argument to sentence
,
to ensure that all of the tokens in the first argument are consumed:
> (prove '((sentence (john put his car in the garage) ()))) ((sentence (john put his car in the garage) ()))
Putting all of this together, we can see the considerably faster (but uglier) version in the test at the end of Listing 34.
Ugliness is not just an aesthetic thing, it gets in the way of clear and readable code. For that reason any full Prolog implementation provides rewriting rules that will accept a simple grammar with statements like^{61}:
(sentence --> noun-phrase verb-phrase)
It will transform them into the internal form:
((sentence X0 X1) (noun-phrase X0 X2) (verb-phrase X2 X1))
as it reads them in. I'm not going to do that, since it would require generating symbols etc. but it should be obvious that this sort of transformation is not difficult.
If you remember back in Section 17.1.5
The result of differentiating the expression (((x ^ 2) + x) + 1)
was (((2 * (x ^ 1)) + 1) + 0)
. While correct, this is
somewhat unwieldy as it contains redundant operations such as the
addition of zero. It is relatively easy to write a set of rules
that can automatically simplify such expressions, however we have
to be careful of the order in which we specify the rules.
This is not only a feature of our implementation, the order of
the rules, which is the order in which they will be searched,
is significant in Prolog too.
We start off by saying that we cannot simplify anything unless it has some internal structure:
'((simplify E E) (require (not (pair? 'E))))
So if E
is not a pair, then it will simplify to itself.
We next get to the main driver rule for simplification:
'((simplify (X OP Y) E) (simplify X X1) (simplify Y Y1) (s (X1 OP Y1) E))
This says that we can simplify an expression of the form (X OP Y)
to E
if
X
to X1
;Y
to Y1
;(X1 OP Y1)
to E
using the auxilliary simplification
rules (s (‹E1› ‹OP› ‹E2›) ‹E3›)
.These auxilliary simplification rules occupy the rest of the definition of simplification. Firstly here are the rules for addition:
'((s (X + 0) X)) '((s (0 + X) X)) '((s (X + Y) Z) (require (and (number? 'X) (number? 'Y))) (Z is (+ X Y))) '((s (X + Y) (X + Y)))
The first rule says that X
plus zero is just X
. The second rule
is a necessary repetition of the first, reversing 0
and X
.
The third rule says that we can simplify (X + Y)
to Z
if X
and Y
are both numbers, by making Z
equal to their sum.
The last rule is there in case the term can not be simplified, in which case the
result is just the original.
The rules for simplifying multiplication are very similar, except that we can simplify both multiplication by zero and multiplication by one:
'((s (X * 0) 0)) '((s (0 * X) 0)) '((s (X * 1) X)) '((s (1 * X) X)) '((s (X * Y) Z) (require (and (number? 'X) (number? 'Y))) (Z is (* X Y))) '((s (X * Y) (X * Y)))
Likewise for exponentiation, except that we don't have a “^
” operator
in PScheme so we can't perform any actual numeric computation in this case:
'((s (X ^ 0) 1)) '((s (X ^ 1) X)) '((s (X ^ Y) (X ^ Y)))))
With these rules in place we can ask the system to simplify that unwieldy expression we saw before:
> (prove '((simplify (((2 * (x ^ 1)) + 1) + 0) X))) ((simplify (((2 * (x ^ 1)) + 1) + 0) ((2 * x) + 1)))
Note that these rules for simplification are very incomplete, most noticeably they do not deal with subtraction or division. However they are sufficient to demonstrate that they work and you can add the extra rules yourself if you want to extend or experiment (this example is part of the tests in Listing 34.)
cuts
While we've spent some time exploring the potential of logic programming, it would be wrong of me to suggest that PScheme offers anything like the power of a real Prolog system. In fact it is missing some fairly fundamental features, and differs from real Prolog quite significantly. If you're excited by what you've seen here I'd suggest you get acquainted with a real Prolog system: I've barely scratched the surface. You may be surprised to know that Prolog itself is commonly used to build compilers for even higher-level languages and, much like Scheme, it is relatively easy to define a meta-circular evaluator for Prolog in Prolog. I'm not going to go anywhere near that, this is getting silly enough as it is. Rather, In this section I'd like to discuss the shortcomings of this implementation by comparing it with a real Prolog.
In Prolog, facts and rules are not defined as simple lists. Prolog distinguishes between the functor of a rule and its arguments. For example the PScheme “fact”:
((mary likes cheese))
would be written in Prolog as:
likes(mary, cheese).
and the rule:
((likes mary X) (person X) (X likes chips))
would be written as:
likes(mary, X) :- person(X), likes(X, chips).
In this example likes
is called the functor
of the rule. Because it takes two arguments, it is said to have an
arity of 2, and is classified as likes/2
. This is
distinct from any likes
functor with a different number of
arguments, Just as in our implementation lists of different length
cannot match.
The big advantage in distinguishing functor/arity like this is that
Prolog can index its database on this basis. Unification is expensive,
so when searching for a rule to match i.e. likes(mary, X)
Prolog need only inspect rules that are likes/2
.
Of course this means that the functor cannot be matched by a pattern variable. The expression:
X(mary, wine)
is not valid Prolog. However Prolog has mechanisms to extract the functor from a term as a variable, and to call an expression constructed with a variable functor, so this apparent limitation can be worked around.
Prolog also recognises operators and operator precedence, such that the normal mathematical operators are infix and are parsed with the correct precedence and associativity. Prolog operators are functors, so for example the form:
a + b * c
is equivalent to:
+(a, *(b, c))
Prolog also allows you to define new operators as any sequence of non-alphanumeric characters, and assign them a precedence and associativity. These user defined operators don't actually do anything: they just make it easier to write Prolog terms as they translate internally to normal functors just as the built-in operators do.
Another reason that Prolog distinguishes its functors is to allow short circuiting
of the search space. Prolog provides a special rule called the cut
to accomplish this [pip pp69–92]. The cut is written with a single
exclaimation mark “!
”.
As part of the body of a rule, the cut always succeeds. But if it is backtracked through,
it backtracks all the way past the point where the head of the rule was unified, and
past the point where rules of that functor/arity were considered, back to the
decision point before that. This is extremely useful behaviour.
For example, returning to our simplify
example of algebraic simplification
from Section 17.5.2, our very first rule was:
'((simplify E E) (require (not (pair? 'E))))
This was saying that you can simplify E
to E
if E
is not a pair (is atomic.) We might translate this into Prolog as:
simplify(E, E) :- atomic(E).
However this is better expressed in Prolog as:
simplify(E, E) :- atomic(E), !.
This says that if this rule succeeds, then no other simplify/2
rules should be
considered if backtracking occurs through the cut. If the expression E
is atomic,
then it cannot be simplified, end of story.
There are other uses of the cut, but they are best described in a book on Prolog.
In order to properly implement the cut, we would have to pass a third
cut{}
continuation around, which makes the Parameter Object pattern
discussed in Section 16.5.1 even more attractive.
As I've already mentioned in Section 16.5, the chronological backtracking
exhibited by amb
is hopelessly inefficient, and an alternative
dependancy-directed
backtracking is preferable. This kind of backtracking examines the cause of any
failure, and backtracks immediately to the point of execution that most recently affected
the failure. Dependancy directed backtracking is often implemented by a constraint
network, which allows the backtracking to proceed directly to the last place that
the value in question was altered. Again this is beyond the scope of this
book^{62}.
The first set of tests in Listing 33 exercise the individual additions to this version of the interpreter.
The first test proves that unify
elicits backtracking
on failure.
The second test proves that unify
returns a PScm::Env on success.
the third test demonstrates that unify
plus
substitute
can resolve the variable terms in an example
that we've seen before.
The last test in this file shows instantiate
in
action. Although the digits in the result look like numbers,
they are actually PScm::Expr::Vars
t/PScm_Unify.t
1 use strict; 2 use warnings; 3 use Test::More; 4 use lib './t/lib'; 5 use PScm::Test tests => 5; 6 7 BEGIN { use_ok('PScm') } 8 9 eval_ok(<<'EOT', <<'EOR', 'simple unify'); 10 (unify '(a b c) '(a b d)) 11 EOT 12 Error: no more solutions 13 EOR 14 15 eval_ok(<<'EOT', <<'EOR', 'simple unify 2'); 16 (unify '(a b c) '(a b c)) 17 EOT 18 PScm::Env 19 EOR 20 21 eval_ok(<<'EOT', <<'EOR', 'unify and substitute'); 22 (substitute 23 '((a A) (b B)) 24 (unify '(f (g A) A) 25 '(f B abc))) 26 EOT 27 ((a abc) (b (g abc))) 28 EOR 29 30 eval_ok(<<'EOT', <<'EOR', 'instantiate'); 31 (instantiate '((f (g A) A) (f B abc))) 32 EOT 33 ((f (g 0) 0) (f 1 abc)) 34 EOR 35 36 # vim: ft=perl
The second set of tests in Listing 34 tries out our logic programming system. It works through pretty much the examples we've already covered in this chapter.
t/AMB_Unify.t
1 use strict; 2 use warnings; 3 use Test::More; 4 use lib './t/lib'; 5 use PScm::Test tests => 13; 6 7 BEGIN { use_ok('PScm') } 8 9 my $prereqs = <<EOT; 10 11 (define not 12 (lambda (x) 13 (if x 0 1))) 14 15 (define require 16 (lambda (x) 17 (if x x (amb)))) 18 19 (define one-of 20 (lambda (lst) 21 (begin 22 (require lst) 23 (amb (car lst) (one-of (cdr lst)))))) 24 25 (define no-vars? 26 (lambda (expr) 27 (if (pair? expr) 28 (and (no-vars? (car expr)) 29 (no-vars? (cdr expr))) 30 (not (var? expr))))) 31 32 (define substitute-all 33 (lambda (expr env) 34 (let ((subst-expr (substitute expr env))) 35 (begin 36 (require (no-vars? subst-expr)) 37 subst-expr)))) 38 39 (define prove 40 (lambda (goals) 41 (substitute-all goals 42 (match-goals goals 43 (new-env))))) 44 45 (define match-goals 46 (lambda (goals env) 47 (if goals 48 (match-goals (cdr goals) 49 (match-goal (car goals) 50 env)) 51 env))) 52 53 (define match-goal 54 (lambda (goal env) 55 (if (eq? (car (cdr goal)) 'is) 56 (match-is goal env) 57 (if (eq? (car goal) 'require) 58 (match-require goal env) 59 (match-goal-to-rule goal 60 (one-of the-rules) 61 env))))) 62 63 (define match-is 64 (lambda (goal env) 65 (let* ((var (car goal)) 66 (value (car (cdr (cdr goal)))) 67 (svalue (substitute-all value env))) 68 (unify var (eval svalue) env)))) 69 70 (define match-require 71 (lambda (goal env) 72 (let ((sgoal (substitute-all goal env))) 73 (begin 74 (eval sgoal) 75 env)))) 76 77 (define match-goal-to-rule 78 (lambda (goal rule env) 79 (let* ((instantiated-rule (instantiate rule)) 80 (head (car instantiated-rule)) 81 (body (cdr instantiated-rule)) 82 (extended-env (unify (substitute goal env) 83 head 84 env))) 85 (match-goals body extended-env)))) 86 EOT 87 88 my $prereqs_output = <<EOT; 89 not 90 require 91 one-of 92 no-vars? 93 substitute-all 94 prove 95 match-goals 96 match-goal 97 match-is 98 match-require 99 match-goal-to-rule 100 EOT 101 102 $prereqs_output =~ s/\n$//s; 103 104 105 eval_ok(<<EOT, <<EOR, 'socrates'); 106 $prereqs 107 (define the-rules 108 (list '((man socrates)) 109 '((mortal X) (man X)))) 110 (prove '((mortal socrates))) 111 EOT 112 $prereqs_output 113 the-rules 114 ((mortal socrates)) 115 EOR 116 117 my $rules = <<'EOT'; 118 (define the-rules 119 (list '((mary likes cheese)) 120 '((mary likes wine)) 121 '((john likes beer)) 122 '((john likes wine)) 123 '((john likes chips)) 124 '((person mary)) 125 '((person john)) 126 '((mary likes X) (person X) 127 (require (not (eq? 'X 'mary))) 128 (X likes Y) 129 (mary likes Y)))) 130 EOT 131 132 eval_ok(<<EOT, <<EOR, 'mary and john [1]'); 133 $prereqs 134 $rules 135 (prove '((mary likes john))) 136 EOT 137 $prereqs_output 138 the-rules 139 ((mary likes john)) 140 EOR 141 142 eval_ok(<<EOT, <<EOR, 'mary and john [2]'); 143 $prereqs 144 $rules 145 (prove '((mary likes X))) 146 ? 147 ? 148 ? 149 EOT 150 $prereqs_output 151 the-rules 152 ((mary likes cheese)) 153 ((mary likes wine)) 154 ((mary likes john)) 155 Error: no more solutions 156 EOR 157 158 $rules = <<'EOT'; 159 (define the-rules 160 (list '((append () Y Y)) 161 '((append (A . X) Y (A . Z)) (append X Y Z)))) 162 EOT 163 164 eval_ok(<<EOT, <<EOR, 'append [1]'); 165 $prereqs 166 $rules 167 (prove '((append (a b) (c d) X))) 168 EOT 169 $prereqs_output 170 the-rules 171 ((append (a b) (c d) (a b c d))) 172 EOR 173 174 eval_ok(<<EOT, <<EOR, 'append [2]'); 175 $prereqs 176 $rules 177 (prove '((append X Y (a b c d)))) 178 ? 179 ? 180 ? 181 ? 182 ? 183 EOT 184 $prereqs_output 185 the-rules 186 ((append () (a b c d) (a b c d))) 187 ((append (a) (b c d) (a b c d))) 188 ((append (a b) (c d) (a b c d))) 189 ((append (a b c) (d) (a b c d))) 190 ((append (a b c d) () (a b c d))) 191 Error: no more solutions 192 EOR 193 194 eval_ok(<<EOT, <<EOR, 'symbolic differentiation'); 195 $prereqs 196 (define the-rules 197 (list '((derivative X X 1)) 198 '((derivative N X 0) (require (number? 'N))) 199 '((derivative (X ^ N) X (N * (X ^ P))) (P is (- N 1))) 200 '((derivative (log X) X (1 / X))) 201 '((derivative (F + G) X (DF + DG)) 202 (derivative F X DF) 203 (derivative G X DG)) 204 '((derivative (F - G) X (DF - DG)) 205 (derivative F X DF) 206 (derivative G X DG)) 207 '((derivative (F * G) X ((F * DG) + (G * DF))) 208 (derivative F X DF) 209 (derivative G X DG)) 210 '((derivative (1 / F) X ((- DF) / (F * F))) 211 (derivative F X DF)) 212 '((derivative (F / G) X (((G * DF) - (F * DG)) / (G * G))) 213 (derivative F X DF) 214 (derivative G X DG)))) 215 216 (prove '((derivative (((x ^ 2) + x) + 1) x X))) 217 EOT 218 $prereqs_output 219 the-rules 220 ((derivative (((x ^ 2) + x) + 1) x (((2 * (x ^ 1)) + 1) + 0))) 221 EOR 222 223 $rules = <<EOF; 224 (define the-rules 225 (list '((add X Y Z) (Z is (+ X Y))) 226 '((add X Y Z) (X is (- Z Y))) 227 '((add X Y Z) (Y is (- Z X))))) 228 EOF 229 230 eval_ok(<<EOF, <<EOR, 'builtin arithmetic'); 231 $prereqs 232 $rules 233 (prove '((add 2 3 X))) 234 (prove '((add 2 X 5))) 235 (prove '((add X 3 5))) 236 EOF 237 $prereqs_output 238 the-rules 239 ((add 2 3 5)) 240 ((add 2 3 5)) 241 ((add 2 3 5)) 242 EOR 243 244 $rules = <<EOF; 245 (define the-rules 246 (list '(((johann ambrosius) father-of (j s))) 247 '(((j c friedrich) father-of (w f ernst))) 248 '(((j s) (anna magdalena) parents-of (j c friedrich))) 249 '(((j s) (anna magdalena) parents-of (johann christian))) 250 '(((j s) (maria barbara) parents-of (wilhelm friedmann))) 251 '(((j s) (maria barbara) parents-of (c p e))) 252 '((X father-of Y) (X _ parents-of Y)) 253 '((X mother-of Y) (_ X parents-of Y)) 254 '((X parent-of Y) (X father-of Y)) 255 '((X parent-of Y) (X mother-of Y)) 256 '((X ancestor-of Y) (X parent-of Y)) 257 '((X ancestor-of Z) (X parent-of Y) (Y ancestor-of Z)))) 258 EOF 259 260 # had to truncate this test - takes too long to run 261 eval_ok(<<EOF, <<EOR, 'genealogy'); 262 $prereqs 263 $rules 264 (prove '((X ancestor-of (w f ernst)))) 265 EOF 266 $prereqs_output 267 the-rules 268 (((j c friedrich) ancestor-of (w f ernst))) 269 EOR 270 271 $rules = <<EOF; 272 (define the-rules 273 (list 274 '((proper-noun (john . S) S)) 275 '((proper-noun (paul . S) S)) 276 '((noun (car . S) S)) 277 '((noun (garage . S) S)) 278 '((auxilliary (will . S) S)) 279 '((auxilliary (has . S) S)) 280 '((verb (put . S) S)) 281 '((article (the . S) S)) 282 '((article (a . S) S)) 283 '((article (his . S) S)) 284 '((preposition (in . S) S)) 285 '((preposition (to . S) S)) 286 '((preposition (with . S) S)) 287 '((degree (very . S) S)) 288 '((degree (quite . S) S)) 289 '((adjective (red . S) S)) 290 '((adjective (green . S) S)) 291 '((adjective (old . S) S)) 292 '((adjective (new . S) S)) 293 '((sentance S X) 294 (noun-phrase S S1) (verb-phrase S1 X)) 295 '((sentance S X) 296 (noun-phrase S S1) (auxilliary S1 S2) (verb-phrase S2 X)) 297 '((noun-phrase S X) 298 (article S S1) (adj-phrase S1 X)) 299 '((noun-phrase S X) (proper-noun S X)) 300 '((adj-phrase S X) (noun S X)) 301 '((adj-phrase S X) 302 (degree-phrase S S1) (adj-phrase S1 X)) 303 '((degree-phrase S X) (adjective S X)) 304 '((deg-phrase S X) 305 (degree S S1) (deg-phrase S1 X)) 306 '((verb-phrase S X) 307 (verb S S1) (noun-phrase S1 S2) (prep-phrase S2 X)) 308 '((prep-phrase S X) 309 (preposition S S1) (noun-phrase S1 X)) 310 311 )) 312 EOF 313 314 eval_ok(<<EOF, <<EOT, 'parsing'); 315 $prereqs 316 $rules 317 (prove '((sentance (john will put his car in the garage) ()))) 318 EOF 319 $prereqs_output 320 the-rules 321 ((sentance (john will put his car in the garage) ())) 322 EOT 323 324 $rules = <<EOF; 325 (define the-rules 326 (list 327 '((simplify E E) (require (not (pair? 'E)))) 328 '((simplify (X OP Y) E) 329 (simplify X X1) 330 (simplify Y Y1) 331 (s (X1 OP Y1) E)) 332 '((s (X + 0) X)) 333 '((s (0 + X) X)) 334 '((s (X + Y) Z) 335 (require (and (number? 'X) (number? 'Y))) 336 (Z is (+ X Y))) 337 '((s (X + Y) (X + Y))) 338 '((s (X * 0) 0)) 339 '((s (0 * X) 0)) 340 '((s (X * 1) X)) 341 '((s (1 * X) X)) 342 '((s (X * Y) Z) 343 (require (and (number? 'X) (number? 'Y))) 344 (Z is (* X Y))) 345 '((s (X * Y) (X * Y))) 346 '((s (X ^ 0) 1)) 347 '((s (X ^ 1) X)) 348 '((s (X ^ Y) (X ^ Y))))) 349 EOF 350 351 eval_ok(<<EOF, <<EOT, 'simplification'); 352 $prereqs 353 $rules 354 (prove '((simplify (((2 * (x ^ 1)) + 1) + 0) X))) 355 EOF 356 $prereqs_output 357 the-rules 358 ((simplify (((2 * (x ^ 1)) + 1) + 0) ((2 * x) + 1))) 359 EOT 360 361 $rules = <<EOR; 362 (define the-rules 363 (list 364 '((factorial 0 1)) 365 '((factorial N X) (T is (- N 1)) (factorial T U) (X is (* N U))))) 366 EOR 367 368 eval_ok(<<EOF, <<EOT, 'recursion'); 369 $prereqs 370 $rules 371 (prove '((factorial 10 X))) 372 EOF 373 $prereqs_output 374 the-rules 375 ((factorial 10 3628800)) 376 EOT 377 378 eval_ok(<<EOF, <<EOT, 'factorial not bidirectional'); 379 $prereqs 380 $rules 381 (prove '((factorial X 3628800))) 382 EOF 383 $prereqs_output 384 the-rules 385 Error: no more solutions 386 EOT 387 388 # vim: ft=perl
Full source code for this version of the interpreter is available athttp://billhails.net/Book/releases/PScm-0.1.13.tgz
Of
course you can define it even more easily in Perl as
(@a, @b)
but that's only because Perl already has an
append operation, and so does any complete scheme implementation.
A real Scheme implementation is case-insensitive, so does not have this luxury. PScheme is case-sensitive which allows us to follow the convention of the logic programming language Prolog, where capital letters introduce pattern variables.
We use match()
here only because it is convenient: neither the value
of the variable nor the structure will contain variables,
so match()
is being used as a recursive equality test
(like eq?
.)
In fact
it is quite possible to retrieve bindings of one variable directly
to another, like {A => 'B'}
in other circumstances, for
example if 'B'
did not have a value when it was unified
with 'A'
.
We could have further subclassed PScm::Expr::Var and had the
reader recognize underscores as this type, but is_anon()
is
the only method that would then need to be specialized to this
type.
(requre
‹expression›)
fails if ‹expression›
is false, and (‹expr_{1}› is
‹expr_{2}›)
fails if ‹expr_{1}›
does not equal ‹expr_{2}›, in both cases
after variable substitution and evaluation.
it took over ten seconds on my computer.
One way to avoid recursive traps would be
to randomize the order in which one-of
returns
its values. Unfortunately that will cause other problems
in general.
When I say “like”, I'm not suggesting that Prolog looks exactly like this, it's actual syntax is somewhat different. I'm only saying these are conceptually alike.
i.e. I don't know how to make it work yet.