login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBox
SandBox Matrix  ← ↑ →  SandBox Numerical Integration

SandBox Monoid
  
last edited 9 years ago by Bill Page

Edit detail for SandBox Monoid revision 1 of 4
1 2 3 4
Editor:
Time: 2007/11/18 18:28:51 GMT-8
Note: Martin's beautiful idea 
changed:
-
\begin{spad}
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))
\end{spad}

\begin{axiom}
)sh Ring(+,-,"0"::Symbol,*,"1"::Symbol)
Ring(+,-,"0"::Symbol,*,"1"::Symbol) has commutative(+)
\end{axiom}

Let's try this ...
\begin{axiom}
)sh Ring(a,b,c,d,e)
Ring(a,b,c,d,e) has commutative(a)
\end{axiom}
Interesting! Is it somewhere written that "has" can have a category as its first argument?

OK, we are going to implement...
\begin{spad}
)abbrev domain MYINT MyInteger
MyInteger: Ring(a,b,c,d,e) == add
  Rep:=Integer
  a(x: %, y: %): % == x
  b(x: %): % == x
  c(): % == 0 pretend %
  d(x: %, y: %): % == x
  e(): % == 0 pretend %
\end{spad}

Oops, that's not so easy. Have I made some error?
(You originally wrote begin{axiom} but this is spad code.

From kratt6 Thu Mar 2 08:46:49 -0600 2006
From: kratt6
Date: Thu, 02 Mar 2006 08:46:49 -0600
Subject: 
Message-ID: <20060302084649-0600@wiki.axiom-developer.org>

Unfortunately, this won't work. For example in the above definition of 'Monoid', we are effectively creating to different things with the same name, but different types. We have an 'm' of type 'Symbol', and another one of type '(%,%)->%'. As soon as we add a default implementation, this mistake surfaces:

\begin{spad}
)abbrev category MYMON MyMonoid
MyMonoid(m:Symbol): Category == with
       m:(%,%) -> %
       square:% -> %
     add
       square(a:%):% == m(a,a)$%
\end{spad}

\begin{spad}
)abbrev domain WORD Word
Word(c:Symbol): MyMonoid(c) with 
    coerce:String -> %
    coerce:% -> OutputForm
  == add
    Rep := String
    coerce(a:String):% == a pretend %
    coerce(x:%):OutputForm == message(x pretend String)$OutputForm
    c(a:%, b:%):% == concat(a::Rep, b::Rep)
\end{spad}
\begin{axiom}
)sh Word
)sh Word("p"::Symbol)
w1:="a"::Word("p"::Symbol)
w2:="b"::Word("p"::Symbol)
p(w1,w2)$Word("p"::Symbol)
p(w1,w1)$Word("p"::Symbol)
square(w1)$Word("p"::Symbol)
\end{axiom}

What we really would like to have would be something along the lines of:
\begin{spad}
)abbrev category MYMON1 MyMonoid1
MyMonoid1(S:SetCategory, m: (S,S)-> S): Category == with
       m: (S,S)-> S
       square: S -> S
     add
       m
       square a == m(a,a)
\end{spad}

\begin{axiom}
)sh MyMonoid1
\end{axiom}

\begin{axiom}
)set functions compile on
m1:=(a:String,b:String):String+->concat(a,b)
m1("aaa","bbb")
)sh MyMonoid1(String,m1)
m2(a:String,b:String):String==concat(a,b)
m2("aaa","bbb")
)sh MyMonoid1(String,m2)
\end{axiom}

Then::

  Word: MyMonoid1(String,(a:String,b:String):String+->concat(a,b)) with
      coerce: String -> %
    == add

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

However, there are two problems here: 

- it is not possible to refer to the category to be defined in the parameter, as in 'MyMonoid(m: (%,%)-> %)'

- it is not possible to refer to an operation which is not yet defined as in 'Word: MyMonoid(c) with'

Martin

From BillPage Thu Mar 2 09:42:18 -0600 2006
From: Bill Page
Date: Thu, 02 Mar 2006 09:42:18 -0600
Subject: scope of names in default implementation of categories
Message-ID: <20060302094218-0600@wiki.axiom-developer.org>

Martin wrote:

> Unfortunately, this won't work. For example in the above
> definition of Monoid, we are effectively creating to different
> things with the same name, but different types. We have an
> m of type Symbol, and another one of type (%,%)->%. 

I agree that there is a scope issue here. Perhaps it comes from
the idea of allowing default implementation as part of the category
definition. But I think the proper semantics are quite easy to define.
The exports need to have priority over the parameters. The 'm' of
type Symbol is not exported by 'MyMonoid' but the m of type
(%,%)-> % is exported. The m in the implementation 'm(a,a)' should
refer to 'm' that is being exported.

So I think this is a compiler error.

From BillPage Fri Mar 3 15:46:42 -0600 2006
From: Bill Page
Date: Fri, 03 Mar 2006 15:46:42 -0600
Subject: generic monoids in Aldor
Message-ID: <20060303154642-0600@wiki.axiom-developer.org>

Based on an idea posted to this page by Martin Rubey, I have
constructed what I think is a good facsimile of a generic
monoid. I think think that this construction is only possible
in Aldor.

The idea is basically to specify a monoid as a tuple in the
usual manner, consisting of a set 'S', an associative binary
operator 'm' and unit 'u'. In this example MyMonoid exports two
operations and a constant: '*' for the binary operation in the
monoid (whatever it happens to be), '^' for repeated '*'
repeated n times, and '1' denoting the ring identity.

This is rather different that the notion that we started with
in this thread - in fact more or less the opposite: from any
more complex domain we can extract the monoid part. Of course
this is fundamentally very simple, just as it should be. :)

\begin{aldor}[mymonoid]
#include "axiom"

define associative(S:SetCategory, m:(S,S)->S):Category == with {
  default ForAll(a:S,b:S,c:S):Boolean == m(a,m(b,c)) = m(m(a,b),c);
};

define identity(S:SetCategory, m:(S,S)->S, u:S): Category == with {
  default ForAll(a:S):Boolean == m(a,u) = a and m(u,a) = a;
};

MyMonoid(S:SetCategory, m:(S,S)->S, u:S): with {
       associative(S,m);
       identity(S,m,u);
       *:(%,%) -> %;
       1: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} ==   add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- product
       (a:%) * (b:%):% == per(m(rep(a),rep(b)));

       -- Repeated squaring
       (x:%)^(n:NonNegativeInteger):% == {
         import from Integer,NonNegativeInteger;
         (n = 0) => return 1;
         odd?(n::Integer) => return x*(x*x)^shift(n,-1);
         return (x*x)^shift(n,-1);
       };

       -- unit
       1 == per(u);
}
\end{aldor}

