Re-submitting as motion 6
P1788 members
I hereby re-submit my motion as Motion 6, as asked by the Chair.
(Motion 5 remains as the Einarsson Kulisch motion.) Apart from the
number change, the text of motion & rationale is the same. I have
already had a number of useful suggestions, and will issue an amended
version as M0006.02 shortly.
Best wishes
John Pryce
================================================
===Motion P1788/M0006.01_Level_2_Multi-format===
Proposer: John Pryce
Seconder: Dan Zuras
===Cross-referencing notation===
Clauses of the motion are labelled M1, M2, etc. The rationale is
divided into sections labelled R1, R2 etc., with subsections R1.1,
R1.2, etc. Definitions are within R3, but are labelled D1, D2, etc.
===Motion text===
P1788 shall support multiple-format interval arithmetic. Specifically:
M1. The terms "interval format", "interval datum" etc., shall have
the meanings given in the Definitions and Rationale.
M2. An implementation shall specify which interval formats it
supports (it is permitted to support only one). Support consists of
the following two items.
- For each supported interval format, operations (as P1788 will in
due course specify) shall be provided, to at least SRSF level - see
R6.6.
- Conversions shall be provided between any two supported interval
formats - see R6.5.
M3. An implementation shall be called 754-conforming if: (i) its
underlying system is 754-conforming (Definition D1) and the
implementation supports an interval format for each supported
floating-point format; or (ii) it is functionally indistinguishable
from case (i).
[Note. The reason for case (ii) is that it seems feasible to code an
efficient 754-conforming interval system using only a subset of 754
floating point features. If so, a floating point system that behaves
differently from 754 outside this subset can be used. For example, a
system that has only one kind of zero.]
M4. A 754-conforming implementation shall provide SRMF interval
support to the same extent that the underlying floating point
provides "formatOf" operations, see R6.6. It may support interval
formats outside the basic five (binary32, binary64, binary128,
decimal64, decimal128), such as extended or extendable, see 754/3.7.
M5. An implementation shall document:
- What interval formats are supported.
- What interval versions of elementary functions are provided in a
given format.
- For each such version:
* a sharpness measure, as P1788 will decide (e.g. Vienna's "tight",
"accurate", "valid");
* the level of mixed-format support, SRSF or SRMF; and just what
operand
interval formats are supported in the SRMF case.
===Rationale===
===============
This divides into Foundations; Terminology and Notation; Definitions;
Overall Aims; Level 1 description; and Level 2 description.
R1. Foundations.
----------------
Motion 2 and the associated position paper PP008, defining a levels
structure as a guideline for the standard.
Motion 3, which defines P1788's number system and set of intervals.
R2. Terminology and Notation.
-----------------------------
754/X denotes section X in the standard IEEE754-2008. Vienna/X stands
for section X in the final version of the Vienna proposal, 19
December 2008.
Motion 3 decided that the P1788 intervals comprise the closed
connected subsets of the reals. In the (provisional) interval
notation decided by Motion 1 this is denoted (IR), so I use that
here. But I think it is outdated, and hope we will soon decide to use
IR instead. IR currently denotes the _bounded_ intervals.
Usually, point values are denoted by single-character names x, y, ...
and intervals by double-character names xx, yy, ...
The characters ^ and _ are to be read as indicating superscript and
subscript, as in TeX, but without TeX's braces. E.g. read log_b64 as
the name "log" with a subscript "b64", meaning the binary64 (floating
point or interval) logarithm function.
R3. Definitions.
------------
These are intended to be rewritten into a standard set of
definitions, abbreviations and acronyms of this standard. I have put
them into alphabetical rather than logical order (as in 754 section
2) for ease of looking up. Please bear with the fact that some of
them are currently just forward references.
D1. "754-conforming system". A "754-conforming system", or "754
system" for short, is a programming environment that provides
floating point arithmetic conforming to IEEE754-2008.
[Note. A hardware processor (e.g. the Cell processor) may not be
754-conforming in itself, but a 754-conforming system may be built on
it with software assistance.]
D2. "Aformat" (abstract floating point format) and "aformat
associated to a concrete format". See R6.1.
D3. "Basic operations". The five elementary functions + - * / and sqrt.
D4. "Concrete (floating point) format". A floating point format
associated with a particular representation and encoding, such as
754's binary64.
D5. "Interval datum", "F-interval datum". See R6.3.
D6. "Interval elementary function". An interval version of a point
elementary function, that is provided by an implementation. The set
of these is the implementation's "interval elementary function
library" ("interval library" for short). These terms may be qualified
by a format, e.g. "binary64 interval library".
D7. "Interval format". An "infsup interval format" means the set (IR)
_F of F-intervals for some floating point (abstract) format F, as
defined in R6.2. When used without qualification, "interval format"
means an infsup format -- by contrast with, say, a midrad (midpoint-
radius) format. An implementation "supports" such a format (IR)_F if
it provides an (abstract) data type whose valid values are precisely
the F-intervals, possibly together with NaI.
D8. "Interval function", "interval mapping". A function from
intervals to intervals is called an "interval function" if it is an
interval extension of a point function, and an "interval mapping"
otherwise. See R5.5.
D9. "Interval-supported". A point function is "interval-
supported" [resp. "F-interval-supported" for some aformat F] if an
interval extension of it exists in the interval library [resp. F-
interval library].
[Note. An interval-supported function need not be in the point
library. A function in the point library need not be interval-
supported.]
D10. "Interval version" of a point function means the same as
"interval extension"; often with an indication of its operand and
destination formats, as in "binary64 SRMF interval version".
D11. A "mixed-format" interval arithmetic operation is one where the
formats of the operand interval(s) and the destination interval may
not all be the same.
[Note. It does not mean that the lower and upper bounds of an
individual interval can have different floating point formats. The
theory, as phrased here, precludes this.]
D12. "Multiple-format" interval arithmetic supporting arithmetic in
more than one interval format, and conversions between these formats.
[Note. SRSF, SRMF and MRMF interval support are all multiple-
format (if more than one interval format is supported); SRMF and
MRMF, but not SRSF, are mixed-format.]
D13. "Point elementary function". A point function, in the sense of
R5.4, that is provided by an implementation. The set of these is the
implementation's "point elementary function library" ("point library"
for short). These terms may be qualified by a format, e.g. "binary64
point library". The arithmetic operations + - * / count as elementary
functions.
D14. "Sharpness measure". A way to describe the quality of an
interval version of a function: for instance the "tight", "accurate",
"valid" scheme in Vienna/3.2.
R4. Overall Aims.
-------------
Ramon Moore's Basic Theorem of Interval Arithmetic (BTIA) is
fundamental to interval computation. Roughly, it says that if E is an
explicit real expression defining a real function f(x_1, ..., x_n),
then evaluating E "in interval mode" over any interval inputs
(xx_1, ..., xx_n) is guaranteed to give an enclosure of the range of
f over those inputs.
This motion has two linked aims. Aim 1 is to define a framework for
finite precision interval arithmetic in multiple formats. In this
framework the BTIA is easily proved -- indeed almost obvious. The
finite precision interval operations are defined to operate on a set
of abstract objects that happens -- except for Not an Interval, NaI
-- to be a finite subset of the infinite set (IR). The definition of
operations is independent of any representation that may be chosen
for intervals.
The framework should support mixing intervals of different formats in
arithmetic expressions, as well as potential compile-time "exact
denotations" of intervals such as pi + [-0.1,0.1]. However, this
motion does not commit P1788 to any stance on such issues.
[Note: To simplify wording I am assuming P1788 defines an NaI object.
Personally I support NaI; editorially I have no preference; and NaI
is peripheral to the argument.]
This is exactly analogous to how 754 defines the finite precision
point operations, on a set of abstract objects that happens -- except
for -0, +0 and NaN -- to be a finite subset of the extended real
numbers.
The abstract objects and operations form interval level 2. To see its
utility, ask yourself the question "How to prove the BTIA, starting
from a procedural definition of the arithmetic operations as given,
for instance, in the Einarsson-Kulisch position paper presently (May
2009) under discussion as Motion 5?" Answer: you cannot, _except_ by
passing through a stage equivalent, or closely related, to the
abstract objects and operations defined here. (This is no criticism
of these definitions: they have a different purpose.)
Aim 2 is to show that this abstract multiple-format arithmetic is,
for the most frequently used operations, easy to implement
efficiently on a 754 system, by exploiting two features of the 754
standard:
- Every floating point computational operation (754/2.1.11) has a
defined
destination format.
- The basic operations + - * / and sqrt are "formatOf" operations
(754/5.1
and /5.4.1), which means that the correctly rounded result is
produced
for any operands _of the same radix_ as the destination format.
This makes mixed-format interval arithmetic for the basic operations,
between formats of the same radix, only slightly more work to
implement sharply (i.e., with tightest possible enclosures for each
individual operation) than is single-format interval arithmetic.
Mixed-radix is less easy, as there is no one best way to do the
needed radix conversions. In my view it should not be considered.
In summary, Level 2, as defined here, has a precise relation to the
mathematical level 1, that is easily grasped and easily reasoned
about. It also offers -- to turn this into reality is the job of
implementers -- a precise and easily grasped relation to the
representation/algorithmic level 3. Hence it provides a layer between
mathematics and implementation that will be crucial for proving the
correctness of this standard, and of programs built upon it.
R5. Level 1 description.
------------------------
This section recapitulates matters at the mathematical level that
have, I believe, already been decided. The notation is similar to the
Vienna proposal's, which is suitable for a plain-text document such
as this.
I believe nothing in this motion and rationale hinders the
implementation of various forms of non-standard intervals -- Kahan,
modal, etc. -- as discussed at the end of Vienna/1.2. It is
incompatible with certain _representations_, e.g., with a finite
precision midrad (midpoint-radius) representation of intervals,
though there is nothing to stop an algorithm using midrad form
internally.
R5.1. R is the set of reals. R* is the set of extended reals
R* = R union {-oo, +oo},
where we use -oo and +oo to denote negative and positive infinity.
Using the terminology of 754 (see /2.1.25 and elsewhere), any member
of R* is called a number: it is a "finite number" if it is in R, else
an "infinite number".
R5.2. Following Motion 3, the set of "textbook" intervals (Vienna/
1.2) in R,
denoted (IR), comprises the empty set together with all nonempty
intervals
xx = { x in R | xlo <= x <= xhi }, denoted [xlo, xhi],
where -oo <= xlo <= xhi <= +oo.
Square bracket notation xx = [xlo, xhi] is used in all cases, for
simplicity. However the above definition implies -oo and +oo are
never
members of an interval. The traditional round bracket notation may
be used
for specific intervals with an infinite end point, e.g. [2, +oo)
instead
of [2, +oo].
The requirement that xx be nonempty implies xlo cannot be +oo, and
xhi
cannot be -oo, so I regard [-oo, -oo] and [+oo, +oo] as having no
meaning
(rather than being empty).
The empty set is denoted by Empty. The whole of R is denoted by
Entire.
R5.3. The (interval) hull of an arbitrary subset ss of R, written hull
(ss),
is the tightest member of (IR) that contains ss.
(The "tightest" set with a given property is the unique one that is
contained in all other sets having that property. In many areas of
mathematics, "smallest" is used with the same meaning.)
R5.4. A "point function" is a (possibly partial) multivariate real
function:
that is, a mapping f from a subset D of R^n to R^m for some
integers n >= 0,
m > 0. (When n=0 and m=1, we have a "named real constant".)
When not otherwise specified, a scalar function is assumed, i.e.
m=1. If m>1,
the function is called a vector function.
D = D_f is the domain of f.
To specify n, call f an "n-variable point function", or denote f as
f(x_1, ..., x_n).
The "range" (often called "exact range" in the literature) of f over
an arbitrary subset ss of R^n is the set
range(f, ss) = {f(x) | x in ss and x in D_f}.
Notes.
- Here, f is a mapping, not an expression.
- For instance range(sqrt, [-1,1]) = [0,1]. We follow the convention,
usual in mathematics, that when evaluating over sets, points
outside
D_f are simply ignored. The Kulisch-Einarsson position paper on the
basic operations (May 09) makes the same definition.
- For the 754 policy on evaluating point functions outside the
domain,
see 754/9.1.1.
R5.5. Unless otherwise specified, an "interval mapping" is a mapping
ff from
(IR)^n to (IR)^m for some n,m >= 0. To specify n, call ff an "n-
variable
interval mapping", or denote ff as
ff(xx_1, ..., xx_n).
As with point functions, m=1 is assumed unless specified otherwise.
An interval mapping is called an "interval function" if it is an
interval
extension of some point function, as defined next. Examples of
interval
mappings that are not interval functions are the interval hull and
intersection operations.
Given an n-variable point function f, an "interval extension" of
f, also
called an "interval version" of f, is any interval function ff
such that
ff(ss) contains range(f,ss) for any subset ss of R^n.
The "sharp interval extension" of f is defined by
ff(ss) = hull(range(f,ss)) for any subset ss of R^n.
Equivalently, for the case where ff has separate arguments
ss_1, ..., ss_n,
each being a subset of R, an interval extension satisfies
ff(ss) contains range(f,ss_1, ..., ss_n),
and the sharp interval extension satisfies
ff(ss_1, ..., ss_n) = hull(range(f,ss_1, ..., ss_n)),
for any ss_1, ..., ss_n.
This is an alternative notation for the case where ss is the
cartesian
product of the ss_i.
When f is a binary operator "op" written in infix notation, this
gives
the usual definition of its (sharp) interval extension as
xx op yy = hull({x op y | x in xx, y in yy, and x op y is
defined}).
Notes.
- Example. With these definitions
xx * {0} = {0} and xx / {0} = Empty, for any nonempty interval
xx.
- All interval functions used here are automatically defined for all
arguments -- e.g. for the sharp extension of "point sqrt",
sqrt([-1,4]) = [0,2], sqrt([-2,-1]) = Empty.
R6. Level 2 description.
--------------------
R6.1. A floating point "abstract format" ("aformat") F is a finite
subset of R*
such that at least -oo and +oo are elements of F.
A format in the 754 sense (a "concrete format") shall be
identified with
the aformat comprising those extended-real numbers that are exactly
representable in that format, where -0 and +0 both represent 0.
This is
the aformat "associated to" the concrete format.
Notes.
- In view of this definition, 754's -0 and +0 are considered
identical.
Also, in 754 decimal formats, numbers in the same cohort are
considered
identical.
- For examples, we use the abbreviations b64 to mean 754's 64-bit
binary
format, b32 for 32-bit binary, and d64 for 64-bit decimal.
R6.2. An "interval format" is the set (IR)_F of "F-intervals" for
some aformat
F, comprising the empty set together with all textbook intervals
whose
endpoints are in F. When it is necessary to distinguish, it is
called an
"infsup interval format" by contrast to, say, a "midrad interval
format".
Notes.
- Clearly an aformat uniquely determines an interval format (also
vice
versa), and a 754 concrete format uniquely determines an aformat.
- An example of a possibly useful aformat that is not associated to a
concrete format (but is derived from one), is a "flush
underflows to
zero" interval system. Say the concrete format is binary64. Then
the
nonempty intervals are those whose endpoints belong to F, which is
defined to consist of all binary64 numbers that are not subnormal.
Such a system may give speed advantages on some architectures.
- This definition implies some form of infsup, that is (lower bound,
upper bound) representation at level 3. Variants of this exist, see
for instance Vienna/1.6.
- It also implies that it is not just wrong, but actually
meaningless at
this level, to speak of an interval that has NaN as an endpoint
or has
its lower bound greater than its upper bound.
R6.3. An "F-interval datum", by analogy with the definition of
floating-point
datum in 754/3.2, is either
- an F-interval; or
- the abstract object NaI, "Not an Interval".
An "interval datum" is an F-interval datum of any relevant aformat F.
Note.
At this level we consider there is just one NaI for all aformats;
at the
representation level this will probably not be the case.
My view of the purpose of NaI is that it is like NaN in floating
point
computation: if any operand to an operation is NaI, the result is
NaI. Not everyone agrees with this definition, but this
controversy is
peripheral to multiple-format issues, so from now on it is assumed
that
no operand to an operation is NaI.
R6.4. The (interval) F-hull of an arbitrary subset ss of R, written
hull_F(ss),
is the tightest F-interval that contains ss.
Notes.
- The set hull_F(ss) always exists, because F is finite and
contains -oo
and +oo.
- Always, hull_F(ss) contains hull(ss). If aformat G contains
aformat F
in the sense of subsets of R* -- equivalently in the 754 case,
if format
G is wider than F in the sense of 754/2.1.36 -- then hull_F(ss)
contains
hull_G(ss).
R6.5. Interval format conversion.
If F is an aformat, the "conversion" to format F shall mean the
operation
that maps an interval xx of any other supported format to its F-hull,
yy = hull_F(xx).
<754>This interval operation can in all cases (whether xx has the
same radix
as F or not) be implemented in terms of one of the floating point
operations
formatOf-convertFormat
defined in 754/5.4.2, with the appropriate outward rounding.
</754>
R6.6. Interval elementary functions: some options.
The Basic Theorem of Interval Arithmetic (BTIA) relies on each
point elementary function e in a real expression being replaced by an
"interval version", ee. Mathematically, ee can be an arbitrary
interval version of e, and its arguments and result are not limited
by any concrete interval format.
Practically, a level 2 "interval version" must be implemented at
level 3 in terms of concrete formats such as binary64. Typically, ee
is coded to deliver a result of a _specified_ format, from operands
of a _limited number_ of formats. What should multiple-format support
mean? Let F be a supported interval format, and e be an elementary
function. Three levels of support are suggested by the design of the
754 standard. In all of them, conversions as in R6.5 are provided
between all supported interval formats.
- Single-radix, single-format (SRSF).
In SRSF support, e has an interval version ee that takes F-
interval operand(s) and gives an F-interval result. Thus explicit
format conversion is needed for any operand of a different interval
format from F.
- Single-radix, mixed-format (SRMF).
In SRMF support, e has an interval version ee that takes operand
(s) of any supported interval format of the same radix as F, and
gives an F-interval result. Thus explicit format conversion is needed
for any operand of a whose interval format has a different radix from F.
- Mixed-radix, mixed-format (MRMF).
In MRMF support, e has an interval version ee that takes operand
(s) of any supported interval format, and gives an F-interval result.
Thus no explicit format conversion is required for any operand.
Clearly SRMF includes SRSF (SRMF support provides SRSF in
particular); and MRMF includes SRMF.
I believe (this is my personal view):
(a) A function being "interval-supported" should, in all cases,
mean at
least SRSF support.
(b) SRMF support is the interval equivalent of 754's "formatOf"
operations.
Therefore on a 754 system, SRMF support is appropriate for the
"formatOf" operations of 754/5.4.1, namely the basic operations
(Definition D3) and fusedMultiplyAdd.
(convertFromInt is also a "formatOf" operation, but does not seem
relevant for intervals.)
(c) MRMF is not appropriate for the standard.
My reason for view (b) is as follows. For a "formatOf" floating
point operations, whatever the input and output formats, provided
they have the same radix, the correctly rounded result is produced in
all cases. E.g. when adding two b64's, whether the destination format
F is b32, b64 or b128, and whatever the rounding direction, the F-
number nearest the exact result in the relevant direction will be
delivered. The "formatOf" concept eliminates the risk of "double
rounding" error in mixed-format operations.
There are various algorithms for the basic interval operations --
multiply and divide especially have variants optimised for different
environments -- but all those that I know of can exploit the formatOf
feature. That is, all can be written, in terms of the point
operations, so that arbitrary mixed formats of the same radix can be
handled by essentially the same code, while remaining sharp, that is
optimally tight, at the level of a single interval operation.
Therefore I believe the effort in implementing SRMF interval
support of the basic operations, across all 754 formats supported by
a system, is negligibly greater than that of implementing SRSF
support for those operations in just one format such as binary64.
As for (c), 754 does not supported mixed-radix arithmetic and
there seems no reason for P1788 to do so. Conversion between binary
and decimal interval formats should be performed explicitly by the user.
Finally, issues of accuracy (tightness) of interval elementary
functions are largely independent of the SRSF/SRMF/MRMF issue and
should be decided separately.