Rules and Facts (cyclic ?) definition in an inference engine

Question

I am working on an backwards chaining engine as a school project. Until now, I have mostly done projects in C, and so I decided to try Haskell for that projet. I have read LYAH in order to get started and have begun to implement the representation of rules and facts in my inference engine. So far, this is what I got

module Inference () where

type Op = Bool -> Bool -> Bool
type Label = String
type Fact = (Label, [Rule])
data Rule = Operation Rule Op Rule
          | Fact Fact

eval_fact:: [Label] -> Fact -> Bool
eval_fact proved (label,rules) = label `elem` proved || any (eval_rule proved) rules

eval_rule:: [Label] -> Rule -> Bool
eval_rule proved (Fact x) = eval_fact proved x
eval_rule proved (Operation r op r') =  eval_rule proved r `op` eval_rule proved r'

The idea being to have some kind of graph where Fact nodes points to Rules nodes, unless the fact is already in a list of known facts.

However, here I encounter the problem of defining my actual facts and rules.

Doing somethings like

let fact_e = ("E", [Fact ("C", [(Operation (Fact ("A", [])) (||) (Fact ("B", [])))])])

in ghci in order to represent the rules

C => E
A || B => C

That works. But I don't really see what direction to go to construct theses rules programmatically. Furthermore, I don't see how I can handle cyclic rules with that scheme (adding a rule E => A for example).

I have seen that there is ways to define self referencing data structures in haskell with the trick called "Tying the knot" on the Haskell wiki, but I don't see how (or even if) I should apply that in the present case.

My question is essentially, am I going in the right direction, or do I have it completely backward with that approach ?

P.S : It also seems to me that my code is not as concise as it should be (passing around the [Label] list, repeating eVal_rule proved many times...), but I don't really know either how to do it in another way.

Answer 1

The idea would be to first parse the rules into an intermediate representation that is not self referential. For example, given the representation:

type Program = [(Label, [Rule_P])]
data Rule_P = Operation_P Rule_P Op Rule_P | Fact_P Label

then the set of rules:

C => E
A || B => C
E => A
F => E

would be parsed, gathered by implication target, and represented as:

prog1 :: Program
prog1 = [ ("E", [ Fact_P "C"                                       -- C => E
                , Fact_P "F" ])                                    -- F => E
        , ("C", [ Operation_P (Fact_P "A") (||) (Fact_P "B") ])    -- A || B => C
        , ("A", [ Fact_P "E" ]) ]                                  -- E => A

Then, to convert this to a cyclically self-referential knowledge base (using your original Fact type):

type Knowledge = [Fact]

you tie the knot like so:

learn :: Program -> Knowledge
learn program = knowledge

  where

    knowledge :: [Fact]
    knowledge = [ (target, map learn1 rules_p) | (target, rules_p) <- program ]

    remember lbl = fromJust (find ((==lbl) . fst) knowledge)

    learn1 :: Rule_P -> Rule
    learn1 (Fact_P lbl) = Fact (remember lbl)
    learn1 (Operation_P rule1 op rule2) = Operation (learn1 rule1) op (learn1 rule2)

This perhaps deserves some explanation. We create knowledge by simply applying learn1 to convert each occurrence of a non-self-referential Rule_P in the original program into a self-referential Rule in the knowledge base. The function learn1 does this in the obvious recursive manner, and it "ties the knot" at each Fact_P by looking up (remembering) the label in the body of knowledge that we're in the middle of defining.

Anyway, to prove to yourself that it's self-referential, you can play with it in GHCi:

> know1 = learn prog1
> Just [Operation factA _ _] = lookup "C" know1
> Fact ("A", [factE]) = factA
> Fact ("E", [factC, _]) = factE
> Fact ("C", [Operation factA' _ _]) = factC
> Fact ("A", [factE']) = factA'

Of course, trying:

> eval_fact [] $ fromJust $ find ((=="E").fst) (learn prog1)

will loop until it runs out of memory, as it tries to (unsuccessfully) prove E from C from A from E, etc., so you'll need to add some logic to abort cyclic proofs.