Re: [Core][PRD] Definition of safeness

Axel,

Thanx for the comments.

Axel Polleres <axel.polleres@deri.org> wrote on 16/06/2009 10:33:45:
> 
> *
> "A variable, v, is bound in an atomic formula, a, if an only if
> [...]
> or v is bound in the conjunction formula f = And(a)."
> 
> I get the intention, though it is a bit hard to grasp, admittedly.
> Maybe better to have separate bullets for External terms and
> equalities for atomic formulas, but well, it works, I think.

Well, I did the change yesterday, on Jos's request... But the separate 
bullets for External terms and equalities for atomic formulas are only 
commented out, so, if you prefer to have them...

Your choice :-)

> *
> "or v occurs as the i-th argument in a conjunct, ci, that is an 
> externally defined predicate, and the i-th position in a binding pattern 

> that is associated with ci is u, and all the arguments that occur, in 
> ci, in positions with value b in the same binding pattern are bound in 
> f' = And(c1...ci-1 ci+1...cn);
> 
> index confusion, it seems. guess i should be replaced by j when talking 
> about the argument position:

Ooops, yes, your are right, of course! I added the two indices at two 
different times, yesterday, and I did not even think of checking that I 
was using different symbols...

Corrected.

> *
>  >>> Do you mean that we need to specify the rewriting to DNF? Isn't
>  >>> pointing to a textbook enough? I mean, is not that considered basic
>  >>> knowledge?
> 
> I would think it is ok to assume that. The potential blowup is a bit 
> nasty, though.

I do not get you: what blowup are you talking about? The size of the 
section if we add a specification of disjunctive form normalization? That 
would go in an appendix, I guess.

You did not conclude: after looking at the bottom-up definition, what is 
you opinion wrt switching definitions in Core?

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