# Re: [PRD] Safeness definition in PRD (ACTION-826 complete)

From: Christian De Sainte Marie <csma@fr.ibm.com>
Date: Tue, 2 Jun 2009 11:23:39 +0200
To: Gary Hallmark <gary.hallmark@oracle.com>
Cc: RIF <public-rif-wg@w3.org>
Message-ID: <OF73E9F44A.4EB71775-ONC12575C9.002CE540-C12575C9.00339A64@fr.ibm.com>
```********* NOTICE **********
My new email address at IBM is: csma@fr.ibm.com
My ILOG email address will not be forwarded after June 8
*****************************
Hi Gary,

Thanx for the fast feedback.

Gary Hallmark <gary.hallmark@oracle.com> wrote on 02/06/2009 09:31:07:
>
> Just to spot check the accuracy, I tried to apply the PRD safeness to
> http://www.w3.org/2005/rules/wiki/Core_NonSafeness

Good point. I should have checked that before.

I checked and it works, essentially; except for a few bugs in the
definitions...

To wit, the unsafe rule in the example is:

FORALL y, z, IF y=z AND z>0 THEN p(y)

Computing bindable variables for the atomic formulas, following [1]:
- a1 is y=z: UBV(a1) = {}, CBV(a1) = {y, z}, with BCOND(y, a1)={{z}},
BCOND(z, a1)={{y}}
- a2 is z>0; UBV(a2)=CBV(a2)={}

[1] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var_atom

Computing bindable variables for the condition formula, following [2]:
- c is AND(a1, a2): UBV(c)={}, CBV(c)={y,z}, with BCOND(y,c)={{z}},
BCOND(z,c)={{y}}

[2] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var_formula

Conputing bindable variables for the rule, following [3]:
- r is FORALL y, z, IF y=z AND z>0 THEN p(y); we try the second case,
since {y,z} is in UBC(c) U CBV(c).  Therefore, we check that we can remove
all the quantified variables from the bindability conditions (of the
conditionally bindable variables), that is, we execute reduceBCOND({y,z},
{y,z}, {c}). And we find out:
1. that BCOND(y, c) reduces to {{y}}, and thus that we are in the third
case, and the rule is unsafe;
2. that the specification of reduceBCOND is buggy, since after reducing
BCOND(y, c) to {{y}}, it will loop forever trying to reduce
BCOND(z,c)=[{{y}} (since it replaces y by y...)
3. that the definition of a safe rule [4] (and, thus, of a well-formed
group) is buggy as well, since UBV(r) is always empty for a closed rule...

[3] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var_rule
[4] http://www.w3.org/2005/rules/wiki/PRD#def-safe-rule

I will correct the bugs raised in 2. and 3. But 1. seems to indicate that
the definitions are essentially correct. I also checked Core_NonSafeness_2
(it works without hitting the bug in reduceBCOND, because it goes directly
in the third bucket for a forall), Core_Safeness (it works, except for the
wrong definition as raised in 3, of course; that is, the rule is not
unsafe according to the operational definition, but it is not safe either,
according to definition [4] :-).

Core_Safeness_2 raises a bug in the specification of UBV for a
conjunction: the variables that are UBV in one of the conjunct are
correctly removed from the CBV of the conjunction, but I forgot to update
UBV with the CBV that depends only on such... I'll correct that.
Core_Safeness_3 hits the same bug.

> I ran up against this:
>
> *Definition (Safe condition formula).* A RIF-PRD condition formula is
> /*safe*/ if and only if it does not contain any unsafe sub-formula (and
> if it is not unsafe itself).

I used safe/unsafe for formulas only. But UBV means safe variables (and
CBV conditionally safe). I thought that using names that referred
explicitly to binding was a good idea: maybe it is not.

> The only mention of "unsafe" is in the context of an Exists formula.

...and in the context of a Forall formula.

> Surely some condition formulas without Exists are also unsafe.

No, as far as I understand: a formula is safe if you can guarantee that
all the variables can be bound (without constraint resolution) when
evaluating the formula. If a formula contains no variable, it is always
safe; if it contains free variables, you cannot decide whether it is safe
or not (at least in the context of RIF: if a variable is free in a
formula, that means that the formula is a component of another formula,
and, thus, that the free variable might be bound somewhere else).

So a condition formula without an Exists cannot be unsafe; but a rule with
that condition can be (because it is closed under forall).

> It's not
> very clear when you define safeness as the absence of unsafeness or vice

> versa.

Yes, as I said, the wording and presentation can certainly be improved.
Currently, unsafeness is defined operationally, and safeness is defined as
the absence of unsafeness. The difficulty is that, really, there is safe,
unsafe, and maybe safe; at least as long as a formula has free
variables...

Cheers,

Christian

Sauf indication contraire ci-dessus:/ Unless stated otherwise above:
Compagnie IBM France
Siège Social : Tour Descartes, 2, avenue Gambetta, La Défense 5, 92400
Courbevoie
RCS Nanterre 552 118 465
Forme Sociale : S.A.S.
Capital Social : 609.751.783,30 ?
SIREN/SIRET : 552 118 465 02430
```
Received on Tuesday, 2 June 2009 09:49:09 UTC

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