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

Gary, all,

I corrected the bugs in the definition of safe (unconditionally bindable) 
and conditionally safe (conditionally bindable) variables, and in the 
definitions of safe formulas and rules (and I took the opportunity to 
correct a bug in the definition of well-formed groups, as well :-).

The spec passes the 2 unsafe and the 3 safe tests.

I also tried to simplify the definitions and to make them easier to read 
and understand.

Cheers,

Christian

csma wrote on 02/06/2009 11:23:39:
> 
> ********* 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


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