This is how the 'MyMonoid' domain looks to the Axiom interpreter.
\begin{axiom}
)sh MyMonoid
)sh MyMonoid(String,concat,"")
)sh MyMonoid(List INT,concat,[])
\end{axiom}

Here is Martin Rubey's String monoid example:
\begin{axiom}
w1:="a"::MyMonoid(String,concat,"")
w2:="b"::MyMonoid(String,concat,"")
w1*w2
w1*w1
w1^10
w1*1$MyMonoid(String,concat,"")
1$MyMonoid(String,concat,"")*w1
\end{axiom}

And of course we can construct a large number
of other examples.
\begin{axiom}
i1:=[1,2]::MyMonoid(List INT, concat,[])
i2:=[3]::MyMonoid(List INT, concat,[])
i1*i2
i1*i1
i1^3
i1*1$MyMonoid(List INT, concat,[])
1$MyMonoid(List INT, concat,[])*i1
\end{axiom}

\begin{axiom}
i1:=10::MyMonoid(INT, +, 0)
i2:=20::MyMonoid(INT, +, 0)
i1*i2
i1*i1
i1^0
i1*1$MyMonoid(INT, +, 0)
1$MyMonoid(INT, +, 0)*i1
\end{axiom}

\begin{axiom}
i1:=10.1::MyMonoid(Float, *, 1)
i2:=20.2::MyMonoid(Float, *, 1)
i1*i2
i1*i1
i1^4
i1*1$MyMonoid(Float, *, 1)
1$MyMonoid(Float, *, 1)*i1
\end{axiom}

Now try to define a group.

\begin{aldor}[mygroup]
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;

define inverse(S:SetCategory, m:(S,S)->S, inv:S->S, u:S): Category == with {
  default ForAll(a:S):Boolean == m(inv(a),a)=u and m(a,inv(a))=u;
};

MyGroup(S:SetCategory, m:(S,S)->S, inv:S->S, u:S): with {
       associative(S,m);
       identity(S,m,u);
       inverse(S,m,inv,u);
       ~:% -> %;
       *:(%,%) -> %;
       1: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == MyMonoid(S,m,u) add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- inverse
       ~(a:%):% == per(inv(rep(a)));
}
\end{aldor}

This is how the 'MyGroup' domain looks to the Axiom interpreter.
\begin{axiom}
)sh MyGroup
)sh MyGroup(INT,+,-,0)
\end{axiom}

For example:
\begin{axiom}
x:=3::MyGroup(INT,+,-,0)
y:=~x
x*y
\end{axiom}

From wyscc Wed Mar 8 12:35:43 -0600 2006
From: wyscc
Date: Wed, 08 Mar 2006 12:35:43 -0600
Subject: A different issue?
Message-ID: <20060308123543-0600@wiki.axiom-developer.org>

I am not impressed. However, this kind of finessed the whole issue of notation and neglected the dual inheritance situation, and I expect one will get into trouble when one wants to go on to 'MyRing'.  Any domain in 'MyRing' should work without unnecessary package calls in the Interpreter. All this mechanism did was passing a function 'm' to  constructors, here to be used as the monoid categorically defined multiplication. This technique has been used before, in Axiom, in 'GDMP'. The notation in an Interpreter session is still '*', the operator declared in 'MyMonoid'. So even though we have 'MyMonoid(INT,+,0)' and we can compute using 'i1*i2' to really get the sum of 'i1' and 'i2', this is not using '+' notation. Notice also that 'MyGroup' should have been implemented as a category constructor. In ')sh MyGroup', the group operation is '*', the unit is '1' and the inverse is '-' (which is incompatible with '*' and wrong, since a group should not be commutative in general). But these last two comments are minor quibbles and easily corrected.

I indicated before that I believe one needs to make some deeper changes to implement inheritance that would support notational changes in a way such that multiple inheritance of 'MyMonoid' to the same domain constructor can distinguish the operators. Any proposed solution under the currently available systems, if possible at all, should include 'MyRing' (as a category, not domain) and 'MyInteger' as a domain in 'MyRing'.

I am more interested in the 'associative' category and the 'ForAll' in Aldor.  How exactly does that differ from Axiom? 'ForAll' seems to be only a case by case verification, given actual elements of the domain.

William

From BillPage Wed Mar 8 21:45:13 -0600 2006
From: Bill Page
Date: Wed, 08 Mar 2006 21:45:13 -0600
Subject: Re: A different issue?
Message-ID: <20060308214513-0600@wiki.axiom-developer.org>

William, it seems to me that you are easily *not impressed* ;)
But thanks for your comments.

I agree that the second half of this page implements a different
structure than the first half - I said as much above. It is in a
formal sense the exact opposite thing. But opposites can be useful.
I am working out the details here because I am hoping that in the
end we can see the issue of inheritance more precisely as the dual
to this construction.

The point here is that 'MyGroup(INT,+,-,0)' **declares** that this
combination of domain, operations and constant constitutes a group.
It does not attempt to **construct** this group in 'INT' but rather
it **extracts** this part of INT as a subdomain having the structure
of a group::

    MyGroup(INT,+,-,0) >-----> INT
    with *, ~, 1               with +, -, 0, *, /, 1,  ...

In categorical terms both 'MyMonoid' and 'MyGroup' are monomorhic
functors, i.e. subdomain constructors.

(Note that I changed the notation for inverse in 'MyGroup' to ~
so that perhaps it is less confusing.)

'MyGroup' is not implemented as a category constructor because
as I said, the intent here is not to construct 'MyInteger' by
inheritance. In this case the implementation of 'Integer' is
given and we are simply identifying parts of it.

