|
 |
>> 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
|
|
null> wrote: