Re: [Core] Definition of strict safeness

Hi Axel,

Option 2 actually seems to covers Gary's requirements fine, though I've 
no real objection to 3.

Presumably the full definition would also include the normal safeness 
constraint that variables in the rule head must all be safe wrt to the 
condition part so that "universal facts" like:

    Forall ?x ?y _sameKey(rdf:nil, ?x, ?y)

would not be safe, right?

Dave

Axel Polleres wrote:
> 
> This completes my action from the last Core conf.-call:
> 
> 
> In the following, I give some possible definitions of strict safeness, 
> proposed to be included in Core. Personally, I favor either Option 1 (no 
> disjunction in bodies) or  Option 3 (allowing disjunction, but checking 
> safeness recursively within disjunctions). Option 2 is somewhat 
> middle-ground in that it says basically that a variable can't be "saved"
> within a disjunction.
> 
> I will try to extend these definitions for weak safeness, but weak 
> safeness was more argued about, whereas strict safeness seems to have 
> been agreed.
> 
> Comments welcome!
> 
> best,
> Axel
> 
> ------------- start of proposed text for Core document --------------
> 
> Safeness is a syntactic condition which guarantees finiteness and finite
> computability of the minimal model of a RIF Core ruleset. In the 
> following, we define
> the different notions of safeness.
> 
> Option 1: no disjunction in Rule bodies
> =========================
> 
> A subformula of a RIF condition formula is called external sub-formula 
> if it
> appears within an Externally defined term. A variable ?v  is called safe 
> with respect
> to a RIF formula φ if it appears in at least one non-external atomic 
> subformula
> ψ of φ
> such that ?v  is not in the  scope of an existential quantifier within 
> ψ.
> A RIF condition formula φ is called strictly safe if all its 
> variables are safe
> with respect to φ
> and for all its existential subformulas
> Exists ?V<sub>1</sub> ... ?V<sub>n</sub> ( &psi; ) each
> ?V<sub>1</sub>, ... , ?V<sub>n</sub> is safe with respect to &psi;
> A RIF rule &phi :- &psi; is called stricty safe if all its variables are 
> safe with respect to
> &psi;.
> 
> Note: If we disallow nested existentials in Core than we can remove in 
> this definition
> "such that v  is not in the scope of an existential quantifier within 
> &psi;."
> as well as
> "and for all its existential subformulas Exists ?V<sub>1</sub> ... 
> ?V<sub>n</sub> ( &psi; ) each ?V<sub>1</sub>, ... , ?V<sub>n</sub> is 
> safe with respect to &psi;"
> 
> 
> Option 2: disjunction in Rule bodies over-cautions non-recursive definition
> ================================================
> 
> A subformula of a condition formula is called external subformula if it
> appears within an Externally defined term. A subformula of a condition 
> formula
> is called disjunctive subformula if it appears within a Disjunction.
> A variable v  is called safe with respect to a RIF formula &phi; if it 
> appears in
> at least one non-external, non-disjunctive atomic subformula of &phi;
> such that ?v  is not in the  scope of an existential quantifier within 
> &psi;.
> 
> (the remainder of the definition is as for Option 1)
> 
> Option 3: disjunction in Rule bodies recursive definition:
> ====================================
> 
> A subformula of a condition formula is called external subformula if it
> appears within an Externally defined term.
> - A variable ?v  is called safe  with respect to a non-external, atomic 
> RIF formula &phi; if
> it appears in &phi;.
> - A variable ?v is called safe with respect to a disjunction Or( 
> &phi;<sub>1</sub> ... &phi;<sub>n</sub>) if ?v
> is safe with respect to each &phi;<sub>1</sub> ... &phi;<sub>n</sub>.
> - A variable ?v is called safe with respect to a conjunction Or( 
> &phi;<sub>1</sub> ... &phi;<sub>n</sub>) if it
> is safe with respect to at least one of &phi;<sub>1</sub> ... 
> &phi;<sub>n</sub>.
> - A variable is called safe with respect to an Existential  Exists 
> ?V<sub>1</sub> ... ?V<sub>n</sub> ( &phi ) if
> (i) ?v != ?V<sub>1</sub> and ... and v != ?V<sub>n</sub>, and
> (ii) ?v is safe with respect to &phi, and
> (iii) all ?V<sub>1</sub> ... ?V<sub>n</sub> are safe with respect to &phi;
>

Received on Friday, 26 September 2008 00:16:17 UTC