On Sun, Dec 14, 2008 at 6:06 PM, Ralf Hemmecke wrote: > Bill Page wrote: >> See: http://axiom-wiki.newsynthesis.org/LimitsAndColimits > >> Then for example the definition of a simple piecewise function >> might look like this: >> >> p:Sum(NegativeInteger,ZeroInteger,PositiveInteger)->Integer := >> sum(Integer,x +-> -(x^2), x +-> 0,x +-> x^2) > > That looks nice. But, of course it involves quite a lot. (You have > demonstrated that by the package Sum2Functions.) Namely, if > I define (or rather just use) for two domains X and Y the type > Sum(X, Y), then for every other domain A the compiler would > know about a function > > sum: (X->A,Y->A) -> Sum(X,Y)->A > > (of course *without* the need of some package like Sum2Functions). >
I do not think that implementing co-product and product involves anything really new. The function 'sum' is very "natural". It is exactly what you would expect it to be if you first evaluated one function and then another in "series". It is dual to the also very natural idea of evaluating two functions in "parallel" implemented by 'product'. > > But then Sum and Product are just special cases of (Co-)Limits. So > maybe a Limit and CoLimit constructor should be built-in to the > language. There is a theorem called the "existence theorem for limits" which says that for a category to have all limits, it is sufficient that it have products and equalizers. So one gains essentially nothing by generalizing to all limits. On the other hand, an equalizer is a rather complex thing - it corresponds to the largest subdomain A' over which two functions evaluate to the same value. I.E. f:A->B g:A->B h:A'->A f h = g h Finding h:A'->A is what we would normally call "solving" an equation. Co-equalizers on the other hand are a generalization of the process of unification of terms - something that is very important in symbolic processing. > My question would then be, does such a general construction allow > to recover the concrete handling of Record/Cross/Union etc.? (Record, > Cross, and Union would then, of course, not be built-in.) By "concrete" > I don't just mean theoretically, but it rather concerns the question how > could this Limit stuff really be implemented into the compiler? > Record and Cross can be easily recovered from Product. And Union from Sum. The problem is the equalizer (and co-equalizer). To implement these in the most general case, one needs a large part of what normally constitutes a complete computer algebra system. > ... > Invent some other concrete application for which you could > demonstrate the benefit of the categorical programming language > SPAD-CAT. Your example, I cited above, is already something. > Other examples? > I suspect that most of the benefits are conceptual. These might be rather difficult to capture in concrete examples but I will let you know when I find anything worth sharing. In the mean time I might try to take up Waldek's challenge to give a possible treatment of piecewise polynomial functions. Regards, Bill Page. --~--~---------~--~----~------------~-------~--~----~ 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 -~----------~----~----~----~------~----~------~--~---
