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.