Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Ralf Hemmecke]

On 03/14/2006 06:56 PM, Page, Bill wrote:
> Ralf, 
>
> On Tuesday, March 14, 2006 9:57 AM you wrote:
> > > "Bill Page" <address@hidden> writes:
> > >
> > > | On March 13, 2006 6:34 AM Ralf Hemmecke asked:
> > > | > ... 
> > > | > But here the question to our category theory experts:
> > > | > Since Monoid is something like (*,1) would it make sense
> > > | > to speak of a category (in the mathematical sense) of
> > > | > 
> > > | >    monoids that have * and 1 as their operations   (1)
> > > | > 
> > > | > ? Morphisms would respect 1 not just the identity element 
> > > | > with respect to *. And for each morphism f we would have
> > > | > f(a*b) = f(a)*f(b). Of course as operations the two * above
> > > | > are different but in that category they have to have the same
> > > | > name. (No idea whether this makes sense, but it seems that
> > > | > this is the way as "Category" it is implemented in Axiom/Aldor.)
> > > | > 
> > > | > Then, of course, (N, +, 0) is not an object in the category 
> > > | > given by (1).

> > Well, Bill, are you saying that I cannot have (1) as a category?
> Let me try to answer again: No. :)

> I think your definition (1) is not a category in the usual sense
> of category theory.

> > A category is a collection of objects and morphisms. Let's 
> > define MYMON. Let an object be as follows:
> >    A set M together with to operations *: (M, M) -> M
> >    and 1: M such that the monoid axioms are satisfied.
> >    (I am lazy and don't specify them here explicitly.)
> > The morphisms in MYMON are the usual monoid-homomorphisms.

> Ok.

> > And yes, if something wants to be an object in MYMON, it
> > has to have * as its binary operation and not +.

> This does not make much sense to me.

OK, that would be the answer to my question above.

> That is the same thing as trying to say that if some set "wants to
> be" an object in MYMON it must be named M and not N. This is
> irrelevant when defining a category. Both M and * are "formal
> parameters" that do not have any more meaning than we wish to assign
> to them.

OK, it's in some sense similar to the signature as it appears in Doye's 
thesis. M is a sort and * and 1 are operator symbols.

> > And yes, I consider (N, +, 0) not an object in MYMON. What
> > I try to say is that Aldor has currently this view for the
> > "Monoid" category.

> Do you mean you think the distinction is a "syntactic" one
> and not a semantic one? If so, then I think I agree with
> you. 

I did not think about syntax and semantic, but it seems that is it.

> Aldor categories are not categories in the sense of
> category theory.

By now, we should all know that. And anyway, if Aldor categories were 
true categories then the morphisms are missing.

But let's try to identify what the morphisms could be in the current 
view of Aldor.

OK, just an example that should be further formalised.

define CatA(A: Type): Category == with {foo: (A, %) -> %}
X: CatA(Boolean) == add {foo(a: A, x: %): % == ...}
Y: CatA(Boolean) == add {foo(a: A, x: %): % == ...}

Let h: X -> Y. It consists of several maps, namely
h_A: A_X -> A_Y (where A_X = A_Y = A)
h_%: %_X -> %_Y (where %_X and %_Y are the respective %'s)
Then h_A(a)=a for all a in A
and we require compatibility with the operations so:

  h_%(foo(a, x)) = foo(h_A(a), h_%(x))                 (C1)

All such h for any domains that are declared to be of type CatA(Boolean) 
are morphisms of CatA. By the way, since any Aldor program consists of a 
finite number of characters, doesn't that just mean that any Aldor 
category can have only finitely many objects.

And yes, (C1) seems to be syntactic, since there is foo on both sides of 
the equality and not foo_X and foo_Y.

> Nonetheless it is the nature of symbolic
> calculation on a computer that we are always in the position
> of trying to express semantic ideas in terms of syntax. In
> the same way the series of digits:
>
>    3 1 4 1 9 5
>
> is not an "integer" in the mathematical sense. Nonetheless
> we do use this symbolic representation of an integer to
> perform calculations by hand and a similar (usually binary)
> notation to do calculations inside the computer.

Good point. We agree on some representation of Integer (or natural 
numbers) an never really question it, although there are more such 
things that satisfy the Peano axioms.

Maybe that is one reason why the Axiom designers did not try to 
distinguish between operator symbols and operator names (see Doye's 
thesis chapter 9) with the consequence that AbelianMonoid does not 
inherit from Monoid.

> But I do not see how recognizing this fact gets us any
> further along the path to understanding how to represent
> the mathematical notion of a monoid in Axiom.

Well, understanding the current situation is certainly one step to a 
solution. To me it seems that Aldor needs a way to distinguish operator 
symbols from operator names.

Maybe we could agree on a temporary syntax for such a distiction and 
then try to figure out what positive and negative consequences such a 
language feature would have.

What do you all think? The goal is to make Aldor more mathematical 
without introducing unhandy language constructs.

And maybe at the same time we should think about introducing axioms to 
Axiom that are not just declarative objects like "commutative(+)" but 
logical formulae.

Ralf