Re: [Core](PRD] safeness

********* NOTICE **********
My new email address at IBM is: csma@fr.ibm.com
My ILOG email address will not be forwarded after June 8
*****************************

Hi Stella,

Thanx for the detailled comments. Responses in-line.

Stella Mitchell <stellamit@gmail.com> wrote on 10/06/2009 17:55:49:
>  
> Here are some comments on the Safeness in Core section,
>  
>   1st para: (I know it's just copied over)
>       You could take out the "Intuitively" and just say "b stands 
> for "bound"..."

Done.

>   5th para: ("The definitions of boundedness...")
>        1st sentence:
>            formula --> condition formula ? 
>                 (for extra clarity because formula (in the math english)
>                  in Core is defined as atomic formula, condition 
formula,
>                  rule formula, document formula.... Also, the the 
current 
>                 core safeness definition specifies condition formula)

You are right. I replaced "formula" by "condition formula" everywhere the 
reference might have been ambiguous.

>        1st bullet:
>            I think you should be more precise about 
>            "the quantifiers are moved out of f"
>                - say where they are moved to, e.g. that f
>                  becomes an existentially quantified formula,
>                  if it wasn't already one?

Yes, indeed. I made that more precise. That was esp. needed to clarify how 
it extends to the case with negation (I am still working on that part).

>                - if there are 2 exists subformulas, will there
>                  be 2 exists outside after the transform?

As it is currently described, yes. They could be merged into a single one, 
but who cares? That would only make the description heavier, without 
changing anything to the definitions of boundedness and safeness.

>        2nd bullet:
>            resuling --> resulting

Done.
 
>   Definition (boundedness)
>   -----------------------------------
> ...
>       boundedness of an external term is defined but never
>       used in the definition of safeness (which only refers to
>       boundedness of variables). 

Yes, if all the variables are bound, then all the terms are bound, 
external or else.

The boundedness of an external term is used in the definition of the 
boundedness of a variable that occurs as an argument of an external 
predicate ("...and all the arguments that occur in positions marked 'b' 
are bound..."), or on one side of an equality ("...and the term on the 
other side is bound...").

>       do you also need to define boundedness of a variable in 
>       an equality formula and in an external predicate -- in case
>       those occur in a disjunct, those definitions will be needed to 
>       evaluate the definition of a bound variable in a 
>       disjunction formula?

I added the two cases that, 
- v is bound in an equality if it occurs as the argument on one side of 
the equality, and the term on the other side is variable free;
- v is bound in an external predicate if it occurs as an argument in a u 
position, and all the terms in b positions are variable free.

>       2nd sentence:
>            mentions subclass formulas but they don't exist in Core.

Ooops! Right. I change the sentence to correct that (and still keep is 
valid for PRD, that has subclass).
  
>       e, , --> e, 

Done

>   Definition (safeness)
>   -----------------------------
>    Formulas:
>       1st sentence:
>            formula --> condition formula
>  
>       Safe existentially quantified formulas are not defined?

Safe formulas are not defined, except for safe rules (and rule compounds). 
They are not nedeed.

>    RIF-Core rule:   
>      1st bullet: 
>          ground or fact aren't defined in Core, BLD or FLD
>          (they mention "variable free atomic formula" and universal
>          fact) so it's a change of terminology for a reader 
>          who is only referring to those documents.

Right. Corrected.

>      2nd bullet:
>          occurs in b --> occur in b
>  
>     3rd bullet:
>          an universal rule --> a universal rule

Oh! Why is that? Isn't the liaison added in every case 'a' precedes a 
vowel? Is that because of the unpleasantly sounding "an uni..." (oniony 
versal rule? What are oniony versal rules?)?

Corrected, anyway.

>   General: when replacing the section in Core, I think it's 
>   useful to keep the first sentence of existing section 6.1.

Absolutely agree. I copied it.

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