Inheritance does require something similiar::

    MyInteger: Join(Group(%,+,-,0), Monoid(%, *, 1), ...
                    with *, ~, 1    with *, 1

In this case the categories 'Group', 'Monoid', etc. are given and
we wish to provide new names for their operations in 'MyInteger'
as suggested by Ralf. Unfortunately as Martin demonstrated on
the first part of this page, the SPAD compiler does not compile
it correctly. Maybe we can still find a way to do this with Aldor.
I haven't given up yet, I am just working on a different aspect
of the problem.

The 'associative' category as I implemented it above in Aldor
can also be written this way in SPAD. But as far as I know Aldor
does not implement Axiom's axioms (assertions) so in Aldor these
must be coded as categories with a possibly empty 'with { }' clause.

'ForAll' is not an Aldor primitive construct, it is just a simple
export that is intended to express the axioms in a manner that
could be used in some kind of theorem proving subsystem (which
does not exist yet :). You are right however that this could very
easily be used to implement an automatic verification system.
Such as system could least provide useful counter examples when
the axioms fail.

I am still thinking about how best to encode these sort of axioms,
so the 'ForAll' construct above is likely to change a little.

Stay tuned to this channel ...

<hr />

Define an Abelian (commutative) group:
\begin{aldor}[myabeliangroup]
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
#library MyGroup "mygroup.ao";
import from MyGroup;

define commutative(S:SetCategory, m:(S,S)->S): Category == with {
  default ForAll(a:S,b:S):Boolean == m(a,b) = m(b,a);
};

MyAbelianMonoid(S:SetCategory, s:(S,S)->S, z:S): with {
       commutative(S,s);
       associative(S,s);
       identity(S,s,z);
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} ==   add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- product
       (a:%) + (b:%):% == per(s(rep(a),rep(b)));

       -- Repeated squaring
       (x:%)^(n:NonNegativeInteger):% == {
         import from Integer,NonNegativeInteger;
         (n = 0) => return 0;
         odd?(n::Integer) => return x+(x+x)^shift(n,-1);
         return (x+x)^shift(n,-1);
       };

       -- unit
       0 == per(z);
}

MyAbelianGroup(S:SetCategory, s:(S,S)->S, inv:S->S, z:S): with {
       commutative(S,s);
       associative(S,s);
       identity(S,s,z);
       inverse(S,s,inv,z);
       -:% -> %;
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == MyAbelianMonoid(S,s,z) add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- inverse
       -(a:%):% == per(inv(rep(a)));
}
\end{aldor}

MyAbelianMonoid is a MyMonoid. MyAbelianGroup is a MyGroup and a MyMonoid.
\begin{axiom}
)sh MyAbelianMonoid
)sh MyMonoid(MyAbelianMonoid(INT,+,0),+,0)
)sh MyAbelianGroup
)sh MyGroup(MyAbelianGroup(INT,+,-,0),+,-,0)
)sh MyMonoid(MyAbelianGroup(INT,+,-,0),+,0)
\end{axiom}

Define a ring:
\begin{aldor}
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
#library MyGroup "mygroup.ao";
import from MyGroup;
#library MyAbelianGroup "myabeliangroup.ao";
import from MyAbelianGroup;

define distributes(S:SetCategory, m:(S,S)->S, s:(S,S)->S): Category == with {
  default ForAll(a:S,b:S,c:S):Boolean ==
    m(a,s(b,c)) = s(m(a,b),m(a,c)) and
    m(s(a,b),c) = s(m(a,c),m(b,c));
};

MyRing(S:SetCategory, s:(S,S)->S, inv:S->S, z:S, m:(S,S)->S, u:S): with {
       distributes(S,m,s);
       associative(S,s);
       commutative(S,s);
       identity(S,s,z);
       inverse(S,m,inv,z);
       associative(S,m);
       identity(S,m,u);
       *:(%,%) -> %;
       1: %;
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == {
     MyAbelianGroup(S,s,inv,z);
     MyMonoid(S,m,u);
} add { }
\end{aldor}

It looks like this.
\begin{axiom}
)sh MyRing
\end{axiom}

Integer is a MyRing.
\begin{axiom}
x3:=3::MyRing(Integer,+,-,0,*,1)
y3:=~x3
z3:=x3*y3
w3:=x2+z3
\end{axiom}

<hr />

Martin Rubey discovered a way to use the Aldor 'extend' construct
to add 'Monoid(Integer,*,1)' as a category to an existing domain,
thus in principle also allowing this to be distinguished from
'Monoid(Integer,+,0)' in a 'if ... has ...' statement. But there
may be problems. See: [SandBox Monoid Extend].



spad
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))
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/5748985099523682154-25px001.spad using 
      old system compiler.
------------------------------------------------------------------------
   initializing NRLIB MONOID for Monoid 
   compiling into NRLIB MONOID 

;;;     ***       |Monoid| REDEFINED
Time: 0 SEC.

   finalizing NRLIB MONOID 
   Processing Monoid for Browser database:
--------(m (% % %))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/MONOID.spad-->Monoid((m (% % %))): Improper first word in comments: returns
"returns the product of \\spad{x} and \\spad{y}"
--------(u (%))---------
--------(associative (attribute m))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/MONOID.spad-->Monoid((associative (attribute m))): Improper first word in comments: m
"\\spad{m}(a,{}\\spad{m}(\\spad{b},{}\\spad{c})) = \\spad{m}(\\spad{m}(a,{}\\spad{b}),{}\\spad{c})"
--------(identity (attribute u))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/MONOID.spad-->Monoid((identity (attribute u))): Improper first word in comments: m
"\\spad{m}(a,{}\\spad{u}) = \\spad{m}(\\spad{u},{}a) = a"
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/MONOID.spad-->Monoid(constructor): Not documented!!!!
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/MONOID.spad-->Monoid(): Missing Description
------------------------------------------------------------------------
   Monoid is now explicitly exposed in frame initial 
   Monoid will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MONOID.NRLIB/code

------------------------------------------------------------------------
   initializing NRLIB GROUP for Group 
   compiling into NRLIB GROUP 

;;;     ***       |Group| REDEFINED
Time: 0 SEC.

   finalizing NRLIB GROUP 
   Processing Group for Browser database:
--------(inv (% %))---------
--------(inverse (attribute m inv))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/GROUP.spad-->Group((inverse (attribute m inv))): Improper first word in comments: m
"\\spad{m}(inv(a),{}a) = \\spad{m}(a,{}inv(a)) = \\spad{u}"
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/GROUP.spad-->Group(constructor): Not documented!!!!
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/GROUP.spad-->Group(): Missing Description
------------------------------------------------------------------------
   Group is now explicitly exposed in frame initial 
   Group will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/GROUP.NRLIB/code

------------------------------------------------------------------------
   initializing NRLIB ABELGRP for AbelianGroup 
   compiling into NRLIB ABELGRP 

;;;     ***       |AbelianGroup| REDEFINED
Time: 0 SEC.

   finalizing NRLIB ABELGRP 
   Processing AbelianGroup for Browser database:
--------(commutative (attribute m))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/ABELGRP.spad-->AbelianGroup((commutative (attribute m))): Improper first word in comments: m
"\\spad{m}(a,{}\\spad{b}) = \\spad{m}(\\spad{b},{}a)"
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/ABELGRP.spad-->AbelianGroup(constructor): Not documented!!!!
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/ABELGRP.spad-->AbelianGroup(): Missing Description
------------------------------------------------------------------------
   AbelianGroup is now explicitly exposed in frame initial 
   AbelianGroup will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/ABELGRP.NRLIB/code

