From: Axel Polleres <axel.polleres@deri.org>

Date: Sat, 27 Sep 2008 09:41:11 -0400

Message-ID: <48DE37F7.90801@deri.org>

To: Dave Reynolds <der@hplb.hpl.hp.com>

CC: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Date: Sat, 27 Sep 2008 09:41:11 -0400

Message-ID: <48DE37F7.90801@deri.org>

To: Dave Reynolds <der@hplb.hpl.hp.com>

CC: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

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> ( ψ ) each > > ?V<sub>1</sub>, ... , ?V<sub>n</sub> is safe with respect to ψ > > A RIF rule &phi :- ψ is called stricty safe if all its variables are > > safe with respect to > > ψ. > > > > 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 > > ψ." > > as well as > > "and for all its existential subformulas Exists ?V<sub>1</sub> ... > > ?V<sub>n</sub> ( ψ ) each ?V<sub>1</sub>, ... , ?V<sub>n</sub> is > > safe with respect to ψ" > > > > > > 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 φ if it > > appears in > > at least one non-external, non-disjunctive atomic subformula of φ > > such that ?v is not in the scope of an existential quantifier within > > ψ. > > > > (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 φ if > > it appears in φ. > > - A variable ?v is called safe with respect to a disjunction Or( > > φ<sub>1</sub> ... φ<sub>n</sub>) if ?v > > is safe with respect to each φ<sub>1</sub> ... φ<sub>n</sub>. > > - A variable ?v is called safe with respect to a conjunction Or( > > φ<sub>1</sub> ... φ<sub>n</sub>) if it > > is safe with respect to at least one of φ<sub>1</sub> ... > > φ<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 > φ > > > -- 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

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