(OT) Pushing inductive systems to their limit

[Ovid]

This is an expansion of something in my use.perl journal where I explained how logic programming works. What follows is a brief and over-simplified overview of what lies at the core of automated deduction and logical inference systems the world over. In short, it's at the heart of many AI projects. Even though it's one programming paradigm that's not natively supported by Perl, it's surprisingly simple.

If the following interests you, check out AI::Prolog, Logic or Language::Prolog::Yaswi. If you'll be at OSCON, I'll be talking about the first module.

I was looking at Luke Palmer's Logic module on the CPAN and it got me to thinking a bit about logic programming in general, as opposed to the specific implementation of Prolog I've been focusing on. To implement logic programming, you basically have to implement two things, backtracking and unification.

You already understand backtracking from regular expressions. If you fail to find a match (in our case, if we fail to unify two data structures), back up to the last point in the string (stack) where we can make a different decision and try again. It's pretty straightforward.

Unification is also fairly simple. You know it from makefiles or SQL, but we'll look at logic programming in particular. Imagine that you have two five element lists:

( 1, 2, undef, undef,     5 )
( 1, 2,     3,     4, undef )

Imagine that undef means "unknown". We can unify those two lists because every element that is known corresponds in the two lists. This leaves us with a list of the integers one through five.

( 1, 2, 3, 4, 5 )

However, what happens if the last element of the first list is unknown?

( 1, 2, undef, undef, undef )
( 1, 2,     3,     4, undef )

We can still unify the two lists. In this case, we get the same five element list, but the last item is unknown.

( 1, 2, 3, 4, unknown )

Logic programming works by pushing these lists onto a stack and walking through the stack and seeing if you can unify everything (sort of). But how to unify from one item to the next? We assign names to the unknown variables and see if we can unify them. When we get to the next item in the stack, we check to see if any named variables have been unified. If so, we unify the individual variables prior to trying to unify items with their counterparts in our lists.

Thats a bad explanation, so here's how it works. Imagine the following "knowledge base" of lists:

(parent, sally, tom)
(parent, bill, tom)
(parent, tom, sue)
(parent, alice, sue)
(parent, sarah, tim)

(male, bill)
(male, tom)
(male, tim)

Now let's assume we have a rule which states that someone is a father if they are a parent and they are male. Maybe we'd define it something like this (imagine that the angle brackets mean "read this and say 'if'"):

(
  <father, $person>,
  (parent, $person, $anyone),
  (male, $person)
)

Taking the first term in the rule, the logic engine might try to unify this with the first fact in the knowledge base, "(parent, sally, tom)". $person unifies with "sally" and $anyone unifies with "tom". We then push this information onto a stack. If subsequent facts fail to unify and we come back here, because there are still more facts we can try, we set a "choice point" in the stack telling us which fact we last tried. If we come back and see a choice point, we move on to the next fact and try again.

Moving on to the next term in the rule, "(male, $person)", we know that "sally" is unified to $person, so we now try to unify "(male, sally)" with all of the corresponding rules in the knowledge base. Since we can't, the logic engine backs up to the last item where we could make a new choice and sees "(parent, bill, tom)". $person gets unified with "bill" and $anyone gets unified with "tom". Then in moving to the next rule we see that we unify with "(male, bill)". Now, we check the first item in the rule and see that it's "(father, $person)" and the logic engine reports that "bill" is a father.

Note that we can then force the engine to backtrack and by continuously following this procedure, we can determine who all of the fathers are. ($anyone is ignored and in Prolog, it's marked with an underscore: "_". This means that it's an anonymous variable whose value we really don't care about.)

And that's how logic programming works. Simple, eh? (well, individual items can be lists or other rules, but you get the idea).

Getting back to Perl (and Prolog), the above can be implemented in AI::Prolog like so:

#!/usr/bin/perl
use strict;
use warnings;
use AI::Prolog;

my $prolog = AI::Prolog->new(<<END_PROLOG);
parent(sally, tom).
parent(bill, tom).
parent(tom, sue).
parent(alice, sue).
parent(sarah, tim).

male(bill).
male(tom).
male(tim).

father(Person) :-
    parent(Person, _),
    male(Person).
END_PROLOG

$prolog->query('father(Whom)');
while (my $results = $prolog->results) {
    print "@$results\n";
}
__END__
father bill
father tom

(Note: see also Bringing Logic Programming to Perl for some code with an older version of this module)

Now that's all well and good, but Luke Palmer's code has me thinking a bit. Generally we're unifying lists. What if we try to unify arbitrary data structures? What if we also want to unify hashes, or typeglobs or URI objects? What should happen if I tried to unify a regular expression against a string?

In other words, I'm seriously interested in an entirely separate module which allows robust unification of perl data structures. Consider how unification works. First, if a particular item has a value we say it is "bound" to that value. We can then unify two items if they fall under one of the following three conditions:

1. They are both bound to the same value ("bob" and "bob").
2. The are both unbound (unknown and unknown).
3. One is bound and the other is not ("bob" and "unknown").

(There's something else called an "occurs check", but that's beyond the scope of this meditation)

So what happens if we add a fourth condition: one item is bound and another item is "conditionally bound". If one item is "bob" and the second item is qr/[[:alpha:]]/, then both terms could be bound to "bob". If one item is the HTML of a Web page and the second item is a URI object, they could be bound to the HTML if the entity body of the URI matches the HTML. So for each type of "conditionally bound" object, we'd have to specify unification criteria. Imagine a Number::Prime object which only unifies with prime numbers. This could simplify quite a bit of logic code.

The main problem that I see is what happens when one tries to unify two conditionally bound objects? Should a junction be the result? Should the unification fail because we have nothing real to bind to? Should they only be allowed to unify iff they are identical? Is there any merit to this idea at all?

Update: Fixed typo that AReed pointed out.