- From: Axel Polleres <axel.polleres@deri.org>
- Date: Tue, 14 Apr 2009 16:16:08 -0400
- To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

p.s.: small "process question" I am not sure whether I should not add the draft text for strongly safe rulesets at this point, since Core is frozen or are wiki changes allowed? Axel Axel Polleres wrote: > When going through the current safeness definition, I > 1) had some open quesitions and editorial suggestions and > 2) thought it turns out that strong safeness in the Eiter Schindlauer > sense probably "goes quite well" with the definitions Jos set up for > safety. > > Let's go for 1) first: > > "t=?V, in the context of ÃÂ, iff all variables appearing in tare safe > (resp., strongly safe) in ÃÂ', which is obtained from ÃÂ by > replacing > every occurrence of ?V=t with And(), in the context of ÃÂ'. " > > * I think that ?V=t should be replaced by t=?V, right? > > * "(resp., strongly safe)" should be > "(or strongly safe, resp.)" as far as I know. > > > * "for every variable symbol ?V and each occurrence of ?V in an atomic > formula ÃÂ±, let ÃÂ be the largest subformula of ÃÂ > such that ÃÂ± is a > subformula of ÃÂ and ?V is strongly safe in ÃÂ, then all > occurrences of > ?V in ÃÂ must be replaced with the symbol b; and with u otherwise," > > I don't really understand what the "otherwise" is referring to and where > I should replace ?V with u. > > * "Forall ?x ?y ?z ?u (ex:p(?x) :- Or( > And( ex:q(?z) pred:iri-string(?x ?z))) > And( ?x=?y ?y=?u ex:q(?u)))" > > should be: > > Forall ?x ?y ?z ?u (ex:p(?x) :- Or( > And( ex:q(?z) (External pred:iri-string(?x ?z)))) > And( ?x=?y ?y=?u ex:q(?u))) > > What about nested Externals?, I think the b-u replacement needs to be > defined recursively to cater for those, yes? I.e. starting with the > leaves of any nested subformula with externals, you start to apply your > algorithm and, if, there is a valid binding pattern for the formula, one > may replace that formula by b. Does that work? > > > Now for 2). I probably need jos' help to get that straight, but here a > first attempt to extend the notion of safe rule implications to strong > safety of a ruleset in the sense of Eiter&Schindlauer&Tompits. > To this end, I transcribed my sketch from > http://www.w3.org/mid/4992204B.7040705@deri.org > to the notation in the Core document. This shall go in place of the > Editor's note > > "Editor's Note: The working group has resolved to further extend this > notion of safeness to Eiter-Schindlauer safeness but place this > extended notion at risk. The definition of the additional constraints > which constitute Eiter-Schindlauer safeness and the associated At Risk > note are to be added." > > ===================================================================== > <p> > A ruleset consisting of only safe rule implications is called safe. > </p> > <p> > We now extend this notion to <i>strongly safe rulesets</i>. > The notion of <i>strongly safe</i> rulesets is inspired by > [Eiter&Schindlauer&Tompits] and implies that the ruleset always has a > finite set of ground atomic formulas entailed. > </p> > <p> > </p> > <p> > Let r be a set of safe rule implications of the form > <tt>φ :- ψ</tt> > as defined above. Then r<sub>a</sub>, the set of <i>adorned > rules</i> corresponding to r, is obtained as follows: > </p> > <p> > For each replacement <tt>θ</tt> of variable occurrences in <tt>φ > :- ψ</tt> as defined > before, a rule r<sub><tt>θ</tt></sub> is added to r<sub>a</sub> > such that > <ul> > <li>each variable ?X with ?X/<tt>b</tt> in <tt>θ</tt> is replaced by > ?X<sub>b</sub>, i.e., we say "?X is adorned with <tt>b</tt> in > r<sub>θ</sub>", and</li> > <li>each variable ?X with ?X/<tt>u</tt> in <tt>θ</tt> is replaced by > ?X<sub>u</sub>, i.e., we say "?X is adorned with <tt>u</tt> in > r<sub>θ</sub>"</li> > </ul> > > <p> > Let R be a ruleset of safe rule implications. > Then, by R<sub>a</sub> we denote ∪<sub>r in R</sub> r<sub>a</sub>. > </p> > > <p> > In order to define strong safety of R, we first build a dependency > relation <i>Rel</i> between all head and body predicates (ordinary or > external) occurring in rules r in R<sub>a</sub> as follows: > </p> > > <ul> > <li> if H occurs in head of a rule r and H in the body of r then add > (H,B).</li><li> if B occurs in the body of a rule r and H in the head of > r' such that > B and H unify, then add (B,H)</li> > <li>if B is an external predicate with ?X adorned with 'u' or an > ordinary predicate with variable ?X adorned with 'b', and B' is an > external predicate with ?X adorned with 'b' such that B,B' appear in the > same rule body, then add (B',B). > </li> > </ul> > > <p> > We say predicate P depends on Q if (P,Q) is in Rel. We say P > transitively depends on Q, if (P,Q) is in the transitive closure > <i>Rel<sup>*</sup></i> of <i>Rel</i>. We say P strictly depends > on Q if (P,Q) in <i>Rel<sup>*</sup></i> but not vice versa. > </p> > <p> > We are now ready to define strong safety: > </p> > <p> > Let r be a rule in R<sub>a</sub>. Let further <i>In</i> be the > set of all variables appearing in external predicates the body of r > adorned with 'b', i.e. the union of all "input variables" and > <i>Out</i> be the set of all variables appearing in external > predicates the body of r adorned with 'u', i.e. the union of > all "output variables". > </p> > <p> > Moreover, let S be the set of body atoms B in r, > such that the head atom of r depends strictly on B. > </p> > <p> > Let V be the set of all variables that occur in the ordinary atoms in > S plus all variables in <i>Out</i>\cup S. Then, r is strongly safe, iff > all head variables in r appear in the body and additionally <i>In</i> > is a subset of V. > </p> > <p> > We now say that the ruleset R is strongly safe if all rules r in > R<sub>a</sub> are strongly safe. > </p> > > > > -- Dr. Axel Polleres Digital Enterprise Research Institute, National University of Ireland, Galway email: axel.polleres@deri.org url: http://www.polleres.net/

Received on Tuesday, 14 April 2009 20:16:50 UTC