Ralf, I think I have had some insight into the idea of "lifting" operations in relation to Sum (analogous to Product) and my faith in the importance of categorical duality is restored. :-)
It seems that in any mathematical category sufficiently complicated to include the semantics of Spad (Axiom) - probably something like a topos - the dual of a particular construction such as "lifting" in the case of 'Product' need not be so obvious as the relation between Limits and Colimits. In fact is seems clear to me now that the dual to "lifting" in the case of 'Product' is the concept of "sub-domain" in the case of 'Sum'! Just as products can automatically inherit operations from components in a "pair-wise" fashion, components of a sum can inherit operations from the sum. (The inheritance is in the opposite direction, of course. :-) For example, suppose we have Sum(Z,PI) == NNI where Z ==> Zero, PI ==> PositiveInteger, NNI ==> NonNegativeInteger If we declare that 'PI has AbelianSemiGroup' then the fact that 'NNI has AbelianSemiGroup' entitles us to simply take the '+' from 'NNI' as '+' in 'PI'. Similarly, that 'NNI has Monoid' implies '*' comes from 'NNI'. In fact this is how 'PI' is constructed in Axiom but unfortunately the SubDomain construction does not fully reflect this relationship to category theory: PositiveInteger: Join(AbelianSemiGroup,OrderedSet,Monoid) == SubDomain(NonNegativeInteger,#1 > 0) add ---------- The function '#1 > 0' provides the 'case' construction on NNI that picks out the particular subdomain. Perhaps the language would be a little prettier if there was some construction dual to 'SubDomain' that performed the "lifting" for domains like Product: Product(A:SetCategory, B:SetCategory): Lift(Monoid,A,B) with ... But given the nature of the Spad language, I do not think this can be made entirely automatic. Critical opinions invited ... For example, one might remark that such language features hardly seem worth the effort since right now the Axiom library contains only two instances of the use of 'SubDomain' and there may similarly be a rather limited number of cases where the kind of lifting that occurs in 'Product' is repeated in other domains. I am not currently convinced by this observation. Regards, Bill Page. On Sun, May 18, 2008 at 9:19 AM, Bill Page wrote: > 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'. > _______________________________________________ Axiom-math mailing list Axiom-math@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-math
