Re: [Core][PRD] Definition of safeness

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
>