|
 |
So what does this look like when implemented in Haskell?
> module Logic where
Well, the program basically takes a predicate, and returns an
answer which says either:
- The predicate cannot be satisfied.
- The predicate can be satisfied, and this set of variable
bindings satisfies is.
We can store the variable bindings in a key/value dictionary.
To do that, let's import the requisit Haskell module:
> import qualified Data.Map
Now let's define a variable bindinds table type:
> type Table = Data.Map.Map Var Expression
> empty_table = Data.Map.empty
As I say, an "answer" is either a "no" or a "yes, and here's
the bindings". In Haskell, we can use the pre-defined "Maybe"
type for this.
> type Answer = Maybe Table
Now let's define what an "expression" is. Let's say that an
expression can be a number, a variable, or a list. (I'll
define lists recursively so that predicates can recurse
over them.)
> data Expression =
> Number Integer |
> Variable Var |
> ListNode Expression Expression |
> ListEndNode
> deriving (Eq, Show)
I'm going to have two types of variable - named ones that the
programmer creates, and numbered ones that are auto-generated
by the "exists" predicate later on:
> data Var = Named String | Numbered Integer deriving (Eq, Ord, Show)
Let's continue now by defining the unification algorithm.
Remember, unification takes two expressions and determins
whether it is possible to make them the same by setting
some variable bindings. We start with an empty bindings
table, and proceed by adding new bindings.
> unify :: Table -> Expression -> Expression -> Answer
Firstly, let's apply the current set of bindings to the
two input expressions before proceeding. This ensures that
any variables already bound are eliminated from the
expressions.
> unify t e0 e1 = case (apply t e0, apply t e1) of
Now we take the possibilities case by case. For example,
if we have to unify a number against a number, we check
whether the numbers are equal. If they're not, unification
fails. If they are, unification suceeds (and the table
remains unchanged).
> (Number x, Number y) -> if x == y then Just t else Nothing
A variable matches anything. Well no, not quite. A variable
matches any expression not containing that variable. (E.g.,
you can't unify x = 2*x.) Assuming that condition holds, just
add the binding to the table.
> (Variable x, e) -> if e `contains` x
> then Nothing
> else Just (bind t x e)
> (e, Variable x) -> if e `contains` x
> then Nothing
> else Just (bind t x e)
Lists are slightly more tricky. Obviously an empty list
matches an empty list
> (ListEndNode, ListEndNode) -> Just t
For a non-empty list, we want to unify the list heads,
and then (using the binding table) continue unifying the
list tails. Oh, but if the first part fails, skip
the second part...
Fortunately, Haskell's much-feared "monad" concept implements
exactly this behaviour:
> (ListNode x xs, ListNode y ys) -> do
> t' <- unify t x y
> unify t' xs ys
That is, unify x against y using table t, thus generating a
new table t'. Then unify xs against ys using t' as the table
(thus generating a new table, which is the final result).
Oh, and finally, any combination that doesn't match one of
the above patterns (e.g., unify a number against a list)
causes unification to fail:
> (_, _) -> Nothing
Now we just need to implement that "apply" function:
> apply :: Table -> Expression -> Expression
> apply t (Variable v) = case Data.Map.lookup v t of
> Nothing -> Variable v
> Just e -> e
> apply t (ListNode x xs) = ListNode (apply t x) (apply t xs)
> apply t e = e
And also the "contains" function:
> contains :: Expression -> Var -> Bool
> (Variable v) `contains` v0 = v == v0
> (ListNode x xs) `contains` v0 = x `contains` v0 || xs `contains` v0
> _ `contains` v0 = False
Finally, the "bind" function. In principle this just inserts
a binding into the table - but actually I've made it rescan all
the existing bound expressions and apply any applicable expansions
to them as well to eliminate intermediate temporary variables.
> bind :: Table -> Var -> Expression -> Table
> bind t v e = Data.Map.map (apply t) (Data.Map.insert v e t)
Now we have unification. You can try out an example such as
unify
empty_table
(ListNode (Number 1) (ListNode (Number 2) ListEndNode)
(ListNode (Variable (Named "x")) (ListNode (Number 2) ListEndNode)
which yields the result
Just (fromList [(Named "x",Number 1)]
In other words, "[1,2]" unified against "[x,2]" yields "x=1".
We can implement this as a predicate. But first we need to decide
what a "predicate" actually is. In my implementation, a predicate
is a function that takes a current bindings table and returns
a list of all possible bindings tables (starting from the given
one) that satisfy the predicate:
> type State = (Table,Integer)
> type Predicate = State -> [State]
What the heck is that integer there for? Well, it's used by
"exists", as we'll see a bit later. Let's now write a "run"
function:
> run_pred :: Predicate -> [State]
> run_pred p = p (empty_table, 1)
Anyway, the equality predicate is quite easy:
> pred_equals :: Expression -> Expression -> Predicate
> pred_equals x y (t,n) = case unify t x y of
> Nothing -> []
> Just t' -> [(t',n)]
If unification fails, return an empty list. If unification
succeeds, return a 1-element list containing the new
bindings table.
Implementing an OR predicate is similarly simple:
> pred_OR :: Predicate -> Predicate -> Predicate
> pred_OR p1 p2 (t,n) = p1 (t,n) ++ p2 (t,n)
In other words, run the first predicate, run the second
predicate, and then just JOIN the two answer lists thus
produced!
Implementing AND is moderately harder. We want to run the
first predicate, and then for EVERY result produced, run
the second predicate starting from that answer. Once again,
Haskell's monad structure leaps to the rescue:
> pred_AND :: Predicate -> Predicate -> Predicate
> pred_AND p1 p2 s0 = return s0 >>= p1 >>= p2
And finally, the "exists" predicate. It takes a function
that accepts a temp variable and returns a predicate.
> pred_exists :: (Expression -> Predicate) -> Predicate
> pred_exists fn (t,n) = (fn (Variable (Numbered n))) (t,n+1)
Now, to prove all this works, let's have that "join"
predicate:
> pred_join :: Expression -> Expression -> Expression -> Predicate
> pred_join xs ys zs =
> (
> (xs `pred_equals` ListEndNode) `pred_AND`
> (ys `pred_equals` zs)
> )
> `pred_OR`
> (
> pred_exists $ \t ->
> pred_exists $ \ts0 ->
> pred_exists $ \ts1 ->
> (xs `pred_equals` ListNode t ts0) `pred_AND`
> (zs `pred_equals` ListNode t ts1) `pred_AND`
> (pred_join ts0 ys ts1)
> )
To see it in action, you need to do quite a bit of typing,
unfortunately:
run_pred $
pred_join
(Variable "xs")
(Variable "ys")
(ListNode (Number 1) (ListNode (Number 2) ListEndNode))
Should give you the following:
[(fromList [(Named "xs",ListEndNode),(Named "ys",ListNode (Number 1)
(ListNode (Number 2) ListEndNode))],1),(fromList [(Named "xs",ListNode
(Number 1) ListEndNode),(Named "ys",ListNode (Number 2)
ListEndNode),(Numbered 1,Number 1),(Numbered 2,ListEndNode),(Numbered
3,ListNode (Number 2) ListEndNode)],4),(fromList [(Named "xs",ListNode
(Number 1) (ListNode (Number 2) ListEndNode)),(Named
"ys",ListEndNode),(Numbered 1,Number 1),(Numbered 2,ListNode (Number 2)
ListEndNode),(Numbered 3,ListNode (Number 2) ListEndNode),(Numbered
4,Number 2),(Numbered 5,ListEndNode),(Numbered 6,ListEndNode)],7)]
which, if you unscramble it, translates as
xs = [], ys = [1,2]
xs = [1], ys = [2], ?1? = 1, ?2? = [], ?3? = [2],
xs = [1,2], ys = [], ?1? = 1, ?2? = [2], ?3? = [2], ?4? = 2, ?5? =
[], ?6? = []
Ignoring all the temp variables, that's basically
xs = [], ys = [1,2]
xs = [1], ys = [2]
xs = [1,2], ys = []
Which is, indeed, all possible ways to construct the list [1,2].
Now, to make it properly fun, implement a small parser than can take
an expression such as "[x,y,z]" and construct the appropriate
Haskell data structure, and a pretty printer that takes the
result and prints it in human-readable form. ;-)
Oh, by the way, if you take this entire post and save it to disk as
"Logic.lhs", you can load it into any Haskell-98 compliant compiler
or interpretter and run it. This is actual source code!
[Alternatively, if you want to just delete all lines not starting
with ">", that'll give you the raw Haskell code, so you can
inspect it without my comments interspersed.]
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
|
