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

Date: Mon, 15 Jun 2009 16:40:27 +0200

To: Jos de Bruijn <debruijn@inf.unibz.it>

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

Message-ID: <OF6C90601C.8C18624B-ONC12575D6.0049F8DC-C12575D6.00509BE1@fr.ibm.com>

Date: Mon, 15 Jun 2009 16:40:27 +0200

To: Jos de Bruijn <debruijn@inf.unibz.it>

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

Message-ID: <OF6C90601C.8C18624B-ONC12575D6.0049F8DC-C12575D6.00509BE1@fr.ibm.com>

Jos, I made some corrections to the bottom-up definition, already, based on your comments. Jos de Bruijn <debruijn@inf.unibz.it> wrote on 15/06/2009 12:35:05: > > - the use of fonts is inconsistent. Sometimes you use two different > fonts (e.g., times and teletype) to refer to the same thing (e.g., b in > the definition of rule safeness) Corrected. > - in the definition of bound, it is unclear what f\e and f\a are. I explicited f=And(c1...cn), and I replaced a and e by ci, and f\a and f\e by f' = And(c1...ci-1 ci+1...cn). > - there is unnecessary duplication between the definitions of > boundedness in atomic formulas and conjunctions; these two definitions > should be compounded. This is the reason I compounded them in the first > place. I implemented the easy fix (v is bound in an atom a iff a is a non-external, non-equality atom and v is an argument of a, or v is bound in the conjunction And(a). > - the notion of labeled positions in binding patterns is not defined I changed the wording to "the i-th position in a binding pattern is 'u'" (resp. 'b'). > - what is an equality formula involving two variables? is ?x=f(?y) one? > This needs to be clarified. Clarified to "an equality where the terms on both sides are variables". > - it is unclear what is meant with "bound within the scope of their > respective quantifiers" I came back to your definition (all the variables that occur in the head are safe in the body, and all the variables that occur in the body are bound in the body),and added a comment, earlier, about the boundedness of existentially quantified variables, namely: "Notice that the variables, v1...vn, that are existentially quantified in an existential formula f = Exists v1,...vn (f'), are bound in any formula, F, that contains f as a sub-formula, if and only if the are bound in f, since thay do not exist outside of f; that is, even if F is a disjunction." Is that better? 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 Monday, 15 June 2009 14:42:02 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 15 June 2009 14:42:03 GMT
*