From: Stella Mitchell <stellamit@gmail.com>

Date: Wed, 10 Jun 2009 11:55:49 -0400

Message-ID: <d64b0f2c0906100855y46467c66l1614ed3ea7c10fa@mail.gmail.com>

To: Christian De Sainte Marie <csma@fr.ibm.com>

Cc: RIF <public-rif-wg@w3.org>

Date: Wed, 10 Jun 2009 11:55:49 -0400

Message-ID: <d64b0f2c0906100855y46467c66l1614ed3ea7c10fa@mail.gmail.com>

To: Christian De Sainte Marie <csma@fr.ibm.com>

Cc: RIF <public-rif-wg@w3.org>

Hi Christian, Here are some comments on the Safeness in Core section, 1st para: (I know it's just copied over) You could take out the "Intuitively" and just say "b stands for "bound"..." 5th para: ("The definitions of boundedness...") 1st sentence: formula --> condition formula ? (for extra clarity because formula (in the math english) in Core is defined as atomic formula, condition formula, rule formula, document formula.... Also, the the current core safeness definition specifies condition formula) 1st bullet: I think you should be more precise about "the quantifiers are moved out of f" - say where they are moved to, e.g. that f becomes an existentially quantified formula, if it wasn't already one? - if there are 2 exists subformulas, will there be 2 exists outside after the transform? 2nd bullet: resuling --> resulting Definition (boundedness) ----------------------------------- 1st sentence: formula --> condition formula boundedness of an external term is defined but never used in the definition of safeness (which only refers to boundedness of variables). do you also need to define boundedness of a variable in an equality formula and in an external predicate -- in case those occur in a disjunct, those definitions will be needed to evaluate the definition of a bound variable in a disjunction formula? 2nd sentence: mentions subclass formulas but they don't exist in Core. e, , --> e, Definition (safeness) ----------------------------- Formulas: 1st sentence: formula --> condition formula Safe existentially quantified formulas are not defined? RIF-Core rule: 1st bullet: ground or fact aren't defined in Core, BLD or FLD (they mention "variable free atomic formula" and universal fact) so it's a change of terminology for a reader who is only referring to those documents. 2nd bullet: occurs in b --> occur in b 3rd bullet: an universal rule --> a universal rule General: when replacing the section in Core, I think it's useful to keep the first sentence of existing section 6.1. Stella On Tue, Jun 9, 2009 at 10:33 AM, Christian De Sainte Marie <csma@fr.ibm.com>wrote: > > ********* NOTICE ********** > My new email address at IBM is: csma@fr.ibm.com > My ILOG email address will not be forwarded after June 8 > ***************************** > > </Chair> > > All, > > From my initial definition in PRD, which is too complex, and from the > definition in Core, which does not extend naturally to PRD, as Gary's > attempt shows, I derived a bottom-up definition of safeness and boundedness > in Core, that, I think, is correct (in the sense that it is equivalent to > the definition currently in Core) and that extends very easily to PRD [1]. > > [1] http://www.w3.org/2005/rules/wiki/PRD_Safeness_Bottomup > > Jos agreed that, if that definition is, indeed, correct, we should use it > in Core instead of the current one (and thus in PRD as well). > > But he is not is a shape, today, to check the equivalence of his definition > in Core and the bottom-up one... > > He said he would look at it tomorrow, but if you all could review it as > well, in the meantime, that would help. > > 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 15:56:26 UTC

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