[Axiom-math] Re: Product & Sum

[Bill Page]

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'.
>