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
place.
- 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] http://www.w3.org/2005/rules/wiki/PRD_Safeness_Bottomup
> 
> 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        debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
Many would be cowards if they had courage
enough.
  - Thomas Fuller