Re: [Core][PRD] Definition of safeness

I had a brief look at the definition.

- 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)
- The transformations 1 and 2 are not specified in sufficient 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.
- in the definition of bound, it is unclear what f\e and f\a are.
- 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
- the notion of labeled positions in binding patterns is not defined
- what is an equality formula involving two variables? is ?x=f(?y) one?
This needs to be clarified.
- the terminology used for rules is not in line with the definitions in
BLD (e.g., a fact is not a rule)
- in general, the symbols you use are not in line with 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
- in the definition of safeness you forget to do the rewriting to
disjunctive normal form
- it is unclear what is meant with "bound within the scope of their
respective quantifiers"

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:
- remove definition of equivalence class
- replace definition of B_psi with (a proper definition of) rewriting to
disjunctive normal form
- changing the definition of boundedness so that equality of variables
is dealt with using rewriting (i.e., removing the equality from the
conjunct) rather than equivalence classes
- reversing the order of the definition of safeness of formulas (i.e.,
first safeness or facts, ..., then safeness of documents)
- introducing bullets here and there
- making everything coherent

Best, Jos

Christian De Sainte Marie wrote:
> Jos,
> What is your opinion wrt the definition of safeness? Should we switch to
> the bottom-up definition [1], now that it has been reviewed and
> improved, or shall we stick by yours?
> I am trying to get a feeling of what the consensus might be, esp.
> amongst the main stake holders (that is, you and the editors).
> Cheers,
> Christian
> [1]
> 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

+43 1 58801 18470

Jos de Bruijn,
Many would be cowards if they had courage
  - Thomas Fuller

Received on Monday, 15 June 2009 10:35:46 UTC