From: Christian De Sainte Marie <csma@fr.ibm.com>

Date: Tue, 2 Jun 2009 15:48:24 +0200

To: Christian De Sainte Marie <csma@fr.ibm.com>

Cc: Gary Hallmark <gary.hallmark@oracle.com>, RIF <public-rif-wg@w3.org>

Message-ID: <OFA8D28BBE.81278B7C-ONC12575C9.004A6FC2-C12575C9.004BD71E@fr.ibm.com>

Date: Tue, 2 Jun 2009 15:48:24 +0200

To: Christian De Sainte Marie <csma@fr.ibm.com>

Cc: Gary Hallmark <gary.hallmark@oracle.com>, RIF <public-rif-wg@w3.org>

Message-ID: <OFA8D28BBE.81278B7C-ONC12575C9.004A6FC2-C12575C9.004BD71E@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 ***************************** 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 02430Received on Tuesday, 2 June 2009 13:49:10 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Tuesday, 2 June 2009 18:34:08 GMT
*