Re: [Core][PRD] Definition of safeness

Below are a few minor comments on the definition,

Stella

-------------------------------------------------------

 The definition of safeness of a variable in a condition formula doesn't
cover the case where the condition formula is an existential formula.

 Definition (Boundedness):

  1st sentence:
        "external term" --> "external function term", since earlier
        in Core (2.3) external term is defined to mean external
        function or predicate.

    2nd sentence:
        if *an* only if --> if and only if

    Last para:
        what is the significance of  "...that is, even if F is a
disjunction" at the end?


Definition (Safeness):
   3rd para: (groups)
        if *an* only if --> if and only if

   4th para: (documents)
       if and only if *it* -> if and only if




On Wed, Jun 17, 2009 at 5:24 PM, Christian De Sainte Marie
<csma@fr.ibm.com>wrote:

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