John's position paper...
Folks,
I like John's very sound approach to prits. Sound both in
its mathematical foundation & our ability to implement it.
Let me mention a few things.
John mentions "the Zuras definition of 'bounded'".
So far, as I recall, I have confined my discussion of that
to private conversations between John & I.
No matter. It is a simple concept. That is, I would like
a definition of 'bounded' that roughly follows the IEEE-754
definition of overflow. That would be "For all x in X, f(x)
evaluated in the current working precision & rounded away
from zero does (or does not) overflow to an infinity". It
sounds like a 'for all' to me but feel free to quantify &
negate to taste.
The idea was that one cannot always know if a function has
a pole in it if one is confined to evaluatiing it on a
computer. Indeed, if eps > 0 is small enough such that
1/eps^2 overflows in our working precision then the functions
1/(x^2 + eps)^2, 1/x^4, 1/(x^2 - eps)^2 have 0, 1, & 2 poles,
respectively, in spite of the fact that they are virtually
indistinguishable from each other throughout that portion of
their domain that returns finite results.
Thus, a 'bounded' that can be easily evaluated on a conputer
seems the most natural to me. In my discussions with John,
we knocked around the names large, range, overflow, bounded,
& finite to describe this sort of thing. I think I favored
range or inRange on grounds of least baggage.
I have a similar notion that applies to underflow but now
is not the time to go into that.
John & I also kicked around wellFormed & illFormed as names
for valid or invalid. This is NOT equivalent to the 754
invalid & so needs another name.
My objection to an earlier form of John's continuous prit
involved one-sided continuity for functions like sqrt() at
zero & the like. John neatly solves this problem with the
phrase "and f(x) is defined". This also solves his problem
with things like the floor() function when evaluated on an
interval that is bounded by one of its discontinuities.
Finally, John & I considered a form of the defined prit which
was just a bit like "for all x in X, f(x) is defined" together
with the predicate isEmpty(). It came out that all 4 of the
needed states (all in, some in & some out, all out, & empty)
were possible with a 'defined' bit together with isEmpty().
But I like John's blue & red bits. Much neater. It may take
some getting used to but its simpler in the end.
IMHO, of course.
Yours,
Dan