http://axiom-wiki.newsynthesis.org/SandBoxLimitsAndColimits On Sat, May 17, 2008 at 1:54 PM, Ralf Hemmecke wrote: >> Of course using 'Product' in this manner is also applicable in the >> compiler. > > Would that mean you want Product or Cross be more intelligent by > lifting operations from their input domains? >
I am not so sure. After writing 'Sum' I am not so happy. >> It is easy in principle to implement the categorical dual of 'Product' >> that we might call 'Sum'. See for example some initial coding effort >> here: >> >> http://axiom-wiki.newsynthesis.org/SandBoxSum >> >> 'Sum' then is a type of 'Union' that lifts operations from it's >> component domains in the manner as 'Product'. > Although it is obviously the categorical dual, i.e. a co-limit as implemented in http://axiom-wiki.newsynthesis.org/SandBoxLimitsAndColimits it seems that unlike the case of 'Product', I do not understand how (or when) I can properly "lift" operations to 'Sum'. > Yes, both Product and your Sum is an approximation of the categorial > concept. But look more closely at both implementations. They explicitly > state something like > > if A has Finite and B has Finite then Finite > if A has Monoid and B has Monoid then Monoid > if A has AbelianMonoid and B has AbelianMonoid then AbelianMonoid > if A has CancellationAbelianMonoid and > B has CancellationAbelianMonoid then CancellationAbelianMonoid > if A has Group and B has Group then Group > etc. > This list is a problem. It makes sense for 'Product' but in most cases it is wrong for 'Sum'. For example: Yes, if A is finite and B is finite then their direct sum is also finite. But this is not the case if A and B are monoids - their sum is not a moniod. There is no why to define x*y if x is from A and y is from B. If we answer with an error message (as in my code), then the resulting domain does not satisfy the axioms for a monoid. And what is the required *unique* identity in the sum? Apparently all the operations are partial and if A and B are groups then a most, the sum of A and B is a groupoid. > It is so easy for a programmer to forget something important in that list. > And if later somebody comes and introduces a new category that should > also be lifted via Sum, one would have to modify the sources or use > "extend". That is somehow unsatisfactory. However, I also don't see, > how that lifting could be done in a generic fashion, i.e. categorically, > since some categories lift and others don't. > 'Sum' is a problem (for other reasons I think) but in the case of 'Product' I have the impression that such lifting is universal. Can you give an example of a Product over some category that does not lift in this manner? In the case of 'Sum', it seems that something dual to lift must be involved. Right now I do not know this transformation. > Still, the conditional exports are nice, but if this leads to such a list as > in Sum or Product, it doesn't seem to be the last word. > I agree. > Let me dream. > > For example, there appears > > if A has Monoid and B has Monoid then Monoid > > in the category part of Product. So there is a function *: (%,%)->% in A and > B. We all know how the pattern for the lifted function is. So it would be > nice if "Product" or Cross is language defined (and thus the representation > is given) and one only would give such a "pattern" that would apply for any > bivariate function of the same signature. So giving the pattern for (%,%)->% > in the Ring case would suffice to lift + and *, i.e., there would no need to > give identical implementations (except for the names of the operation) for > + and *. > Yes, I think this might be possible for 'Product'. > Of course, that is just made up and there are certainly problems how to lift > not only signatures, but also axioms. > I agree. Regards, Bill Page. ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
