- From: Christian De Sainte Marie <csma@fr.ibm.com>
- Date: Mon, 15 Jun 2009 15:01:41 +0200
- To: Jos de Bruijn <debruijn@inf.unibz.it>
- Cc: RIF <public-rif-wg@w3.org>
- Message-ID: <OF0EB79A21.CC75448C-ONC12575D6.00440973-C12575D6.004790D1@fr.ibm.com>

Hi Jos, Thanx for the comments. Can I infer that the bottom-up definition is equivalent to yours, once all your comments are taken into account? Responses to yu comments are in-lined, below. 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) Easy to fix: that is only typography. > - The transformations 1 and 2 are not specified in sufficient detail. Can you point more precisely where they are ambiguous and need be specified in more detail? > This is easy to fix; they essentially mean to do the same thing as the > collection B_psi I defined. In fact, I guess rewriting to disjunctive > normal form is probably easier to understand for many readers than the > tree decomposition I defined. Of course, it needs to be specified. Do you mean that we need to specify the rewriting to DNF? Isn't pointing to a textbook enough? I mean, is not that considered basic knowledge? > - in the definition of bound, it is unclear what f\e and f\a are. Yep. Laziness... Easy to correct, though: it means conjunction, f, minus the conjunct, e (or a), of course. > - 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. Well, of course, this is feasible. It just seemed eaiser to read and understand if the two cases where handled separately (variable-free and variables bound elsewhere in the formula). An easy fix, that does not require the introduction of equivalence classes or whatever, is to describe only the conjunction case, and say that an atomic formula is handled as a conjunction with a single conjunct. > - the notion of labeled positions in binding patterns is not defined Laziness again: as you probably guessed, it was shorthand for "...the i-th postion in the binding pattern is 'u'..." (or 'b', whateber). Easy to correct, too. > - what is an equality formula involving two variables? is ?x=f(?y) one? > This needs to be clarified. "Equality involving two variables" is something I copied from your definition... I understood that it meant that the term on each side of the equality was a variable. It can be made precise easily, of course. > - the terminology used for rules is not in line with the definitions in > BLD (e.g., a fact is not a rule) Did you read the latest version, after I took Stella's comment into account? The terminology is that of BLD, I think. > - in general, the symbols you use are not in line with the symbols we > use for rules and condition formulas I do not understand the comment: can you explain what are "the symbols we use for rules and condition formulas"? > - safeness of document and group formulas can be written more concisely, > see the way I defined them Your definitions are, indeed, more concise, but they seemed ambiguous, to me, which is why I completed them: - you omit the case of an empty group (without saying whether it is safe or not), - and you say nothing about imports (is a document that contains a safe group but that imports a document that contains an unsafe one safe?). But I may be wrong. If your definitions are not ambiguous, of course, they should be used. > - in the definition of safeness you forget to do the rewriting to > disjunctive normal form I do not understand what you mean. The text says that "the definitions of boundedness and safeness, below, apply to a condition formula, f, after it has been simplified syntactically ..." Do you mean that it should be repeated befor ethe definition of safeness? > - it is unclear what is meant with "bound within the scope of their > respective quantifiers" Is it? How would you say that each existentially quantified variable must be bound in the formula that is in the scope of its quantifier? > I think the best way to proceed is to change the definition that are > currently in Core to bring them in line with the kind of definition I > think you want, by doing the following: > [...] If you have, really, no other comments, do not you think that it is easier, instead, to make all the corrections that you request in the bottom-up definition? My point is that, if we rewrite the top-down definition the way you suggest, we will end up with a whole new definition again, that we will have to review, and from which we will have to derive the correct extension for PRD, whereas, with your and Stella's review of the bottom-up definition, we have one that seems to be correct and sufficient for our purpose, and for which we have a very simple extension for PRD... What do you think? 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 Monday, 15 June 2009 13:02:57 UTC