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

Date: Mon, 15 Jun 2009 19:44:24 +0200

Message-Id: <094DAEE4-3630-4E54-A5F9-89D795C82E2E@inf.unibz.it>

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

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

Date: Mon, 15 Jun 2009 19:44:24 +0200

Message-Id: <094DAEE4-3630-4E54-A5F9-89D795C82E2E@inf.unibz.it>

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

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

Sorry, I cannot deal with this discussion right now. I commented on the proposal and said what I think is the best way forward. I leave it up to the editors of the Core document to decide how to proceed. Cheers, Jos On 15 Jun 2009, at 15:01, Christian De Sainte Marie <csma@fr.ibm.com> wrote: > > 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, 924 > 00 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 17:45:08 UTC

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