Re: Possreps and numeric types

From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Thu, 29 Mar 2007 01:12:48 GMT
Message-ID: <koEOh.16751$PV3.172425@ursa-nb00s0.nbnet.nb.ca>

Marshall wrote:

> On Mar 28, 5:27 am, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
>

>>Marshall wrote:
>>
>>>Has anyone seen it? :-(
>>
>>Not yet. Is it in a 'Sent Items' folder of any kind?

>
> Crappity crap. Nope, no sent folder.
>
> Well, for some years now it's been true that I've needed to
> read news at multiple sites, and that stopped being true
> Monday. Maybe I should get a "real" newsreader now.
>
> Roughly, I said my primary interest is in correctness, and
> that proofs of properties of code are the best tool I
> know of in that direction, and that code tends to manipulate
> a lot of numbers, and that proofs depend on algebraic
> properties, and the rationals have many desirable algebraic
> properties and floats don't. Furthermore if we declare
> that floats do have those properties (because they
> *almost* do) then we have rendered our proof system
> unsound.

I respectfully suggest any finite representation of rationals will fail to have many desirable algebraic properties. While the pseudo-rational operations might not have algebraic properties, the implementations of those operations will comprise operations that will have useful algebraic properties on their respective domains.

For a formal proof system, I suggest deferred calculation system that represents numbers as formulae. While finite, such a system can work with irrationals as well as rationals. It would have the nice property that it could automatically trade off performance and accuracy at the final step. I believe products like matlab and derive provide such functionality.

> I also claimed that epsilon was a floating-point specific
> idea that had no bearing on the rationals, no more so
> than the integers, and that epsilon does not belong to
> the domain of discourse of any actual application nor
> of any mathematical theory.

I admit I used epsilon somewhat sloppily and not necessarily with the exact meaning used when discussing a particular floating-point implementation. I used it to mean the distance to the representable predecessor or successor of any representable rational value.

In the infinite set of rationals, one has an infinite number of rationals between any two rationals. However, in every representation of a finite subset of rationals, a predecessor and successor will exist with no intervening values (except at the extreme ends of the range.)

In that sense, every finite approximation of the rationals will involve such an epsilon; although, evaluating the successor and predecessor may be very costly in some representations.

One cannot avoid epsilon. If one represents rationals as a ratio of two integers, epsilon will vary over the range [1/maxint,1/1] and the successor epsilon may differ from the predecessor epsilon. However, the concept of epsilon exists for every value. ie. the successor to 0/1 is 1/maxint and the successor to (maxint-1)/1 is maxint/1.

The successor to 1 is maxint/(maxint-1) and the predecessor to 1 is (maxint-1)/maxint.

Are you suggesting that error analysis does not belong to the domain of discourse of any application or mathematical theory?

> Except there was, like, actual argument and examples
> and stuff, whereas the above is just a bunch of
> unsupported claims.

Yeah, yeah, yeah... a likely story... my newsreader ate my homework. LOL Received on Wed Mar 28 2007 - 20:12:48 CDT