On Tue, Apr 8, 2008 at 8:59 PM, Gabriel Dos Reis wrote: > Bill Page writes: > > | I can not agree. Because something cannot always be computed > | does not mean that it is therefore ill-defined. This is especially true > | in mathematics. > > I believe you're putting confusing the issues. Function equality > is well-defined in classic mathematics (set theoretical). But > that definition is almost useless from algorithmic perspective. >
I do not think "almost unless" is synonymous with ill-defined even from an algorithmic perspective. In reply to a similar comment by Waldek in this thread I characterized the current fully computable syntactic definition of equality for functions as an "approximation" to the actual equality. I think what it means to be approximate can in principle be rigorously defined. > > | For example, the assumed equality of functions, i.e. the > | concept of a commutative diagram, is essential for category theory. > > `category theory' is a medium, not the message. By itself it is void > of content. > You would have a hard time convincing me of this - and I dare say a lot of mathematicians and even physicists who now consider themselves "category theorists". Take a look for exampe at: http://golem.ph.utexas.edu/category or in particular: http://golem.ph.utexas.edu/category/2008/03/computer_scientists_needed_now.html Would you say that classical set theory is similarly "devoid of content"? If not, what do you say about topos from category theory as an algebraic version of set theory? > > | And we have not problems (in principle) in dealing with exact > | representations of real numbers in computer algebra systems. > > Sure, we do. > What problems do you have in mind? See for example: http://axiom-wiki.newsynthesis.org/RealNumbers In this case equality of computable exact real numbers is formally not decidable since in general corresponding to each computable exact real number is some algorithm that computes it. But from the point of view of computer algebra I do not see any problems with defining such a domain for use in Axiom. There are even "problems" with the concept of equality in floating point numbers, e.g. the equality normally used there is not transitive - so it is not even formally an equivalence relation. But nonetheless floating point numbers are an important domain in computer algebra systems. Wouldn't you agree? > > | > I don't see a point in build a tower of hacks over hacks. > | > | I do agree with you there! Let's fix the original hacks. :-) > > Please, don't hesitate to submit patches fundamentally grounded in > category theory and of practical use. > Ok. That is work in progress. I see the Record, Union and Mapping types in Axiom as directly related to categorical constructions and I think it is possible to extend SPAD to more directly support these ideas. Being able to at least syntactically define equality for functions is critically important to this goal. > > | > The fact that Mapping belongs to SetCategory is largely > | > historical accident. I would rather ditch that relationship out. > | > > | > | I think SetCategory is mis-named. It does not provide anything > | substantially more than BasicType. Would you propose that > | Mapping not even belong to BasicType? > > The question is not whether foo belongs to bar. The question is > what does bar mean? What is the semantics of BasicType? > The source code says: "BasicType is the basic category for describing a collection of elements with = (equality)." Like Mapping, both Record and Union currently also belong to SetCategory. Do you also object to this? Regards, Bill Page. ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Don't miss this year's exciting event. There's still time to save $100. Use priority code J8TL2D2. http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
