Re: [Core][PRD] Definition of safeness

Christian De Sainte Marie wrote:
> 
> 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?

blowup for naive normal form DNF transformation is potentially 
exponential in the formula size... which makes me a bit nerveous, if the 
definition contains such a potentially expensive operation. Thus...

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

...I am reluctant, see above.

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


-- 
Dr. Axel Polleres
Digital Enterprise Research Institute, National University of Ireland, 
Galway
email: axel.polleres@deri.org  url: http://www.polleres.net/

Received on Tuesday, 16 June 2009 13:40:18 UTC