------------------------------------------------------------------------
   initializing NRLIB RING for Ring 
   compiling into NRLIB RING 

;;;     ***       |Ring| REDEFINED
Time: 0.01 SEC.

   finalizing NRLIB RING 
   Processing Ring for Browser database:
--------(distributes (attribute m s))---------
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/RING.spad-->Ring((distributes (attribute m s))): Improper first word in comments: m
"\\spad{m}(a,{}\\spad{s}(\\spad{b},{}\\spad{c})) = \\spad{s}(\\spad{m}(a,{}\\spad{b}),{}\\spad{m}(a,{}\\spad{c})) \\spad{m}(\\spad{s}(a,{}\\spad{b}),{}\\spad{c}) = \\spad{s}(\\spad{m}(a,{}\\spad{c}),{}\\spad{m}(\\spad{b},{}\\spad{c}))"
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/RING.spad-->Ring(constructor): Not documented!!!!
--->/usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/RING.spad-->Ring(): Missing Description
------------------------------------------------------------------------
   Ring is now explicitly exposed in frame initial 
   Ring will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/RING.NRLIB/code

axiom
)sh Ring(+,-,"0"::Symbol,*,"1"::Symbol)

 Ring(+,-,0,*,1) is a category constructor.
 Abbreviation for Ring is RING
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/5748985099523682154-25px001.spad to see algebra source
code for RING 

------------------------------- Operations --------------------------------

 ?*? : (%,%) -> %                      ?+? : (%,%) -> %
 -? : % -> %                           0 : () -> %
 1 : () -> %                          

Ring(+,-,"0"::Symbol,*,"1"::Symbol) has commutative(+)
LatexWiki Image(1)
Type: Boolean

Let's try this ... 

axiom
)sh Ring(a,b,c,d,e)

 Ring(a,b,c,d,e) is a category constructor.
 Abbreviation for Ring is RING
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/5748985099523682154-25px001.spad to see algebra source
code for RING 

------------------------------- Operations --------------------------------

 a : (%,%) -> %                        b : % -> %
 c : () -> %                           d : (%,%) -> %
 e : () -> %                          

Ring(a,b,c,d,e) has commutative(a)
LatexWiki Image(2)
Type: Boolean

Interesting! Is it somewhere written that "has" can have a category as its first argument?

OK, we are going to implement... 

spad
)abbrev domain MYINT MyInteger
MyInteger: Ring(a,b,c,d,e) == add
  Rep:=Integer
  a(x: %, y: %): % == x
  b(x: %): % == x
  c(): % == 0 pretend %
  d(x: %, y: %): % == x
  e(): % == 0 pretend %
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/4007632824524312372-25px004.spad using 
      old system compiler.
   MYINT abbreviates domain MyInteger 
------------------------------------------------------------------------
   initializing NRLIB MYINT for MyInteger 
   compiling into NRLIB MYINT 
   compiling local a : ($,$) -> $
      MYINT;a is replaced by x 
Time: 0 SEC.

   compiling local b : $ -> $
      MYINT;b is replaced by x 
Time: 0.01 SEC.

   compiling local c : () -> $
      MYINT;c is replaced by 0 
Time: 0 SEC.

   compiling local d : ($,$) -> $
      MYINT;d is replaced by x 
Time: 0 SEC.

   compiling local e : () -> $
      MYINT;e is replaced by 0 
Time: 0 SEC.

   >> System error:
   The index, 7, is too large.

Oops, that's not so easy. Have I made some error? (You originally wrote begin{axiom} but this is spad code.

... --kratt6, Thu, 02 Mar 2006 08:46:49 -0600 reply
Unfortunately, this won't work. For example in the above definition of Monoid, we are effectively creating to different things with the same name, but different types. We have an m of type Symbol, and another one of type (%,%)->%. As soon as we add a default implementation, this mistake surfaces:

spad
)abbrev category MYMON MyMonoid
MyMonoid(m:Symbol): Category == with
       m:(%,%) -> %
       square:% -> %
     add
       square(a:%):% == m(a,a)$%
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/1161784151565736029-25px005.spad using 
      old system compiler.
   MYMON abbreviates category MyMonoid 
------------------------------------------------------------------------
   initializing NRLIB MYMON for MyMonoid 
   compiling into NRLIB MYMON 

;;;     ***       |MyMonoid| REDEFINED
Time: 0 SEC.

   MYMON- abbreviates domain MyMonoid& 
------------------------------------------------------------------------
   initializing NRLIB MYMON- for MyMonoid& 
   compiling into NRLIB MYMON- 
   compiling exported square : S -> S
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MyMonoid&| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor MyMonoid&
      Time: 0 seconds

   finalizing NRLIB MYMON- 
   Processing MyMonoid& for Browser database:
--->-->MyMonoid&((m (% % %))): Not documented!!!!
--->-->MyMonoid&((square (% %))): Not documented!!!!
--->-->MyMonoid&(constructor): Not documented!!!!
--->-->MyMonoid&(): Missing Description
------------------------------------------------------------------------
   MyMonoid& is now explicitly exposed in frame initial 
   MyMonoid& will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MYMON-.NRLIB/code
   finalizing NRLIB MYMON 
   Processing MyMonoid for Browser database:
--->-->MyMonoid((m (% % %))): Not documented!!!!
--->-->MyMonoid((square (% %))): Not documented!!!!
--->-->MyMonoid(constructor): Not documented!!!!
--->-->MyMonoid(): Missing Description
------------------------------------------------------------------------
   MyMonoid is now explicitly exposed in frame initial 
   MyMonoid will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MYMON.NRLIB/code

spad
)abbrev domain WORD Word
Word(c:Symbol): MyMonoid(c) with 
    coerce:String -> %
    coerce:% -> OutputForm
  == add
    Rep := String
    coerce(a:String):% == a pretend %
    coerce(x:%):OutputForm == message(x pretend String)$OutputForm
    c(a:%, b:%):% == concat(a::Rep, b::Rep)
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/4459260466707001674-25px006.spad using 
      old system compiler.
   WORD abbreviates domain Word 
------------------------------------------------------------------------
   initializing NRLIB WORD for Word 
   compiling into NRLIB WORD 
   compiling exported coerce : String -> $
      WORD;coerce;S$;1 is replaced by a 
Time: 0.01 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0.01 SEC.

   compiling exported c : ($,$) -> $
      WORD;c;3$;3 is replaced by STRCONC 
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Word| REDEFINED

;;;     ***       |Word| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] coerce: pretend$ -- should replace by @

   Cumulative Statistics for Constructor Word
      Time: 0.02 seconds

   finalizing NRLIB WORD 
   Processing Word for Browser database:
