haskellrecursive-datastructurescyclic-referenceinference-engine

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


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.


Solution

  • 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.