axiom-developer
[Top][All Lists]

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

 From: Ralf Hemmecke Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures Date: Tue, 14 Mar 2006 22:39:20 +0100 User-agent: Thunderbird 1.5 (X11/20051201)

```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

```