Re: [Axiom-math] POLY INT =\\= UP(x, INT)

[Dylan Thurston]

On Sat, Oct 11, 2003 at 12:02:45AM -0400, William Sit wrote:
> Dylan Thurston wrote:
> Agreed. But since "equality" can be tested at different levels (for example a
> mathematical object may be using a certain representation, but equality of the
> mathematical object can be tested using only a portion of the representation
> (the representation may carry additional information for efficiency); equality
> of the entire data representation can be tested if each part of it can be 
> tested
> but this may not tell mathematical equality always because the representation
> need not be unique; or equality of the mathematical object can only be tested
> after rewriting to some canonical form that is not the data representation.

Another case to bear in mind is when the data representation is not a
data _structure_, per se, but rather something like a function closure
(as is likely to be the case with the computable reals example; then
there isn't really a sensible equality, other than surface equality,
equality of function pointers.

> So perhaps a better signature would be:
> 
>      "=": (%,%)->Union(Boolean, "Failed")
>   ++ x = y returns true if x and y are equal
>   ++ or false if x and y are not equal
>   ++ or "failed" if this cannot be decided

This is useful in many cases, but not always.  For instance, in work on
Functional Reactive Animations, they had some interesting types that
support all the operations of a ring: time-varying numbers: functions
from a time to (say) an integer.  Their examples were things like the
position of a mouse as a function of time.  "Equality" on such types
should really return a time-varying Boolean, which does not really fit
into the scheme above.

I would propose to leave equality as it is, and just not require that
every domain in the entire heirarchy implement it!  (That is, remove it
from the base of the heirarchy, and instead inherit from it when you
really need it.)  After all, the ordinary signature for equality is
useful in a great many cases.  (This may be impractical without some
better type inference, however.)

Alternatively, to tie the threads together, the more topos-like idea
would be to have equality possibly take values in different types:
ordinary Booleans, Booleans that may fail, Booleans that can be computed
to any specified degree of accuracy, time-varying Booleans...  But I
don't see clearly how that would work.

Peace,
        Dylan

signature.asc
Description: Digital signature