Re: [Core][PRD] Definition of safeness

Jos,

I made some corrections to the bottom-up definition, already, based on 
your comments.

Jos de Bruijn <debruijn@inf.unibz.it> wrote on 15/06/2009 12:35:05:
> 
> - 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)

Corrected.

> - in the definition of bound, it is unclear what f\e and f\a are.

I explicited f=And(c1...cn), and I replaced a and e by ci, and f\a and f\e 
by f' = And(c1...ci-1 ci+1...cn).

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

I implemented the easy fix (v is bound in an atom a iff a is a 
non-external, non-equality atom and v is an argument of a, or v is bound 
in the conjunction And(a).

> - the notion of labeled positions in binding patterns is not defined

I changed the wording to "the i-th position in a binding pattern is 'u'" 
(resp. 'b').

> - what is an equality formula involving two variables? is ?x=f(?y) one?
> This needs to be clarified.

Clarified to "an equality where the terms on both sides are variables".

> - it is unclear what is meant with "bound within the scope of their
> respective quantifiers"

I came back to your definition (all the variables that occur in the head 
are safe in the body, and all the variables that occur in the body are 
bound in the body),and added a comment, earlier, about the boundedness of 
existentially quantified variables, namely: "Notice that the variables, 
v1...vn, that are existentially quantified in an existential formula f = 
Exists v1,...vn (f'), are bound in any formula, F, that contains f as a 
sub-formula, if and only if the are bound in f, since thay do not exist 
outside of f; that is, even if F is a disjunction."

Is that better?

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