Proving correctness of LR parser facts

I have came across following facts while reading some compilers related text. However I did not find them in any standard reference book (mainly dragon book). Are they correct? If yes, how can we prove them?


  1. If there is a λ-free LL(1) grammar for a language, then we can also prepare SLR(1) grammar for it. (λ-free means: there is no null productions of the form $ A\rightarrow\lambda$ for any non terminal $ A$ )
  2. LL(1) grammar whose variable are all able to derive a not null string is LALR(1). (able to derive a not null string means: there may exist null production $ A\rightarrow \lambda$ , but along with it, there should also exist non-null production $ A\rightarrow \alpha$ for every such $ A$ , where $ \alpha = (V+t)^*$ where $ V$ is any non terminal and $ t$ is any terminal)

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.