Re: [Core][PRD] Definition of safeness

Axel Polleres <axel.polleres@deri.org> wrote on 17/06/2009 15:34:53:
> 
> fair enough, if no one else has a problem with that I am ok to back off 
> with that concern, since, admittedly, I find your definition easier to 
> grasp in general. As far as I can see so far, (i) it does the job and 
> (ii) it also seems independent from the definition of strong safeness 
> (those are my two main concerns, did you check that as well Christian?, 
> Jos?), so it seems replaceable.

Re strong safeness: I checked, and the only dependency is that the 
definition of the dependency graph mentions "...any A in B_psi..." once.

I see two possible fixes:
- one is to add the definition of B_psi from Jos's definition in the 
section on strong safeness. That would require some editing, because Axel 
uses the same symbols, E and L, as Jos for edges and labels, but for a 
different graph; but Jos's E and L could simply be renamed E_psi and 
L_psi;
- the alternative is to define B_psi, in the definition of strong 
safeness, as the set of the sets of the atomic formulas that are conjuncts 
in each disjunct in psi in DNF (that sentence needs improving, of course, 
but it is quite late, here, and tomorrow is the deadline for my tax form 
and I have not started looking at it yet :-(

I suggest that we use the latter fix, if somebody can come up with 
sensible wording for it.

All the Core editors agreed on switching to the bottom-up definition: if 
there is no objection until tomorrow EOB, I will implement the change on 
Friday morning my time. If somebody comes up with a reasonably clear 
sentence to define B_psi wrt the sets of conjuncts in a DNF, I will add it 
in the definition of strong safeness; if not, I will copy, and edit as 
appropriate, the tree decomposition from the current definition of 
safeness.

Cheers,

Christian

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