--->-->Word((coerce (% (String)))): Not documented!!!!
--->-->Word((coerce ((OutputForm) %))): Not documented!!!!
--->-->Word(constructor): Not documented!!!!
--->-->Word(): Missing Description
------------------------------------------------------------------------
   Word is now explicitly exposed in frame initial 
   Word will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/WORD.NRLIB/code

axiom
)sh Word

 Word c: Symbol  is a domain constructor
 Abbreviation for Word is WORD
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/4459260466707001674-25px006.spad to see algebra source
code for WORD 

------------------------------- Operations --------------------------------
 c : (%,%) -> %                        coerce : % -> OutputForm
 coerce : String -> %                  square : % -> %

axiom
)sh Word("p"::Symbol)

 Word p is a domain constructor.
 Abbreviation for Word is WORD
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/4459260466707001674-25px006.spad to see algebra source
code for WORD 

------------------------------- Operations --------------------------------

 coerce : % -> OutputForm              coerce : String -> %
 p : (%,%) -> %                        square : % -> %

w1:="a"::Word("p"::Symbol)
LatexWiki Image(3)
Type: Word p
axiom
w2:="b"::Word("p"::Symbol)
LatexWiki Image(4)
Type: Word p
axiom
p(w1,w2)$Word("p"::Symbol)

   The function p is not implemented in Word p .
p(w1,w1)$Word("p"::Symbol)

   The function p is not implemented in Word p .
square(w1)$Word("p"::Symbol)

Function:  m : (%,%) -> % is missing from domain: Word p
   Internal Error
   The function m with signature $$$ is missing from domain Wordp

What we really would like to have would be something along the lines of: 

spad
)abbrev category MYMON1 MyMonoid1
MyMonoid1(S:SetCategory, m: (S,S)-> S): Category == with
       m: (S,S)-> S
       square: S -> S
     add
       m
       square a == m(a,a)
spad
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/6825787861264248532-25px008.spad using 
      old system compiler.
   MYMON1 abbreviates category MyMonoid1 
------------------------------------------------------------------------
   initializing NRLIB MYMON1 for MyMonoid1 
   compiling into NRLIB MYMON1 

;;;     ***       |MyMonoid1| REDEFINED
Time: 0 SEC.

   MYMON1- abbreviates domain MyMonoid1& 
------------------------------------------------------------------------
   initializing NRLIB MYMON1- for MyMonoid1& 
   compiling into NRLIB MYMON1- 
   compiling exported square : S -> S
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MyMonoid1&| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] unknown Functor code m

   Cumulative Statistics for Constructor MyMonoid1&
      Time: 0 seconds

   finalizing NRLIB MYMON1- 
   Processing MyMonoid1& for Browser database:
--->-->MyMonoid1&((m (S S S))): Not documented!!!!
--->-->MyMonoid1&((square (S S))): Not documented!!!!
--->-->MyMonoid1&(constructor): Not documented!!!!
--->-->MyMonoid1&(): Missing Description
------------------------------------------------------------------------
   MyMonoid1& is now explicitly exposed in frame initial 
   MyMonoid1& will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MYMON1-.NRLIB/code
   finalizing NRLIB MYMON1 
   Processing MyMonoid1 for Browser database:
--->-->MyMonoid1((m (S S S))): Not documented!!!!
--->-->MyMonoid1((square (S S))): Not documented!!!!
--->-->MyMonoid1(constructor): Not documented!!!!
--->-->MyMonoid1(): Missing Description
------------------------------------------------------------------------
   MyMonoid1 is now explicitly exposed in frame initial 
   MyMonoid1 will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MYMON1.NRLIB/code

axiom
)sh MyMonoid1

 MyMonoid1(S: SetCategory,m: ((t#1,t#1) -> t#1))  is a category
constructor
 Abbreviation for MyMonoid1 is MYMON1
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/6825787861264248532-25px008.spad to see algebra source
code for MYMON1 

------------------------------- Operations --------------------------------
 m : (S,S) -> S                        square : S -> S

axiom
)set functions compile on

m1:=(a:String,b:String):String+->concat(a,b)
LatexWiki Image(5)
Type: ((String,String) -> String)
axiom
m1("aaa","bbb")
LatexWiki Image(6)
Type: String
axiom
)sh MyMonoid1(String,m1)

 MyMonoid1(String,LAMBDA-CLOSURE(G1567 G1568 envArg)(SPADCALL G1567 G1568 (ELT
*2;anonymousFunction;0;initial;internal;MV 0))) is a category constructor.
 Abbreviation for MyMonoid1 is MYMON1
 This constructor is exposed in this frame.
 Issue )edit /var/zope2/var/LatexWiki/6825787861264248532-25px008.spad to see algebra source
code for MYMON1 

------------------------------- Operations --------------------------------

 square : String -> String
 (LAMBDA-CLOSURE    (G1567 G1568 envArg) (SPADCALL G1567 G1568 (ELT
*2;anonymousFunction;0;initial;internal;MV 0))) : (String,String) -> String

m2(a:String,b:String):String==concat(a,b)

   Function declaration m2 : (String,String) -> String has been added
      to workspace.
Type: Void
axiom
m2("aaa","bbb")
axiom
Compiling function m2 with type (String,String) -> String
LatexWiki Image(7)
Type: String
axiom
)sh MyMonoid1(String,m2)

   >> System error:
   The function MAP is undefined.

Then: 

  Word: MyMonoid1(String,(a:String,b:String):String+->concat(a,b)) with
      coerce: String -> %
    == add

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

However, there are two problems here:

  • it is not possible to refer to the category to be defined in the parameter, as in MyMonoid(m: (%,%)-> %)
  • it is not possible to refer to an operation which is not yet defined as in Word: MyMonoid(c) with

Martin

scope of names in default implementation of categories --Bill Page, Thu, 02 Mar 2006 09:42:18 -0600 reply
Martin wrote:
Unfortunately, this won't work. For example in the above definition of Monoid, we are effectively creating to different things with the same name, but different types. We have an m of type Symbol, and another one of type (%,%)->%.

I agree that there is a scope issue here. Perhaps it comes from the idea of allowing default implementation as part of the category definition. But I think the proper semantics are quite easy to define. The exports need to have priority over the parameters. The m of type Symbol is not exported by MyMonoid but the m of type (%,%)-> % is exported. The m in the implementation m(a,a) should refer to m that is being exported.

So I think this is a compiler error.

generic monoids in Aldor --Bill Page, Fri, 03 Mar 2006 15:46:42 -0600 reply
Based on an idea posted to this page by Martin Rubey, I have constructed what I think is a good facsimile of a generic monoid. I think think that this construction is only possible in Aldor.

