axiom-developer
[Top][All Lists]

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

 From: Martin Rubey Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures Date: 02 Mar 2006 11:11:32 +0100 User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.4

```"Bill Page" <address@hidden> writes:

> In Axiom (SPAD) we can write:
>
> Monoid(m:Symbol,u:Symbol): Category == with
>        m: (%,%) -> %       ++ returns the product of x and y
>        u: () -> %          ++ unit
>        associative(m)      ++ m(a,m(b,c)) = m(m(a,b),c)
>        identity(u)         ++ m(a,u) = m(u,a) = a
>
> Group(m:Symbol,inv:Symbol,u:Symbol): Category == Monoid(m,u) with
>        inv: % -> %         ++ inverse
>        inverse(m,inv)      ++ m(inv(a),a) = m(a,inv(a)) = u
>
> AbelianGroup(m:Symbol,inv:Symbol,u:Symbol): Category
>    == Group(m,inv,u) with
>       commutative(m)       ++ m(a,b) = m(b,a)
>
> Ring(s:Symbol,inv:Symbol,z:Symbol, m:Symbol,u:Symbol): Category
>    == Join(AbelianGroup(s,inv,z),Monoid(m,u)) with
>       distributes(m,s)     ++ m(a,s(b,c)) = s(m(a,b),m(a,c))
>                            ++ m(s(a,b),c) = s(m(a,c),m(b,c))
>
> Then we can write:
>
>   )sh Ring(+,-,"0"::Symbol,*,"1"::Symbol)
>   Ring(+,-,"0"::Symbol,*,"1"::Symbol) has commutative(+)
>
> See the example at http://wiki.axiom-developer.org/SandBoxMonoid

That's very interesting. I would have thought that it's not possible to use a
parameter as the name of an operation. Is this possible in Aldor, too? (I'd
guess so)

Ooops, I just tried to implement a domain:

)abbrev category MYMON MyMonoid
MyMonoid(m:Symbol): Category == with
m: (%,%) -> %       ++ returns the product of x and y

square: % -> %

square a == m(a,a)

)abb domain WORDS Words
Words: Exports == Implementation where

Exports ==> MyMonoid("c"::Symbol) with

coerce: String -> %

Rep := String

coerce(a: String): % == a

c(a:%, b:%):% == concat(a::Rep, b::Rep)

but square won't work then: Axiom is looking for an operation m, which does not
exist, of course.