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>

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 02430Received on Tuesday, 2 June 2009 09:49:09 GMT

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