The idea is basically to specify a monoid as a tuple in the usual manner, consisting of a set S, an associative binary operator m and unit u. In this example MyMonoid? exports two operations and a constant: * for the binary operation in the monoid (whatever it happens to be), ^ for repeated * repeated n times, and 1 denoting the ring identity.

This is rather different that the notion that we started with in this thread - in fact more or less the opposite: from any more complex domain we can extract the monoid part. Of course this is fundamentally very simple, just as it should be. :)

aldor
#include "axiom"

define associative(S:SetCategory, m:(S,S)->S):Category == with {
  default ForAll(a:S,b:S,c:S):Boolean == m(a,m(b,c)) = m(m(a,b),c);
};

define identity(S:SetCategory, m:(S,S)->S, u:S): Category == with {
  default ForAll(a:S):Boolean == m(a,u) = a and m(u,a) = a;
};

MyMonoid(S:SetCategory, m:(S,S)->S, u:S): with {
       associative(S,m);
       identity(S,m,u);
       *:(%,%) -> %;
       1: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} ==   add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- product
       (a:%) * (b:%):% == per(m(rep(a),rep(b)));

       -- Repeated squaring
       (x:%)^(n:NonNegativeInteger):% == {
         import from Integer,NonNegativeInteger;
         (n = 0) => return 1;
         odd?(n::Integer) => return x*(x*x)^shift(n,-1);
         return (x*x)^shift(n,-1);
       };

       -- unit
       1 == per(u);
}
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/mymonoid.as using AXIOM-XL compiler and 
      options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file ./mymonoid.lsp
   Issuing )library command for mymonoid
   Reading /var/zope2/var/LatexWiki/mymonoid.asy
   identity is now explicitly exposed in frame initial 
   identity will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mymonoid
   associative is now explicitly exposed in frame initial 
   associative will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mymonoid
   MyMonoid is already explicitly exposed in frame initial 
   MyMonoid will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mymonoid

This is how the MyMonoid domain looks to the Axiom interpreter. 

axiom
)sh MyMonoid

 MyMonoid(S: SetCategory,m: ((S,S) -> S),u: S)  is a domain constructor
 Abbreviation for MyMonoid is MYMON
 This constructor is exposed in this frame.
 Issue )edit mymonoid.as to see algebra source code for MYMON 

------------------------------- Operations --------------------------------
 ?*? : (%,%) -> %                      1 : () -> %
 ForAll : (S,S,S) -> Boolean           ForAll : S -> Boolean
 coerce : S -> %                       coerce : % -> OutputForm
 ?^? : (%,NonNegativeInteger) -> %

axiom
)sh MyMonoid(String,concat,"")

 MyMonoid(String,theMap(ISTRING;concat;3$;7,928),) is a domain constructor.
 Abbreviation for MyMonoid is MYMON
 This constructor is exposed in this frame.
 Issue )edit mymonoid.as to see algebra source code for MYMON 

------------------------------- Operations --------------------------------

 ?*? : (%,%) -> %                      1 : () -> %
 ForAll : String -> Boolean            coerce : % -> OutputForm
 coerce : String -> %
 ForAll : (String,String,String) -> Boolean
 ?^? : (%,NonNegativeInteger) -> %


axiom
)sh MyMonoid(List INT,concat,[])

 MyMonoid(List Integer,theMap(STAGG-;concat;3A;7,436),[]) is a domain constructor.
 Abbreviation for MyMonoid is MYMON
 This constructor is exposed in this frame.
 Issue )edit mymonoid.as to see algebra source code for MYMON 

------------------------------- Operations --------------------------------

 ?*? : (%,%) -> %                      1 : () -> %
 ForAll : List Integer -> Boolean      coerce : % -> OutputForm
 coerce : List Integer -> %
 ForAll : (List Integer,List Integer,List Integer) -> Boolean
 ?^? : (%,NonNegativeInteger) -> %

Here is Martin Rubey's String monoid example: 

axiom
w1:="a"::MyMonoid(String,concat,"")
LatexWiki Image(8)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
w2:="b"::MyMonoid(String,concat,"")
LatexWiki Image(9)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
w1*w2
LatexWiki Image(10)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
w1*w1
LatexWiki Image(11)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
w1^10
LatexWiki Image(12)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
w1*1$MyMonoid(String,concat,"")
LatexWiki Image(13)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)
axiom
1$MyMonoid(String,concat,"")*w1
LatexWiki Image(14)
Type: MyMonoid?(String,theMap(ISTRING;concat;3$;7,928),)

And of course we can construct a large number of other examples. 

axiom
i1:=[1,2]::MyMonoid(List INT, concat,[])
LatexWiki Image(15)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
i2:=[3]::MyMonoid(List INT, concat,[])
LatexWiki Image(16)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
i1*i2
LatexWiki Image(17)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
i1*i1
LatexWiki Image(18)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
i1^3
LatexWiki Image(19)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
i1*1$MyMonoid(List INT, concat,[])
LatexWiki Image(20)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])
axiom
1$MyMonoid(List INT, concat,[])*i1
LatexWiki Image(21)
Type: MyMonoid?(List Integer,theMap(STAGG-;concat;3A;7,436),[])

axiom
i1:=10::MyMonoid(INT, +, 0)
LatexWiki Image(22)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
i2:=20::MyMonoid(INT, +, 0)
LatexWiki Image(23)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
i1*i2
LatexWiki Image(24)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
i1*i1
LatexWiki Image(25)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
i1^0
LatexWiki Image(26)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
i1*1$MyMonoid(INT, +, 0)
LatexWiki Image(27)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)
axiom
1$MyMonoid(INT, +, 0)*i1
LatexWiki Image(28)
Type: MyMonoid?(Integer,theMap(INT;+;3$;37,36),0)

axiom
i1:=10.1::MyMonoid(Float, *, 1)
LatexWiki Image(29)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
i2:=20.2::MyMonoid(Float, *, 1)
LatexWiki Image(30)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
i1*i2
LatexWiki Image(31)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
i1*i1
LatexWiki Image(32)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
i1^4
LatexWiki Image(33)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
i1*1$MyMonoid(Float, *, 1)
LatexWiki Image(34)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)
axiom
1$MyMonoid(Float, *, 1)*i1
LatexWiki Image(35)
Type: MyMonoid?(Float,theMap(FLOAT;*;3$;79,296),1.0)

Now try to define a group.

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;

define inverse(S:SetCategory, m:(S,S)->S, inv:S->S, u:S): Category == with {
  default ForAll(a:S):Boolean == m(inv(a),a)=u and m(a,inv(a))=u;
};

