login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBox Monoid
  ↑ → SandBoxAbelianDuck

SandBox Monoid Extend
last edited 1 year ago

Edit detail for SandBox Monoid Extend revision 1 of 1
1
Editor:
Time: 2007/11/18 18:29:09 GMT-8
Note: 
changed:
-
Martin's beautiful idea:

  We can use the Aldor 'extend' construct to add 'MyMonoid(...)' as
a category to a previously defined domain.

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

MyMonoid(T: Type, m: (T, T) -> T): Category == with {
   square:T -> T;
   coerce:T -> OutputForm;
   default {
     -- This hack for output only works for domains that
     -- have a representation known to Lisp.
     coerce(x:T):OutputForm == x pretend OutputForm;
     square(t: T): T == m(t,t)
   }
}
\end{aldor}

\begin{aldor}
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyWord: with { 
   coerce: String -> %;
   c:(%, %) -> %;
   d:(%, %) -> %;
}
   == add {
   Rep == String;
   import from String;
   coerce(a: String): % == per(a);
   c(a: %, b: %):%  == per(concat(rep(a), rep(b)));
   d(a: %, b: %):%  == a;
}

import from MyWord;
extend MyWord: MyMonoid(MyWord, c) == add;
\end{aldor}

This is what Axiom sees:
\begin{axiom}
)sh MyMonoid
)sh MyWord
\end{axiom}

Try it:
\begin{axiom}
a := "Bingo"::MyWord
square a
MyWord has MyMonoid(MyWord, c)
\end{axiom}

That's pretty cool that Axiom knows 'MyWord' is a 'MyMonoid'!

But:
\begin{axiom}
MyWord has MyMonoid(MyWord, d)
\end{axiom}
Oops, that's **not** cool! :( Aldor and the Axiom interpreter
ought to be able to do better than this.

Here are some more examples:
\begin{aldor}
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyInt: with { 
   coerce: Integer -> %;
   +:(%, %) -> %;
}
   == add {
   Rep == Integer;
   import from Integer;
   coerce(a: Integer): % == per(a);
   (a:%) + (b:%):%  == per(rep(a)+rep(b))
}
import from MyInt;
extend MyInt: MyMonoid(MyInt, +) == add;
\end{aldor}

This is what Axiom sees:
\begin{axiom}
)sh MyInt
\end{axiom}

Try it:
\begin{axiom}
b := 3::MyInt
b+1
square b
\end{axiom}

This is very general. Notice that we can rename the monoid
operation from * to +!
\begin{aldor}
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyFloat: with { 
   coerce: DoubleFloat -> %;
   +:(%, %) -> %;
}
   == add {
   Rep == DoubleFloat;
   import from DoubleFloat;
   coerce(a: DoubleFloat): % == per(a);
   (a:%) + (b:%):%  == per(rep(a)*rep(b))
}
import from MyFloat;
extend MyFloat: MyMonoid(MyFloat, +) == add;
\end{aldor}

This is what Axiom sees:
\begin{axiom}
)sh MyFloat
\end{axiom}

Try it:
\begin{axiom}
f := 3.1::DoubleFloat::MyFloat
g := 2::DoubleFloat::MyFloat
-- The operator + in MyInt is * in Integer!
f+g
square f
\end{axiom}


Here's a variation on the example 'dirprod.as' posted by Ralf Hemmecke on 'Mon, 13 Mar 2006 14:33:34 +0100'
'[Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures'
            
\begin{aldor}[mydirprod]
#include "axiom"
define DirProdCat(n: Integer, R: Type): Category == with {
    identity: % -> %;
}
DirProd(n: Integer, R: Type): DirProdCat(n, R) == add {
    Rep == List Integer; -- dummy implementation
    import from Rep;
    identity(x: %): % == x;
 }
\end{aldor}

Try it:

\begin{axiom}
x:= Integer;
y:= NonNegativeInteger;
DPx ==> DirProd(2, x);
DPx has DirProdCat(2, x)
DPx has DirProdCat(2, y)
DPx has DirProdCat(3, x)
DPx has DirProdCat(3, y)
\end{axiom}

The results show that the Aldor compiler treats a domain (R) and an element of a domain (n) differently in terms of information retained for the 'has' operation. Had the 'Type' in 'R: Type' been replaced by 'Symbol' and the lines defining x, y removed, all results would have been 'true'. Notice here, contrary to Ralf's example, both the 'DirProdCat' and 'DirProd' constructors totally ignored the parameters. The two constructions 'DirProd(2,x)' and 'DirProd(2,y)' are really identical in implemetation. So the only information to distinguish 'DirProdCat(2,x)' and 'DirProdCat(2,y)' must have come from the declaration of the parameters (on the left of ':').

