>> Heh. You wanna know how it works? ;-)
> 
> Well, I read the message you wrote, and that seemed to cover a fair bit 
> of it.  But sure, I'd be interested in more details....

OK, well, I'm sure once I've posted this Darren will tell me I've done 
it all wrong, but hey. :-)

[As should be superbly obvious, I got all the techniques out of a book. 
Obviously I'm not this intelligent on my own. All the code, however, I 
wrote myself...]

The idea is that you can write "expressions". An expression can be a 
number, a variable, or a list of subexpressions. And you can write 
"predicates", and ask the system whether it is *possible* to satisfy a 
given predicate, and if so, what variable assignments you need to make 
to do so.

The basic predicate is equality. E.g., given [1, y, 3] and [x, 2, z], is 
there any set of variable assignments that you can construct that can 
make these two expressions be "the same"?

Well, actually yes, there is. If you do x=1, y=2, z=3, then the first 
expression becomes [1, 2, 3] and the second one becomes [1, 2, 3] - 
which is clearly the same expression.

The algorithm for figuring this out is apparently called "unification". 
You start with an empty table of values, and you compare the two 
expressions against each other.

If you've got a pair of numbers, then they're either equal or they 
aren't. If they're equal, unification succeeds. If they aren't equal, 
unification fails. (I.e., the two expressions [obviously] cannot be made 
equal.)

If you've got a thing and a variable, the obvious way to proceed is to 
set the variable to that value. The catch is that you need to check that 
the expression you're setting the variable to doesn't contain the 
variable in question; otherwise you might end up with something like 
settings x = [1,2,x], which doesn't make sense. Also, check that what 
you're setting doesn't contradict an existing setting for that variable. 
(E.g., you can't have x = 1 and x = 2 at the same time!)

And finally, if you're comparing a list, the thing you're comparing it 
to had better be a list, of the same size, and unify its elements one by 
one.

So that's unification, and that's how you check whether two expressions 
are or can be made equal. [Incidentally, this is apparently the 
algorithm Haskell uses for automatically determining what type 
signitures your program should have. Each item has a type, which might 
be a specific type like "Integer", or something involving a type 
variable, and the compiler needs to check it's possible to unify 
everything and determine the most general types, etc.]

Now we get to the amusing part. Suppose we want to have AND and OR 
predicates. How do you do that? Well, it immediately becomes apparent 
that if you're going to do that, you might get more than one answer. So 
let's deal with *lists* of answers. So a predicate, when you run it, 
returns a list of answers, and each such "answer" is a set of variable 
bindings. OK, good.

Implementing OR is spectacularly easy. You run the left predicate and 
gather up its answer list. Then you run the right predicate and gather 
up its answer list. And then you JOIN THE TWO LISTS TOGETHER. That's it. 
That's all there is to it!

Implementing AND is very slightly harder. What you do is you run the 
left predicate. And then, for each answer in its answer list, you run 
the right predicate, STARTING FROM THAT ANSWER. So if one answer says 
that x = 7, you run the right predicate assuming that we already know 
that x = 7. (Notice that if the left predicate yields 8 answers, we run 
the right predicate 8 times over. We take the list of answers from each 
run, and JOIN them all together into one giant final list.)

That's our basic predicates - equals, AND, OR. NOT isn't hard to add. 
But we still don't have enough to implement the join() predicate. That 
requires "local variables". And so there's a predicate for generating 
those. It's called "exists".

The idea is that you can write

   exists t: x = [t, 5] AND y = [t, 6]

The exists predicate is satisfied if it's possible to pick a value for t 
that makes the rest of the predicate true. In this case, that basically 
means that the predicate succeeds if x and y are 2-element lists that 
both begin with the same element, and end with 5 and 6 respectively.

Implementing exists in Haskell requires a small amount of trickery, but 
it's not essentially "hard". It just conjurs up a new variable with a 
guaranteed unique name. (Unique so it won't clash with anything else.) 
It then takes a function that accepts a variable name and returns a 
predicate as a result.

NOW we can implement join:

   JOIN(X,Y,Z) is true if X is an empty list and Y = Z, OR X is T 
followed by A, Z is T followed by B, and JOIN(A, Y, B) is true.

Or, in symbols:

   join(x, y, z) =
     x = [] AND y = Z    OR
     exists t, a, b: x = t:a AND z = t:b AND join(a,y,b)

QED, baby! :-D

Now, if only I could make it so you don't have to write a Haskell 
program every time you want to execute a logic predicate, I'd get round 
to doing stuff like the example where you define who's related to who, 
and then you can ask the computer whether somebody is or isn't a direct 
descendent of somebody else. [But without actually implementing the 
inferance algorithm yourself.] Neat stuff...

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message