MyGroup(S:SetCategory, m:(S,S)->S, inv:S->S, u:S): with {
       associative(S,m);
       identity(S,m,u);
       inverse(S,m,inv,u);
       ~:% -> %;
       *:(%,%) -> %;
       1: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == MyMonoid(S,m,u) add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- inverse
       ~(a:%):% == per(inv(rep(a)));
}
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/mygroup.as using AXIOM-XL compiler and 
      options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file ./mygroup.lsp
   Issuing )library command for mygroup
   Reading /var/zope2/var/LatexWiki/mygroup.asy
   inverse is now explicitly exposed in frame initial 
   inverse will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mygroup
   MyGroup is now explicitly exposed in frame initial 
   MyGroup will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mygroup

This is how the MyGroup domain looks to the Axiom interpreter. 

axiom
)sh MyGroup

 MyGroup(S: SetCategory,m: ((S,S) -> S),inv: (S -> S),u: S)  is a domain
constructor
 Abbreviation for MyGroup is MYGROUP
 This constructor is exposed in this frame.
 Issue )edit mygroup.as to see algebra source code for MYGROUP 

------------------------------- Operations --------------------------------
 ?*? : (%,%) -> %                      1 : () -> %
 ForAll : (S,S,S) -> Boolean           ForAll : S -> Boolean
 coerce : S -> %                       coerce : % -> OutputForm
 ~? : % -> %
 ?^? : (%,NonNegativeInteger) -> %

axiom
)sh MyGroup(INT,+,-,0)

 MyGroup(Integer,theMap(INT;+;3$;37,904),theMap(INT;-;2$;36,904),0) is a domain
constructor.
 Abbreviation for MyGroup is MYGROUP
 This constructor is exposed in this frame.
 Issue )edit mygroup.as to see algebra source code for MYGROUP 

------------------------------- Operations --------------------------------

 ?*? : (%,%) -> %                      1 : () -> %
 ForAll : Integer -> Boolean           coerce : % -> OutputForm
 coerce : Integer -> %                 ~? : % -> %
 ForAll : (Integer,Integer,Integer) -> Boolean
 ?^? : (%,NonNegativeInteger) -> %

For example: 

axiom
x:=3::MyGroup(INT,+,-,0)
LatexWiki Image(36)
Type: MyGroup?(Integer,theMap(INT;+;3LatexWiki Image;36,904),0)
axiom
y:=~x
LatexWiki Image(37)
Type: MyGroup?(Integer,theMap(INT;+;3LatexWiki Image;36,904),0)
axiom
x*y
LatexWiki Image(38)
Type: MyGroup?(Integer,theMap(INT;+;3LatexWiki Image;36,904),0)

A different issue? --wyscc, Wed, 08 Mar 2006 12:35:43 -0600 reply
I am not impressed. However, this kind of finessed the whole issue of notation and neglected the dual inheritance situation, and I expect one will get into trouble when one wants to go on to MyRing. Any domain in MyRing should work without unnecessary package calls in the Interpreter. All this mechanism did was passing a function m to constructors, here to be used as the monoid categorically defined multiplication. This technique has been used before, in Axiom, in GDMP. The notation in an Interpreter session is still *, the operator declared in MyMonoid. So even though we have MyMonoid(INT,+,0) and we can compute using i1*i2 to really get the sum of i1 and i2, this is not using + notation. Notice also that MyGroup should have been implemented as a category constructor. In )sh MyGroup, the group operation is *, the unit is 1 and the inverse is - (which is incompatible with * and wrong, since a group should not be commutative in general). But these last two comments are minor quibbles and easily corrected.

I indicated before that I believe one needs to make some deeper changes to implement inheritance that would support notational changes in a way such that multiple inheritance of MyMonoid to the same domain constructor can distinguish the operators. Any proposed solution under the currently available systems, if possible at all, should include MyRing (as a category, not domain) and MyInteger as a domain in MyRing.

I am more interested in the associative category and the ForAll in Aldor. How exactly does that differ from Axiom? ForAll seems to be only a case by case verification, given actual elements of the domain.

William

Re: A different issue? --Bill Page, Wed, 08 Mar 2006 21:45:13 -0600 reply
William, it seems to me that you are easily not impressed ;) But thanks for your comments.

I agree that the second half of this page implements a different structure than the first half - I said as much above. It is in a formal sense the exact opposite thing. But opposites can be useful. I am working out the details here because I am hoping that in the end we can see the issue of inheritance more precisely as the dual to this construction.

The point here is that MyGroup(INT,+,-,0) declares that this combination of domain, operations and constant constitutes a group. It does not attempt to construct this group in INT but rather it extracts this part of INT as a subdomain having the structure of a group: 

    MyGroup(INT,+,-,0) >-----> INT
    with *, ~, 1               with +, -, 0, *, /, 1,  ...

In categorical terms both MyMonoid and MyGroup are monomorhic functors, i.e. subdomain constructors.

(Note that I changed the notation for inverse in MyGroup to ~ so that perhaps it is less confusing.)

MyGroup is not implemented as a category constructor because as I said, the intent here is not to construct MyInteger by inheritance. In this case the implementation of Integer is given and we are simply identifying parts of it.

Inheritance does require something similiar: 

    MyInteger: Join(Group(%,+,-,0), Monoid(%, *, 1), ...
                    with *, ~, 1    with *, 1

In this case the categories Group, Monoid, etc. are given and we wish to provide new names for their operations in MyInteger as suggested by Ralf. Unfortunately as Martin demonstrated on the first part of this page, the SPAD compiler does not compile it correctly. Maybe we can still find a way to do this with Aldor. I haven't given up yet, I am just working on a different aspect of the problem.

The associative category as I implemented it above in Aldor can also be written this way in SPAD. But as far as I know Aldor does not implement Axiom's axioms (assertions) so in Aldor these must be coded as categories with a possibly empty with { } clause.

ForAll is not an Aldor primitive construct, it is just a simple export that is intended to express the axioms in a manner that could be used in some kind of theorem proving subsystem (which does not exist yet :). You are right however that this could very easily be used to implement an automatic verification system. Such as system could least provide useful counter examples when the axioms fail.

I am still thinking about how best to encode these sort of axioms, so the ForAll construct above is likely to change a little.

Stay tuned to this channel ...

Define an Abelian (commutative) group: 

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
#library MyGroup "mygroup.ao";
import from MyGroup;

define commutative(S:SetCategory, m:(S,S)->S): Category == with {
  default ForAll(a:S,b:S):Boolean == m(a,b) = m(b,a);
};

MyAbelianMonoid(S:SetCategory, s:(S,S)->S, z:S): with {
       commutative(S,s);
       associative(S,s);
       identity(S,s,z);
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} ==   add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- product
       (a:%) + (b:%):% == per(s(rep(a),rep(b)));

       -- Repeated squaring
       (x:%)^(n:NonNegativeInteger):% == {
         import from Integer,NonNegativeInteger;
         (n = 0) => return 0;
         odd?(n::Integer) => return x+(x+x)^shift(n,-1);
         return (x+x)^shift(n,-1);
       };

       -- unit
       0 == per(z);
}

