Re: about emp (was: Motion 42: NO)
On 2013-02-13 11:05:37 +0100, Guillaume Melquiond wrote:
> Le lundi 11 février 2013 à 03:07 +0100, Vincent Lefevre a écrit :
> > Because when considering decorations (and only in this case), reasoning
> > is based on the *point functions*, not their interval version. The point
> > function is here f(x) = sqrt(-x*x-1).
>
> You do not know that! Who said that the point function was f(x) =
> sqrt(-x*x-1)? Is there anything in the motion that prevents the point
> function from being f(x,y) = sqrt(-x*y-1)?
§6.1, paragraph "For instance..." implies that the expression
sqrt(y^2-1) + xy corresponds to the point function
f(x,y) = sqrt(y^2-1) + xy.
But more importantly, there is also text that is not part of this
motion, e.g. Section "Expressions and the functions they define".
> Do not forget about this fundamental principle of modern programming
> languages, "referential transparency", which basically states that, if
> the call to a function has no side effect, then it can be replaced by
> its result. (This is the idea behind numerous compiler optimizations:
> constant propagation, common subexpression elimination, and so on.)
But you don't have just functions calls. You have expressions (which
can be large parts of code), and it is well-known that expressions may
be allowed to be rewritten by the implementation with the effect that
the result is changed.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)