\begin{axiom}
)show DirProd(2,x)
)show DirProd(2,y)
\end{axiom}

Martin's beautiful idea:

We can use the Aldor extend construct to add MyMonoid(...) as a category to a previously defined domain.

aldor
#include "axiom"

MyMonoid(T: Type, m: (T, T) -> T): Category == with {
   square:T -> T;
   coerce:T -> OutputForm;
   default {
     -- This hack for output only works for domains that
     -- have a representation known to Lisp.
     coerce(x:T):OutputForm == x pretend OutputForm;
     square(t: T): T == m(t,t)
   }
}
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
   MyMonoid is now explicitly exposed in frame initial 
   MyMonoid will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mymonoid

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyWord: with { 
   coerce: String -> %;
   c:(%, %) -> %;
   d:(%, %) -> %;
}
   == add {
   Rep == String;
   import from String;
   coerce(a: String): % == per(a);
   c(a: %, b: %):%  == per(concat(rep(a), rep(b)));
   d(a: %, b: %):%  == a;
}

import from MyWord;
extend MyWord: MyMonoid(MyWord, c) == add;
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/9179840256381573157-25px002.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 
      ./9179840256381573157-25px002.lsp
   Issuing )library command for 9179840256381573157-25px002
   Reading /var/zope2/var/LatexWiki/9179840256381573157-25px002.asy
   MyWord is now explicitly exposed in frame initial 
   MyWord will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/9179840256381573157-25px002

This is what Axiom sees: 

axiom
)sh MyMonoid

 MyMonoid(T: Type,m: ((T,T) -> T))  is a category constructor
 Abbreviation for MyMonoid is MYMONOI
 This constructor is exposed in this frame.
 Issue )edit mymonoid.as to see algebra source code for MYMONOI 

------------------------------- Operations --------------------------------
 coerce : T -> OutputForm              square : T -> T

axiom
)sh MyWord

 MyWord  is a domain constructor
 Abbreviation for MyWord is MYWORD
 This constructor is exposed in this frame.
 Issue )edit 9179840256381573157-25px002.as to see algebra source code for MYWORD 

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

Try it: 

axiom
a := "Bingo"::MyWord
LatexWiki Image(1)
Type: MyWord?
axiom
square a
LatexWiki Image(2)
Type: MyWord?
axiom
MyWord has MyMonoid(MyWord, c)
LatexWiki Image(3)
Type: Boolean

That's pretty cool that Axiom knows MyWord is a MyMonoid!

But: 

axiom
MyWord has MyMonoid(MyWord, d)
LatexWiki Image(4)
Type: Boolean

Oops, that's not cool! :( Aldor and the Axiom interpreter ought to be able to do better than this.

Here are some more examples: 

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyInt: with { 
   coerce: Integer -> %;
   +:(%, %) -> %;
}
   == add {
   Rep == Integer;
   import from Integer;
   coerce(a: Integer): % == per(a);
   (a:%) + (b:%):%  == per(rep(a)+rep(b))
}
import from MyInt;
extend MyInt: MyMonoid(MyInt, +) == add;
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/797595480097738355-25px006.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 
      ./797595480097738355-25px006.lsp
   Issuing )library command for 797595480097738355-25px006
   Reading /var/zope2/var/LatexWiki/797595480097738355-25px006.asy
   MyInt is now explicitly exposed in frame initial 
   MyInt will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/797595480097738355-25px006

This is what Axiom sees: 

axiom
)sh MyInt

 MyInt  is a domain constructor
 Abbreviation for MyInt is MYINT
 This constructor is exposed in this frame.
 Issue )edit 797595480097738355-25px006.as to see algebra source code for MYINT 

------------------------------- Operations --------------------------------
 ?+? : (%,%) -> %                      coerce : Integer -> %
 coerce : MyInt -> OutputForm          square : MyInt -> MyInt

Try it: 

axiom
b := 3::MyInt
LatexWiki Image(5)
Type: MyInt?
axiom
b+1
LatexWiki Image(6)
Type: MyInt?
axiom
square b
LatexWiki Image(7)
Type: MyInt?