MyAbelianGroup(S:SetCategory, s:(S,S)->S, inv:S->S, z:S): with {
       commutative(S,s);
       associative(S,s);
       identity(S,s,z);
       inverse(S,s,inv,z);
       -:% -> %;
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == MyAbelianMonoid(S,s,z) add {
       Rep == S;
       coerce(a: S): % == per(a);
       coerce(x:%):OutputForm == coerce(rep(x))$S;

       -- inverse
       -(a:%):% == per(inv(rep(a)));
}
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/myabeliangroup.as using AXIOM-XL 
      compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file ./myabeliangroup.lsp
   Issuing )library command for myabeliangroup
   Reading /var/zope2/var/LatexWiki/myabeliangroup.asy
   commutative is now explicitly exposed in frame initial 
   commutative will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/myabeliangroup
   MyAbelianGroup is now explicitly exposed in frame initial 
   MyAbelianGroup will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/myabeliangroup
   MyAbelianMonoid is now explicitly exposed in frame initial 
   MyAbelianMonoid will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/myabeliangroup

MyAbelianMonoid? is a MyMonoid?. MyAbelianGroup? is a MyGroup? and a MyMonoid?. 

axiom
)sh MyAbelianMonoid

 MyAbelianMonoid(S: SetCategory,s: ((S,S) -> S),z: S)  is a domain constructor
 Abbreviation for MyAbelianMonoid is MYABELI
 This constructor is exposed in this frame.
 Issue )edit myabeliangroup.as to see algebra source code for MYABELI 

------------------------------- Operations --------------------------------
 ?+? : (%,%) -> %                      0 : () -> %
 ForAll : (S,S) -> Boolean             ForAll : (S,S,S) -> Boolean
 ForAll : S -> Boolean                 coerce : S -> %
 coerce : % -> OutputForm
 ?^? : (%,NonNegativeInteger) -> %

axiom
)sh MyMonoid(MyAbelianMonoid(INT,+,0),+,0)

   MyMonoid(MyAbelianMonoid(Integer,+,0),+,0) is not a valid type.
axiom
)sh MyAbelianGroup

 MyAbelianGroup(S: SetCategory,s: ((S,S) -> S),inv: (S -> S),z: S)  is a
domain constructor
 Abbreviation for MyAbelianGroup is MYABELI
 This constructor is exposed in this frame.
 Issue )edit myabeliangroup.as to see algebra source code for MYABELI 

------------------------------- Operations --------------------------------
 ?+? : (%,%) -> %                      -? : % -> %
 0 : () -> %                           ForAll : (S,S) -> Boolean
 ForAll : (S,S,S) -> Boolean           ForAll : S -> Boolean
 coerce : S -> %                       coerce : % -> OutputForm
 ?^? : (%,NonNegativeInteger) -> %

axiom
)sh MyGroup(MyAbelianGroup(INT,+,-,0),+,-,0)

   MyGroup(MyAbelianGroup(Integer,+,-,0),+,-,0) is not a valid type.
axiom
)sh MyMonoid(MyAbelianGroup(INT,+,-,0),+,0)

   MyMonoid(MyAbelianGroup(Integer,+,-,0),+,0) is not a valid type.

Define a ring: 

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
#library MyGroup "mygroup.ao";
import from MyGroup;
#library MyAbelianGroup "myabeliangroup.ao";
import from MyAbelianGroup;

define distributes(S:SetCategory, m:(S,S)->S, s:(S,S)->S): Category == with {
  default ForAll(a:S,b:S,c:S):Boolean ==
    m(a,s(b,c)) = s(m(a,b),m(a,c)) and
    m(s(a,b),c) = s(m(a,c),m(b,c));
};

MyRing(S:SetCategory, s:(S,S)->S, inv:S->S, z:S, m:(S,S)->S, u:S): with {
       distributes(S,m,s);
       associative(S,s);
       commutative(S,s);
       identity(S,s,z);
       inverse(S,m,inv,z);
       associative(S,m);
       identity(S,m,u);
       *:(%,%) -> %;
       1: %;
       +:(%,%) -> %;
       0: %;
       ^:(%,NonNegativeInteger) -> %;  ++ a^0 = 1, a*a^n = a^(n+1)
       coerce: S -> %;
       coerce: % -> OutputForm;
} == {
     MyAbelianGroup(S,s,inv,z);
     MyMonoid(S,m,u);
} add { }
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/4246596118391608395-25px022.as using 
      AXIOM-XL compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
"/var/zope2/var/LatexWiki/4246596118391608395-25px022.as", line 32: 
     MyMonoid(S,m,u);
.....^
[L32 C6] #2 (Error) No one possible return type satisfies the context type.
  These possible return types were rejected:
          -- Join(associative(S, m), identity(S, m, u)) with 
             ...
  The context requires an expression of type 
                Join(distributes(S, m, s), associative(S, s),....

   The )library system command was not called after compilation.

It looks like this. 

axiom
)sh MyRing

   The )show system command is used to display information about types
      or partial types. For example, )show Integer will show
      information about Integer .

      MyRing is not the name of a known type constructor. If you want
      to see information about any operations named MyRing , issue
                         )display operations MyRing

Integer is a MyRing?. 

axiom
x3:=3::MyRing(Integer,+,-,0,*,1)

   Category, domain or package constructor MyRing is not available.
y3:=~x3

   There are 3 exposed and 0 unexposed library operations named ~
      having 1 argument(s) but none was determined to be applicable.
      Use HyperDoc Browse, or issue
                                )display op ~
      to learn more about the available operations. Perhaps
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named ~
      with argument type(s)
                                 Variable x3

      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
z3:=x3*y3
LatexWiki Image(39)
Type: Polynomial Integer
axiom
w3:=x2+z3
LatexWiki Image(40)
Type: Polynomial Integer

Martin Rubey discovered a way to use the Aldor extend construct to add Monoid(Integer,*,1) as a category to an existing domain, thus in principle also allowing this to be distinguished from Monoid(Integer,+,0) in a if ... has ... statement. But there may be problems. See: [SandBox Monoid Extend]?.