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