# [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.

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 UTC