Re: [Core](PRD] safeness

gary.hallmark@gmail.com wrote on 11/06/2009 01:46:56:
> 
> I think that
> 
> Forall x if Not(Px) then print("hello world")
> 
> is equivalent to
> 
> if Not(Exists x (Px)) then print("hello world")
> 
> Both are safe.

If Not(Exists x Px)) then...

is equivalent to

If Forall x Not(Px) then...

Which is not equivalent to

Forall x If Not(Px) then...

In the former case, the rule fires once; in the latter, it fires as many 
times as there are values for x that are not P; which may be many times, 
and which is why the rule is not safe. And
 
> I don't see how your safeness definition for PRD distinguishes the
> safe ones from the unsafe ones.

You are right, the definition is not explicit enough on this aspect (in an 
earlier version, there was a note about whether we should remind readers 
that existentially quantified variables did not exist outside their 
existential formula, but I removed it without action, when Dave seemed to 
imply that it was clear enough).

For the avoidance of doubt and ambiguity,
* the rules for moving out existential quantifiers must be explicited 
(they can be moved out only as far as it does not change there meaning, 
that is, until the next enclosing negation;
* and it must also be made explicit, in the definition of rule safeness, 
that existentially quantified variables need only be bound within the 
scope of their quantifier.

I will edit the text in [1] to make those points precise.

[1] http://www.w3.org/2005/rules/wiki/PRD_Safeness_Bottomup

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