Re: Motion 31 draft text V04.4, extra notes
Nate Hayes wrote, commenting about Ian McIntosh's Sept 2010 post:
> As he points out, the rules for floating-point arithmetic with +OVR are
> almost identical to the IEEE 754 rules for +Inf. For example:
> (+OVR) - (+OVR) = NaN and (+OVR) / (+OVR) = NaN
> but one important difference is:
> (+OVR) * 0 = 0
> as opposed to:
> (+Inf) * 0 = NaN
This is not a relevant argument here, as even with unbounded Level 1
intervals the the rules for arithmetic with infsup bounds are those
for OVR and not those for true Inf (as pointed out already in the
Vienna proposal). That's because Inf is never a member of an interval,
as per Motion 3.
In a separate post, Nate also wrote:
> We don't actually perform arithmetic in a computer at Level 1, ...
No, but we use the Level 1 specifications in proofs about programs
written at Level 2, taking Level 2 issues into account where necessary.
Hardly anything is *essential* in a world of Turing equivalences (or
mathematical modelling of one structure, e.g. Reals, by another, e.g.
sequences of Rationals, subsets of Integers, etc.). That just leaves
issues such as elegance, ease of expression, and such.
Michel.
---Sent: 2012-04-14 21:31:54 UTC