Re: Optimizing for recursive rules

Hey Chimezie,

Let me first try to let some "running code" speak for itself :-)
and point to the small section of Prolog code at
% Skolem Euler Machine
in http://eulersharp.sourceforge.net/2006/02swap/euler.yap

sem/1 is like a forward chaining Horn engine producing
the "trunk" deductive closure and sem/4 is the "branching"
again forward chaining but taking care of false, possible
and counter models. The trunk is like the main tape and
the branches are like the split tapes of the skolem machine
as is nicely depicted in
http://www.csupomona.edu/~jrfisher/www/geolog/

Now to see whar really happens with the small test case
of yesterday

GIVEN
:a :b :c.
:d :e :c.

{?X :b ?Y} => {_:Z :p ?Y}.
{?X :e ?Y} => {_:Z :p ?Y}.

QUERY
{?X :p ?Y} => {?X :p ?Y}.

I have just added some debug info and part of what it shows is

enter branch []
. selecting rule pcl(<http://www.agfa.com/abc/try#b>(_12855,_12856),<
http://www.agfa.com/abc/try#p>(_12858,_12856),<try.n3>)
... labelvars <http://www.agfa.com/abc/try#p>(sk(0),<
http://www.agfa.com/abc/try#c>)
... assert step <http://www.agfa.com/abc/try#p>(sk(0),<
http://www.agfa.com/abc/try#c>)
enter branch []
. selecting rule pcl(<http://www.agfa.com/abc/try#b>(_12950,_12951),<
http://www.agfa.com/abc/try#p>(_12953,_12951),<try.n3>)
.. euler path so do not step in your own step <
http://www.agfa.com/abc/try#p>(_12953,<http://www.agfa.com/abc/try#c>)
. selecting rule pcl(<http://www.agfa.com/abc/try#e>(_12950,_12951),<
http://www.agfa.com/abc/try#p>(_12953,_12951),<try.n3>)
.. euler path so do not step in your own step <
http://www.agfa.com/abc/try#p>(_12953,<http://www.agfa.com/abc/try#c>)

So the key point is that an existential variable in the conclusion
is kept as a prolog variable and labelvars is applied just in time
before the triple is asserted.
That is basically it and I think that it could fit with RETE quite well..

Kind regards,

Jos De Roo | Agfa HealthCare
Senior Researcher | HE/Advanced Clinical Applications Research
T  +32 3444 7618
 http://www.agfa.com/w3c/jdroo/

Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
http://www.agfa.com/healthcare



Chimezie Ogbuji <chimezie@gmail.com> 
Sent by: public-cwm-talk-request@w3.org
02/11/2009 04:21 PM

To
fuxi-discussion@googlegroups.com
cc
Dan Connolly <connolly@w3.org>, public-cwm-talk@w3.org
Subject
Re: Optimizing for recursive rules








Hey Jos.  Good to hear from you.  See my comments inline.

jos.deroo@agfa.com wrote:
> Actually we use quite a lot of (even mutual) recursive rules and
> you are right that existentials in the conclusion can complicate things.
> Our experience is that a fresh bnode label per rule firing or using a
> skolem function (like the euler builtin e:tuple) is giving too much
> artificially introduced triples. On the other hand, a universal skolem
> machine is doing a fine job, e.g. like explained in the last paper in
> 
http://folli.loria.fr/cds/2006/courses/Bezem.Nivelle.IntroductionToAutomatedReasoning.pdf 


Yes, I have tried to glean the method from that last paper but
unfortunately haven't been able to.  Perhaps you can help decipher it or
at least generalize the intuitions / motivations?


> [[
> CL will never for any existential conclusion introduce a new witness if 
> there exists
> already one. Skolem functions give new witnesses even if there exists 
> already one.
> As a simple example, consider the coherent axiom p(x) → ∃y. p(y). This 

> is, of course,
> an easy tautology. CL will never use it since the conclusion is 
> fulfilled whenever
> the premiss is true. In clausifying it without thinking one starts by 
> partly spoiling
> the dependence of the conclusion on the premiss: ∃y. (p(x) → p(y)). 
Then 
> one
> makes the dependence of y on x explicit by introducing a Skolem 
function:
> p(x) → p(f (x))). This is no longer a tautology, but a clause which 
> makes the
> Herbrand universe infinite and can play a complicating role in the proof 

> search.
> ]]
> 
> A small test case that we ran using the euler.yap engine might 
> illustrate above:

Yes, I get the general motivation for (as you explain above) the
artificial nature of simply introducing a skolem term (or witness) in
place of the existential variables in the head of rule since this
doesn't account for  already existing 'witnesses'.  However, I'm having
a hard time understanding Coherent Logic Theory well enough to determine
how I might integrate it with my current inference strategy.

> gives 2 triples
> _:e0 :p :c.
> _:e1 :p :c.
> 
> gives only 1 triple
> _:sk0 :p :c.

(just thinking out loud) the difference seems to have some
correspondence with the notion of lean graphs, correct?

> I think that having the skolem machine effect in fuxi and cwm
> is doable, well I'm convinced it is :)

Excellent.  Your confidence is encouraging.  So perhaps you can help me
out here :)

>From what I can glean, coherent logic is an extension of resolution
theory which is in the category of 'top-down' or theorem proving
methods.  Generally (as of late), I've been relying on the fact that
(after magic set transformation of a set of definite horn clauses)
evaluation via bottom-up methods (forward-chaining or fixed-point
calculation) are equivalent to top-down methods (SLD resolution in
particular) [Brass S. 1995].

So, I'm basically relying on a production rule algorithm (RETE-UL) to
efficiently ( and via forward-chaining ) calculate a unique minimal
model for the ruleset.  I believe CWM does the same (i.e., rely on some
form of RETE for efficiency).

This is very much an operational approach and thus very different from
the more declarative inference procedures such as tableux or resolution
(Prolog) - despite the fact that their semantics coincide (in the case
where the language corresponds to definite horn clause logic).

With that in mind, I was hoping to extract from the CL paper, the
specific aspects of the method that deal with the handling of the so
called coherent disjunctions (where you have existentially quantified
variables in the antecedent) but I wasn't able to.  Could you point me
to the specific sections in that paper?

[Brass S. 1995]
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.591

> 
> Kind regards,
> 
> Jos De Roo | Agfa HealthCare
> Senior Researcher | HE/Advanced Clinical Applications Research
> T  +32 3444 7618
> http://www.agfa.com/w3c/jdroo/
> 
> Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
> http://www.agfa.com/healthcare
> 
> 
> *Chimezie Ogbuji <chimezie@gmail.com>*
> Sent by: fuxi-discussion@googlegroups.com
> 
> 02/09/2009 03:40 AM
> Please respond to
> fuxi-discussion@googlegroups.com
> 
> 
> 
> To
>                fuxi-discussion@googlegroups.com
> cc
> 
> Subject
>                Re: Optimizing for recursive rules
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> Hey Chris.  See my response inline below
> 
> Chris G. wrote:
>  > Suppose I have a rule that, when fired, creates a fact that might
>  > trigger the same rule.  Such rules seem to slow FuXi down 
considerably
>  > (by about fact 250, or so), but when the recursive part is removed, 
it
>  > runs like lightning.  Is there a way to optimize my rules and facts 
to
>  > avoid the cost incurred by recursive rules, or should we try and
>  > figure out a way to not need the recursive rules in the first place?
>  > Here is the rule that is causing the slowness:
> 
> Unfortunately, recursive rules are inherently complex to compute for any
> rule engine.  Fuxi currently doesn't do anything special to handle
> recursion.  One thing that can be ruled out, however, is how much of the
> slow down is primarily due to overhead (inefficiencies in the Python)
> and this can be determined via profiling a run over recursive rules.
> 
> Looking at the rule below, it looks like the problem is further
> compounded by the fact that you have a BNode in the consequent / head of
> the rule.  FuXi will attempt to create a new name for the BNode every
> time the rule is fired.  This is only problematic if this then triggers
> a cycle (where the same rule is fired, etc..).  The only way this can be
> dealt with is via a proper handling of BNodes in the consequent / head
> of rules such as Jos pointed out in an earlier email.
> 
> Overall, I'd suggest you look into trying to avoid recursive rules in
> the first place.
> 
> 
>  > {
>  >   ?sir a m:SequentialInferenceRelation.
>  >   ?inf1 a m:Inference.
>  >   ?inf1 has m:inference_name ?infName1.
>  >   ?sir has m:inference_name_1 ?infName1.
>  >   ?inf2 a m:Inference.
>  >   ?inf2 has m:inference_name ?infName2.
>  >   ?sir has m:inference_name_2 ?infName2.
>  >   ?sir has m:new_inference_name ?newInfName.
>  >   ?inf1 has m:inference_time ?infTime1.
>  >   ?inf2 has m:inference_time ?infTime2.
>  >   ?infTime2 math:greaterThan ?infTime1.
>  > } => {
>  >   @forSome :inf.
>  >   :inf a m:Inference.
>  >   :inf has m:inference_name ?newInfName.
>  > }.
> 
> -- Chimezie
> 
> 
> 
> 
> 
> --~--~---------~--~----~------------~-------~--~----~
> You received this message because you are subscribed to the Google 
> Groups "fuxi-discussion" group.
> To post to this group, send email to fuxi-discussion@googlegroups.com
> To unsubscribe from this group, send email to 
> fuxi-discussion+unsubscribe@googlegroups.com
> For more options, visit this group at 
> http://groups.google.com/group/fuxi-discussion?hl=en
> -~----------~----~----~----~------~----~------~--~---
>