I meant the type should be <br><br>val roundFromString : IEEEReal.rounding_mode * string -> real option<br><br><div><span class="gmail_quote">On 7/27/07, <b class="gmail_sendername">Matthew Fluet</b> <<a href="mailto:fluet@tti-c.org">
fluet@tti-c.org</a>> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>On Fri, 27 Jul 2007, Sean McLaughlin wrote:<br>> As for interval arithmetic, a main concern of mine is that
<br>> the sqrt function rounds correctly given the rounding mode, as specified<br>> in IEEE754.<br><br>The other aspect that I was wondering about was floating-point constants.<br>That is, what should the following program do:
<br><br>val mtenth_lo = (down(); 0.1)<br>val mtenth_hi = (up(); 0.1)<br>val mtenth_near = (near(); 0.1)<br>val mtenth_zero = (zero(); 0.1)<br><br>val _ = print(word8vectorToString (P.toBytes mtenth_lo) ^ "\n")<br>
val _ = print(word8vectorToString (P.toBytes mtenth_hi) ^ "\n")<br>val _ = print(word8vectorToString (P.toBytes mtenth_near) ^ "\n")<br>val _ = print(word8vectorToString (P.toBytes mtenth_zero) ^ "\n")
<br><br><br>A very strict reading of The Definition says that special constants are<br>evaluated as part of the dynamic semantics, yielding "a value according to<br>normal mathematical conventions". However, the function from special
<br>constants to values is:<br> val : SCon -> Val<br>and the evaluation rule is:<br> E |- scon => val(scon) (90)<br>which suggests that the meaning of the special constants are not dependent<br>upon the dynamic state. On the other hand, the function from primitive
<br>functions and arguments to values is:<br> APPLY : BasVal * Val -> Val + Pack<br>and the evaluation rule is:<br> E |- exp => b E |- atexp => v APPLY(b,v) = v'/p<br> ---------------------------------------------------
<br> E |- exp atexp => v'/p<br>which also suggests that primitives are pure functions, not dependent upon<br>the dynamic state. Since Real<N> arithmetic already steps outside of<br>this, the question arises as to whether the evaluation of real constants
<br>should also step outside this.<br><br><br></blockquote></div><br>