W3C home > Mailing lists > Public > public-rif-wg@w3.org > September 2008

[Core] Definition of strict safeness

From: Axel Polleres <axel.polleres@deri.org>
Date: Thu, 25 Sep 2008 09:23:25 +0100
Message-ID: <48DB4A7D.3060303@deri.org>
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 &phi; if it appears in at least one non-external atomic 
subformula
&psi; of &phi;
such that ?v  is not in the  scope of an existential quantifier within 
&psi;.
A RIF condition formula &phi; is called strictly safe if all its 
variables are safe
with respect to &phi;
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 Thursday, 25 September 2008 09:31:10 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 2 June 2009 18:33:54 GMT