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

********* 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