Re: [Core](PRD] safeness

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 England

Received on Wednesday, 10 June 2009 14:24:58 UTC