[Haskell-cafe] Re: 0/0 > 1 == False

[Jonathan Cast]

On 11 Jan 2008, at 10:12 AM, Achim Schneider wrote:

> David Roundy <droundy at darcs.net> wrote:
>
>> Prelude> let x=1e-300/1e300
>> Prelude> x
>> 0.0
>> Prelude> x/x
>> NaN
>>
>> The "true" answer here is that x/x == 1.0 (not 0 or +Infinity), but
>> there's no way for the computer to know this, so it's NaN.

Didn't catch this the first time around, but: only to a physicist.   
(I mean no disrespect to the author of darcs, but nevertheless the  
point stands).  Back in the real world, 0 / 0 may be defined  
arbitrarily, or left undefined.  (Defining it breaks the wonderful  
property that, if lim (xn) = x, lim (yn) = y, and x/y = z, then lim  
(xn / yn) = z.  This is considered a Bad Thing by real  
mathematicians).  In fact, in integration theory 0 * inf = 0 for  
certain 'multiplications', which gives the lie to 0 / 0.

>>
> Weeeeeeeelllllllll...... math philosophy, Ok.
>
> You can't divide something in a way that uses no slices. You just  
> don't
> cut, if you cut zero times. Which is what you do when you divide by
> one, mind you, not when you divide by zero. Division by [1..0] equals
> multiplication by [1..].

Right.  (Although 0 * inf is defined by fiat, as noted above).

> You can't get to the end of either spectrum,
> just axiomatically dodge around the singularities to axiomatically
> connect the loose ends.

`Axiomatically' --- you mean by re-defining standard notation like *  
and / to mean what you need in this case.  I think this is a  
different thing than setting up ZFC so everyone agrees on what a  
`set' is from henceforth.

> There is no true answer here, the question is wrong.

Exactly.

jcc