# Re: [Core](PRD] safeness

From: Christian De Sainte Marie <csma@fr.ibm.com>
Date: Wed, 10 Jun 2009 15:22:12 +0200
To: Dave Reynolds <der@hplb.hpl.hp.com>
Cc: RIF <public-rif-wg@w3.org>
Message-ID: <OF81157BC1.B75320F7-ONC12575D1.0046B3FC-C12575D1.004971F1@fr.ibm.com>
```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...

One heavy fix is to re-introduce the notion o fconditionally bound, and
corry the conditions over, as I did initially in PRD.

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).

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

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

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.

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 Wednesday, 10 June 2009 13:24:11 UTC

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