Re: [Core] 1) editorial things in Core and 2) first draft of Eiter-Schindlauer safety.

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>&theta;</tt> of variable occurrences in <tt>φ 
> :- ψ</tt> as defined
> before, a rule r<sub><tt>&theta;</tt></sub> is added to r<sub>a</sub>
> such that
> <ul>
> <li>each variable ?X with ?X/<tt>b</tt> in <tt>&theta;</tt> is replaced by
> ?X<sub>b</sub>, i.e., we say "?X is adorned with <tt>b</tt> in 
> r<sub>&theta;</sub>", and</li>
> <li>each variable ?X with ?X/<tt>u</tt> in <tt>&theta;</tt> is replaced by
> ?X<sub>u</sub>, i.e., we say "?X is adorned with <tt>u</tt> in 
> r<sub>&theta;</sub>"</li>
> </ul>
> 
> <p>
> Let R be a ruleset of safe rule implications.
> Then, by R<sub>a</sub> we denote &cup;<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