Re: [Core](PRD] safeness

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