Re: [Core][PRD] Definition of safeness

Jos de Bruijn wrote:
> 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. 

I will try to jump in, but can't do anything before late tonite, 
unfortunately.

Axel

> On 15 Jun 2009, at 15:01, Christian De Sainte Marie <csma@fr.ibm.com 
> <mailto: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 <mailto: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
>>


-- 
Dr. Axel Polleres
Digital Enterprise Research Institute, National University of Ireland, 
Galway
email: axel.polleres@deri.org  url: http://www.polleres.net/

Received on Monday, 15 June 2009 18:44:04 UTC