This is very general. Notice that we can rename the monoid operation from * to +! 

aldor
#include "axiom"
#library MyMonoid "mymonoid.ao";
import from MyMonoid;
MyFloat: with { 
   coerce: DoubleFloat -> %;
   +:(%, %) -> %;
}
   == add {
   Rep == DoubleFloat;
   import from DoubleFloat;
   coerce(a: DoubleFloat): % == per(a);
   (a:%) + (b:%):%  == per(rep(a)*rep(b))
}
import from MyFloat;
extend MyFloat: MyMonoid(MyFloat, +) == add;
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/4949806727147037492-25px009.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 
      ./4949806727147037492-25px009.lsp
   Issuing )library command for 4949806727147037492-25px009
   Reading /var/zope2/var/LatexWiki/4949806727147037492-25px009.asy
   MyFloat is now explicitly exposed in frame initial 
   MyFloat will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/4949806727147037492-25px009

This is what Axiom sees: 

axiom
)sh MyFloat

 MyFloat  is a domain constructor
 Abbreviation for MyFloat is MYFLOAT
 This constructor is exposed in this frame.
 Issue )edit 4949806727147037492-25px009.as to see algebra source code for MYFLOAT 

------------------------------- Operations --------------------------------
 ?+? : (%,%) -> %                      coerce : DoubleFloat -> %
 coerce : MyFloat -> OutputForm        square : MyFloat -> MyFloat

Try it: 

axiom
f := 3.1::DoubleFloat::MyFloat
LatexWiki Image(8)
Type: MyFloat?
axiom
g := 2::DoubleFloat::MyFloat
LatexWiki Image(9)
Type: MyFloat?
axiom
-- The operator + in MyInt is * in Integer!
f+g
LatexWiki Image(10)
Type: MyFloat?
axiom
square f
LatexWiki Image(11)
Type: MyFloat?

Here's a variation on the example dirprod.as posted by Ralf Hemmecke on Mon, 13 Mar 2006 14:33:34 +0100 'Axiom-developer Re: BINGO,Curiosities with Axiom mathematical structures'

aldor
#include "axiom"
define DirProdCat(n: Integer, R: Type): Category == with {
    identity: % -> %;
}
DirProd(n: Integer, R: Type): DirProdCat(n, R) == add {
    Rep == List Integer; -- dummy implementation
    import from Rep;
    identity(x: %): % == x;
 }
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/mydirprod.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 ./mydirprod.lsp
   Issuing )library command for mydirprod
   Reading /var/zope2/var/LatexWiki/mydirprod.asy
   DirProd is now explicitly exposed in frame initial 
   DirProd will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mydirprod
   DirProdCat is now explicitly exposed in frame initial 
   DirProdCat will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/mydirprod

Try it:

axiom
x:= Integer;
Type: Domain
axiom
y:= NonNegativeInteger;
Type: Domain
axiom
DPx ==> DirProd(2, x);
Type: Void
axiom
DPx has DirProdCat(2, x)
LatexWiki Image(12)
Type: Boolean
axiom
DPx has DirProdCat(2, y)
LatexWiki Image(13)
Type: Boolean
axiom
DPx has DirProdCat(3, x)
LatexWiki Image(14)
Type: Boolean
axiom
DPx has DirProdCat(3, y)
LatexWiki Image(15)
Type: Boolean

The results show that the Aldor compiler treats a domain (R) and an element of a domain (n) differently in terms of information retained for the has operation. Had the Type in R: Type been replaced by Symbol and the lines defining x, y removed, all results would have been true. Notice here, contrary to Ralf's example, both the DirProdCat and DirProd constructors totally ignored the parameters. The two constructions DirProd(2,x) and DirProd(2,y) are really identical in implemetation. So the only information to distinguish DirProdCat(2,x) and DirProdCat(2,y) must have come from the declaration of the parameters (on the left of :).

axiom
)show DirProd(2,x)

 DirProd(2,Integer) is a domain constructor.
 Abbreviation for DirProd is DirProd
 This constructor is exposed in this frame.
 Issue )edit mydirprod.as to see algebra source code for DirProd 

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

 identity : % -> %                    


axiom
)show DirProd(2,y)

 DirProd(2,NonNegativeInteger) is a domain constructor.
 Abbreviation for DirProd is DirProd
 This constructor is exposed in this frame.
 Issue )edit mydirprod.as to see algebra source code for DirProd 

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

 identity : % -> %