Re: [Core](PRD] safeness

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>
```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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:56 UTC