Re: [Core](PRD] safeness

Christian,

I do not think you can ignore negation in safeness/boundedness. For example,

if P(?x) and ?x=1 then Q(1) // clearly safe
if ?x=1 then Q(0) // clearly not safe

so what about:

R1: if not(P(?x) and ?x=1) then Q(1)
R2: if not(?x=1) then Q(0)
R3: if not(P(?x) and ?x=1) then Q(?x)

I claim R1 is safe because ?x is bounded and used only "inside the not".
R2 is unsafe because ?x is not bounded.
R3 is unsafe because ?x is not bounded or safe "outside the not".


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
> *****************************
>
> </Chair>
>
> All,
>
> From my initial definition in PRD, which is too complex, and from the 
> definition in Core, which does not extend naturally to PRD, as Gary's 
> attempt shows, I derived a bottom-up definition of safeness and 
> boundedness in Core, that, I think, is correct (in the sense that it 
> is equivalent to the definition currently in Core) and that extends 
> very easily to PRD [1].
>
> [1] http://www.w3.org/2005/rules/wiki/PRD_Safeness_Bottomup
>
> Jos agreed that, if that definition is, indeed, correct, we should use 
> it in Core instead of the current one (and thus in PRD as well).
>
> But he is not is a shape, today, to check the equivalence of his 
> definition in Core and the bottom-up one...
>
> He said he would look at it tomorrow, but if you all could review it 
> as well, in the meantime, that would help.
>
> 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, 9 June 2009 20:55:31 UTC