[Top][All Lists]

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

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

From: Gabriel Dos Reis
Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures
Date: 14 Mar 2006 01:43:13 +0100

"Bill Page" <address@hidden> writes:

| I agree with Martin. One should interpret:
|   if Integer has Monoid(*,1)
| as the question of whether F = (*,1) is a functor from the category
| containing Integer to Monoid, the category of monoids.

100% agreed.

| Axiom/Aldor language constraints require us to write
|   Integer has Monoid(Integer,*,1)
| Martin has suggested a method using 'extend' in Aldor to make
| such an assertion by:
|   extend Integer: Monoid(Integer,+,1)

all that makes sense, except that -- upon reflection this a while --
not everythign should be explicit parameter.

Basically, the idea is this.  When have (T, op, e) as a monoid, it is
because the three elements together satisfy some relations.  If I may
borrow some loose analogy, it is like with implicit functions.  The
above means that there are some redundancy in the triple.  Here, e is
uniquely defined by op (maybe non-constructively, but when it exists
it is unique).  Consequently the neutral element is a function of op
and T.  So I would write

     Inetger has Monoid(Integer, *)

     extend Integer: Monoid(Integer, +) with {
         neutral == 0;

-- Gaby

reply via email to

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