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

This seems more complicated than the safeness definition in Core. It 
seems to me the Core definition can be easily extended to cover Not and 
nested Forall, and then it pretty much covers PRD.

Just to spot check the accuracy, I tried to apply the PRD safeness to 
http://www.w3.org/2005/rules/wiki/Core_NonSafeness

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).

The only mention of "unsafe" is in the context of an Exists formula. 
Surely some condition formulas without Exists are also unsafe. It's not 
very clear when you define safeness as the absence of unsafeness or vice 
versa.

Christian De Sainte Marie wrote:
>
> ********* NOTICE **********
> My new email address at IBM is: csma@fr.ibm.com
> My ILOG email address will not be forwarded after June 8
> *****************************
> all,
>
> We all agree that the operational semantics of rules and rule sets in 
> PRD requires some sort of safeness, at least that all the rule 
> variables that occur in the action block must be bound in the condition.
>
> To be able to specify the necessary notions, I added the definition of 
> the sets of the unconditionally (UBV) and conditionally bindable 
> variables (CBV), in atomic formulas [1], general condition formulas 
> [2] and rules [3].
>
> I use the definition of these sets to define safe condition formulas 
> [4] (that can be evaluated relying on pattern matching only) and safe 
> rules [5] (and rule sets).
>
> The presentation of the definition of UBV and CBV could certainly be 
> improved, but, more than anything, somebody must check that they are 
> correct, and that they extend the definition of safeness in Core. 
> *Jos* comes to mind. Bugs can be corrected later, but the definitions 
> must be, at least, essentially correct.
>
> [1] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var
> [2] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var_formula
> [3] http://www.w3.org/2005/rules/wiki/PRD#def-bindable-var_rule
> [4] http://www.w3.org/2005/rules/wiki/PRD#def-safe-formula
> [5] http://www.w3.org/2005/rules/wiki/PRD#def-safe-rule
>
> This completes my ACTION-826.
>
> Cheers,
>
> Christian
>
> ILOG, an IBM Company
> 9 rue de Verdun
> 94253 - Gentilly cedex - FRANCE
> Tel. +33 1 49 08 35 00
> Fax +33 1 49 08 35 10
>
>
> 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 07:32:04 UTC