Well, Float also asserts Approximate. I guess you can interpret
assertions in two ways:
1) mathematical domain modeled by Float is a Group, but Float
is an approximate model
2) Float itself is a group -- clearly false, should be replaced
by some theory of floating point numbers.
The first way is how normally humans reason about Float. Exact
theories of floating point numbers tend to be of limited use.
I agree, that we use Float to model real numbers. But it's in some sense
a bad model. There are at most countably many floats.
Anyway, I don't question the usefulness of Floats, I question where they
live in the category hierarchy. Real numbers form a field. The
"approximate model" float doesn't fulfill field axioms, so it shouldn't
claim "Field". What would be bad in having ApproximateField?
Float currently inherit from Field and from Approximate. Suppose, I
write a domain constructor which expects its argument to be a Field.
My domain constructor never asks for "if D has Approximate then ..."
(why should it?) and my constructor is given Float as an argument. There
surely will go something wrong, because I've written that constructor
under the assumption that the argument domain has all the functions that
Field has and that theses are computable functions. Isn't it that what
Field says? They are computable. Field (as FriCAS category) and field
(in mathematics) are not identical. Field is silently claiming
computability.
I have nothing against constructing a category hierarchy, where, for
example, zero? is not necessarily always succeeding in finite time. But
if it succeeds, the result should be correct.
But I really much want that non-computable and computable isn't mixed.
Now, for computer use we typically need to make things more
precise, so second way (exact theory) has some appeal.
I know that doing mathematics on a computer is more difficult than
mathematics itself. But that's the whole fun of it. And I like that.
I am not going to sacrifice correctness just because some engineers
don't care whether floats form a field or not.
But I am not sure if following second way we can make system
that is as useful as system made according to first principle
and more sound.
Well, if that is unknown then it's open for research, right?
Ralf
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
