Re: [Core] Definition of strict safeness

Dave Reynolds wrote:
> 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?

Indeed:

In option 1+2 only rules were covered by:

" A RIF rule &phi :- ψ is called stricty safe if all its variables 
are safe with respect to  ψ."

Indeed I forgot facts and that sentence misses for  Option 3
So, let's add (for all three options):

========================================================================
- A RIF rule implication &phi :- ψ is called stricty safe if all its 
variables are safe with respect to ψ.

- A RIF Universal rule implication Forall ?V1 ... ?Vn (&phi) is called 
stricty safe if φ is strictly safe.

- A RIF Universal fact Forall ?V1 ... ?Vn (&phi) is called stricty safe 
if φ is ground.

Note that, particularly, the last item disallows variables in facts.
========================================================================





> 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;
>  >
> 


-- 
Dr. Axel Polleres, Digital Enterprise Research Institute (DERI)
email: axel.polleres@deri.org  url: http://www.polleres.net/

Everything is possible:
rdfs:subClassOf rdfs:subPropertyOf rdfs:Resource.
rdfs:subClassOf rdfs:subPropertyOf rdfs:subPropertyOf.
rdf:type rdfs:subPropertyOf rdfs:subClassOf.
rdfs:subClassOf rdf:type owl:SymmetricProperty.

Received on Saturday, 27 September 2008 13:41:57 UTC