Re: [Core][PRD] Definition of safeness

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