Abstraction: xreal
Version: 2
Date: 11 November, 2002
Author: Mike O'Donnell

Depends: ratintvl version >= 1

Changes: Corrected the specification of infinite computation for
         member_xreal_ratintvl?, and removed the optional warning.

         Made the computation of comporder_xreal with prec = 0
         optional.

         Added specification of infinite computation for div_xreal,
         ln_xreal, expt_xreal, rel_xreal->ratintvl, and error reports
         for ln_xreal, expt_xreal, rel_xreal->ratintvl.

         Minor polish and fixing of typos.

Values in the xreal abstraction are exact real numbers. Each xreal x
determines a method for producing an arbitrarily small ratintvl
containing x.

Types
-----

xreal       exact real numbers

xrealcomp   tokens indicating the result of a comparison of xreals

Constructors
------------

lt_xrealcomp is the token indicating that one xreal is less than another.

in_xrealcomp is the token indicating that two xreals are
    indistinguishable at a particular precision.

gt_xrealcomp is the token indicating that one xreal is greater than another.

Type conversions in
-------------------

(rational->xreal r) returns an xreal numerically equal to the rational r.

    If r is not a rational, report an error.

Predicates
----------

(xreal? expr) returns #t if expr is an xreal, #f otherwise.

    xreal? requires an otherwise unneccesary tag in the representation
    of an xreal, so we may decide to skip it.

(member_xreal_ratintvl? xr ri) returns #t if the xreal xr is a member
    of the ratintvl ri, #f otherwise.

    If ri = [r1,r2] and xr = r1 or xr = r2, then the procedure
    may compute infinitely.

(xrealcomp? expr) returns #t if expr is an xrealcomp, #f otherwise.

(lt_xrealcomp? xrc) returns #t if xrc is lt_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

(in_xrealcomp? xrc) returns #t if xrc is in_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

(gt_xrealcomp? xrc) returns #t if xrc is gt_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

Comparisons
-----------

(comporder_xreal xr1 xr2 prec) returns nondeterministically one of

        lt_xrealcomp if xr1 < xr2
        in_xrealcomp if |xr1 - xr2| < prec
        gt_xrealcomp if xr1 > xr2

    Usually, an implementation should prefer lt_xrealcomp or
    gt_xrealcomp when possible at the same cost as in_xrealcomp.

    If prec < 0, report an error.

    If prec = 0, you may decide to report an error, or to run the
    procedure until it definitely determines that xr1 < xr2 or that
    xr1 > xr2. If you decide to try to answer prec = 0 comparisons,
    then you must allow infinite computation when xr1 = xr2. The
    choice depends on the implementation. For the precfunc
    implementation, it is better to report prec = 0 as an error.

Operations
----------

(add_xreal xr1 xr2) returns the sum of two xreals xr1+xr2 as an xreal.

(sub_xreal xr1 xr2) returns the difference of two xreals xr1-xr2 as an xreal.

(mult_xreal xr1 xr2) returns the product of of two xreals xr1*xr2 as an xreal.

(div_xreal xr1 xr2) returns the ratio of two xreals xr1/xr2 as an xreal.

    If xr2 = 0, the procedure may compute infinitely.

(power_xreal xr1 n) returns an xreal to an integer power xr1^n as an xreal.

(exp_xreal xr) returns the exponential function of an xreal e^xr.

(ln_xreal xr) returns the natural logarithm of an xreal ln(xr).

    If you detect that xr1 <= 0, report an error.

    If xr1 = 0, the procedure may compute infinitely.

(expt_xreal xr1 xr2) returns an xreal to an xreal power xr1^xr2 as an xreal.

    If you detect that xr1 <= 0, report an error.

    If xr1 = 0, the procedure may compute infinitely.

Type conversions out
--------------------

(abs_xreal->ratintvl xr a) returns a ratintvl of absolute tolerance (width)
    at most (rational) a containing the xreal xr.

(rel_xreal->ratintvl xr r) returns a ratintvl of relative tolerance at
    most (rational) r containing the xreal xr.

    If r <= 0 report an error.

    If xr = 0, the procedure may compute infinitely.

    rel_xreal->ratintvl is much harder than abs_xreal->ratintvl, so we
    may decide to skip it.

(simplest_xreal->rational ri a) returns the simplest rational r
    such that |r - ri| < a, where a is a rational absolute tolerance.

    simplest_xreal->rational is a bit hard, so we may decide to skip
    it.

Diagnostic utilities
--------------------

(abs_xreal->ratintvllist xr alist) returns a list of ratintvls with
    absolute tolerances in the (rational) list alist containing the
    xreal xr. Normally, if

        alist = (a1 ... an)

   then the returned value is

        ((abs_xreal->ratintvl xr a1) ... (abs_xreal->ratintvl xr an))

    Normally, the values in alist are strictly decreasing, and the
    ratintvls in the returned list are strictly contained in one
    another. But correct implementations may deviate from these norms
    depending on need.

String representations
----------------------

(decimal_sn_xreal->string ri prec) returns a string representing the
    xreal ri in scientific notation with (integer) prec >= 0
    significant digits.

    If prec < 0, report an error.

(decimal_xreal->string ri prec) returns a string representing the

    xreal ri in normal decimal notation with (integer) prec digits to
    the right of the decimal point. If prec < 0, provide |prec|
    insignificant trailing 0s to the left of the decimal point.

(std_rtintvllist->string rilist) returns a character string displaying the
    intervals in the list rilist of ratintvls. std_rtintvllist->string
    is particularly intended to be used with abs_xreal->ratintvllist
    for diagnostic purposes. We may experiment with the most useful
    form of display.