From: Dave Reynolds <der@hplb.hpl.hp.com>

Date: Wed, 10 Jun 2009 15:23:59 +0100

Message-ID: <4A2FC1FF.6020300@hplb.hpl.hp.com>

To: Christian De Sainte Marie <csma@fr.ibm.com>

CC: RIF <public-rif-wg@w3.org>

Date: Wed, 10 Jun 2009 15:23:59 +0100

Message-ID: <4A2FC1FF.6020300@hplb.hpl.hp.com>

To: Christian De Sainte Marie <csma@fr.ibm.com>

CC: RIF <public-rif-wg@w3.org>

Christian De Sainte Marie wrote: > > Dave Reynolds <der@hplb.hpl.hp.com> wrote on 10/06/2009 00:12:16: > > > > > [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.] > > Unfortunally, it does not... Would have been too easy :-) > > A counter example is f = (x=1 and (Py or x=y)). y is safe in f, I think, > although it is not safe in (Py or x=y), because it is not safe in x=y... Argh yes, I should have worried at my worry for longer. > One heavy fix is to re-introduce the notion o fconditionally bound, and > corry the conditions over, as I did initially in PRD. Too much of a change to fit in Core in the few hours available. > An easy fix is to consider that the definitions work fine if the formula > is in disjunctive normal form, with the existential quantifiers moved > out first (and quantified variables being renamed appropriately, of > course). Yes, that's preferable. > I propose, therefore, to change the preprocesisng step, in the bottom-up > definition, to: > <<The definitions of /boundedness/ and /safeness/, below, apply to a > formula, /f/, after it has been simplified syntactically, by applying > the to following transforms: > 1. if f contains existential sub-formulas, all the quantified variables > are renamed and given a name that is unique in f, and the quantifiers > are moved out of f; > 2. the (possibly existentially quantified) resuling formula is rewritten > in disjunctive normal form.>> Might be appropriate to explicitly spell out the transformation to DNF I guess, but that could be done later as an editorial change. > x=1 and Exists y (Py or x=y) in which y is bound but that would fail the > current def, is transformed into > Exists y (x=1 and Py) or (x=1 and x=y), where both x and y are bound and > safe. > > Not only the definitions are then correct, but they are trivially > equivalent to Jos's, since the first pre-processing step is the same as > Jos's elimination of existentials, and the Jos's Tree decomposition in > Jos's definition really amounts to bringing the formula to DNF... Yes, at least that's my understanding of it. > One thing that we could do is use the definition with DNF preprocessing > in Core, and add an implementor's note with the definition of > conditional boundedness and how conditions carry over, and conditionally > bound variables eventually become bound (or not). Not sure it is useful, > though. I don't see the value of such an implementor's note in Core. Dave -- Hewlett-Packard Limited Registered Office: Cain Road, Bracknell, Berks RG12 1HN Registered No: 690597 EnglandReceived on Wednesday, 10 June 2009 14:24:58 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Wednesday, 10 June 2009 14:24:59 GMT
*