[Core] Definition of strict safeness

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 Thursday, 25 September 2008 09:31:10 UTC