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

From: Axel Polleres <axel.polleres@deri.org>
Date: Tue, 14 Apr 2009 16:16:08 -0400
Message-ID: <49E4EF08.7050206@deri.org>
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>&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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:55 UTC