- From: Axel Polleres <axel.polleres@deri.org>
- Date: Thu, 25 Sep 2008 09:23:25 +0100
- To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

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 φ

Received on Thursday, 25 September 2008 09:31:10 UTC