| From: William D Clinger <xxxxxx@ccs.neu.edu>
 | Date: Sun, 24 Jul 2005 10:46:18 +0200
 |
 | Aubrey Jaffer claims to have proved that the language of
 | the R5RS not only regards inexact numbers as neighborhoods,

No, it claims that inexact numbers are in one-to-one correspondence
with neighborhoods around their nominal values.  Although the proof
dealt only with reals, the same is true for complex numbers; and in
that case, the neighborhoods are not all rectangular.

 | but that no other interpretations of the R5RS are tenable.

I don't think so; how could one disprove a proposition before it is
made?

 | Jaffer's alleged proof contains many errors of logic, which
 | I will happily enumerate if anyone claims to remain convinced
 | by the alleged proof.

Yes I would.  I have appended a detailed proof of the first part
(finite number of inexacts).

 | Below I merely offer a simple argument that the "inexact numbers
 | denote neighborhoods" interpretation is itself untenable. ...

Clinger's alleged counterexample assumes interval arithmetic on
inexacts, which was never part of SRFI-70.

In SRFI-70 inexact calculations are performed on the nominal
mathematical values around which the neighborhoods are based.  The
result of a calculation is also single valued; which neighborhood it
lies in determining which inexact number is returned.

For the finite number of inexacts case, the assertion that
mathematical numbers close to the nominal value project onto that
inexact number is neither profound nor revolutionary.  As SRFI-70
demonstrates:

  In an implementation which represents inexact real numbers with
  IEEE-754 64-bit flonums:

  (= 3.14159265358979323846
     3.1415926535897932384626433
     3.141592653589793238462643383279
     3.14159265358979323846264338327950288)       ==>  #t

			      -=-=-=-=-

In the following proof, "inexact number" refers to a member of an
equivalence class (under `=') of inexact numbers represented by the
R5RS-compliant implementation.  Other numbers are mathematical
numbers.

Given:

{a} A R5RS-compliant implementation has a finite number greater
    than 1 of inexact number equivalence classes under the
    transitive R5RS predicate `='.

{b} That implementation contains an inexact number class #i1.0
    such that

    (eqv? #i1.0 (string->number "1.0"))

{c} procedure: string->number string
     Returns a [inexact] number of the maximally precise
     representation expressed by the given STRING.

{d} for any inexact number x:

    (= x #i1.0) if-and-only-if (zero? (- x #i1.0))

Consider the mathematical sequence indexed by positive integer k:

  E[k] = 1 + (-1/10)^k						{e}

  0.9, 1.01, 0.999, 1.0001, 0.99999, 1.000001, ...

E[k+2] is strictly between E[k] and E[k+1] {e}.			{f}

The limit of E[k] as k tends to infinity is 1 {e}.		{g}

Let S[k] be the string containing a decimal representation of
E[k].  That sequence begins:					{h}

  "0.9", "1.01", "0.999", "1.0001", "0.99999", "1.000001", ...

Let I[k] be (STRING->NUMBER S[k]) {c,h}.			{i}

Because the implementation has a finite number (> 1) of distinct
(under `=') inexact numbers classes {a}, the lower bound, L[1],
of the distance between #i1.0 and members of any other inexact
number class must be a nonzero {a,d}.				{j}

Thus there must exist an integer j such that (abs (- E[k] 1))
is less than L[1]/4 for all k > j {f,g,i,j}.			{k}

I[k] must be #i1.0 for k > j, because no other inexact number
class can be closer {c,j}; and because STRING->NUMBER of the
string representation of the limiting value, "1.0", is #i1.0
{b,g,k}.							{l}

Thus the projection of mathematical numbers between E[j] and
E[j+1] into inexact number classes is #i1.0.

			      -=-=-=-=-

Note that the neighborhood between E[j] and E[j+1] is a subset
of the full neighborhood which STRING->NUMBER maps to inexact
number class #i1.0.

There was nothing special about #i1.0 in this proof.  It will
apply to any other finite inexact number y satisfying:

  (eqv? y (string->number (number->string y)))

where the string representation of y, (number->string y), is
"decimal" according to R5RS-6.2.6.				{m}