Re: [Core](PRD] safeness

Discharging action-842 ...

As far as I can see this approach does work for Core and is a simpler 
exposition than the current one since it avoids the explicit 
construction of the disjunction tree. Nice. I'd be happy to shift to 
this definition.

[I did worry the lack of an explicit notion of variable equivalence 
classes but on reflection I can see that this approach handles the 
equivalence chains correctly.]

I thought there was an editorial problem with the definition of bound 
for an existential formula but you seem to have already corrected that 
on the wiki.

Trivial editorial: there's a spurious extra ", ," in the 3rd bullet of 
the definition of boundedness in conjunctions.

Dave

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 22:12:59 UTC