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>

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 02430Received on Wednesday, 10 June 2009 13:24:11 GMT

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