Re: Motion 31 draft text V04.4, extra notes
Michel Hack wrote:
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
I understand. But this is why it is relevant since it means i) choosing
between OVR and Inf is a design choice and ii) switching to OVR would not
actually represent a significant amount of "churn" from where P1788 is
currently at.
Vienna proposal). That's because Inf is never a member of an interval,
as per Motion 3.
I agree that OVR and Inf are practically the same under this interpretation
except that OVR is a Level 2 concept and Inf is Level 1. All intervals at
every level are also closed and bounded with the OVR model.
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.
Ok. So lets drop the pretense unbounded intervals are necessary or
essential, then, and recognize there is a design choice to be made here. I
think the most scientific approach would be to study the merits of each
choice and compare the pros and cons. This is what we're trying to do
offline here at Sunfish... the reason I haven't made a motion or even
presented a position paper is because we're not finished doing this. But it
is one of the reasons I've been asking questions.
Nate