[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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 15:55:48 +0100
User-agent: Thunderbird 1.5 (X11/20051201)

On 03/14/2006 01:37 AM, Gabriel Dos Reis wrote:
Ralf Hemmecke <address@hidden> writes:

| Integer is a name for a structure with carrier set
| | {0, 1, -1, 2, -2, ...} | | and operations {+, *, 0, 1, ...}. | | Integer is certainly not the carrier set alone.

Well, actually, it is a convention what Integer should stand for.
For some people it might just be enough to consider Integer as an abbreviation for the multiplicative structure ({0,1,-1,...}, (*, 1)}
for other people (ie in other contexts) it might be the ring structure.
And very common in algebra, the carrier set is often denoted by the same symbol as the whole algebraic structure. (I guess the latter it too ambiguous to be mapped to a programming language?)

Indeed. It is a type, e.g. set equipped with minimal operations that
let us implement abstractions on top of it.  Just an abstract data
type can be implemented in terms of another one, an algebraic
structure cane be constructed in terms of another one.

| How would you mathematically express that the integers belong to the
| category of monoids? You would probably say that
| | F(Integer) is an object in the category of monoids

I would do it by assertion.

What does that mean?

But I will refrain from needlessly emphasizing on the the carrier set
> -- as F(Integer).

Oh, I hope you understood that F was meant to be a (forgetful) functor in the categorial sense whose result would be an object in the category of monoids.

So, if you like you could say

define MyMonoid: Category == with {*:(%,%)->%;1:%}
  -- axioms still missing :-(
MonoidStructure(T: Type)(binop:(T,T)->T, unit:T): Monoid == T add {
  Rep == T; import from T;
  (x: %) * (y: %): % == per(binop(rep x, rep y);
  1: % == per unit;

That IS Aldor syntax and it would compile. So in Aldor term F from above would be something like

F = G(binop, unit)

for that to work it should be possible to write G as

MonoidStructure(binop:(T,T)->T, unit:T): (T: Type) -> Monoid ...

where the operations would have to be specified before the type is given. I don't think that is possible in a programming language.

HOWEVER, the above code would ALWAYS return something of type Monoid, since it is a type constructor in Aldor and not a forgetful functor in the mathematical sense. For me the question would be, how could one write forgetful functors in Aldor?

Oh, it just came to my mind, we can have forgetful functors.

Let's take Integer. According to what it has been extended it has a definite type (some Aldor category). Basically, if one says

MyInteger: with {+: (%, %)->%; 0: %;} == Integer add;

then MyInteger is like Integer (same carrier set) but everything forgotten except + and 0.

Well, then now it remains the question how one could match the names
+, 0 with *,1 in Monoid when asking "MyInteger has Monoid".

But there are 2 problems here.

1) How to match + and the binary operation from Monoid?

2) My specification above probably forgets to much. After all it also forgets the properties of + and 0. So it could never be a monoid. Unfortunately, Axiom/Aldor does not allow axioms (and I would like to see arbitrary predicate logic formulas not just declarative syntax).


reply via email to

[Prev in Thread] Current Thread [Next in Thread]