- From: Axel Polleres <axel.polleres@deri.org>
- Date: Tue, 14 Apr 2009 13:39:03 -0400
- To: Jos de Bruijn <debruijn@inf.unibz.it>, "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

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>

Received on Tuesday, 14 April 2009 20:08:53 UTC