Re: [Core][PRD] Definition of safeness

I had a quick look for now.

*
"A variable, v, is bound in an atomic formula, a, if an only if
[...]
or v is bound in the conjunction formula f = And(a)."

I get the intention, though it is a bit hard to grasp, admittedly.
Maybe better to have separate bullets for External terms and
equalities for atomic formulas, but well, it works, I think.


*
"or v occurs as the i-th argument in a conjunct, ci, that is an 
externally defined predicate, and the i-th position in a binding pattern 
that is associated with ci is u, and all the arguments that occur, in 
ci, in positions with value b in the same binding pattern are bound in 
f' = And(c1...ci-1 ci+1...cn);

index confusion, it seems. guess i should be replaced by j when talking 
about the argument position:

"or v occurs as the j-th argument in conjunct ci, that is an externally 
defined predicate, and the j-th position in a binding pattern that is 
associated with ci is u, and all the arguments that occur, in ci, in 
positions with value b in the same binding pattern are bound in f' = 
And(c1...ci-1 ci+1...cn);

*
 >>> 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?

I would think it is ok to assume that. The potential blowup is a bit 
nasty, though.

Axel

Axel Polleres wrote:
> 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 Tuesday, 16 June 2009 08:34:26 UTC