|
|
|
last edited 11 years ago by Bill Page |
| 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].
\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,*,1)
Ring(+,-,0,*,1) 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.
... --kratt6, Thu, 02 Mar 2006 08:46:49 -0600 replyUnfortunately, 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)
w1:=a(p)
w2:=b(p)
p(w1,w2)$Word(p)
p(w1,w1)$Word(p)
square(w1)$Word(p)
\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:
MyMonoid(m: (%,%)-> %)Word: MyMonoid(c) withMartin
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.
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, aa^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(xx)^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(String,concat,"") w2:=b(String,concat,"") w1w2 w1w1 w1^10 w11$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,[]) i1i2 i1i1 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) i1i2 i1i1 i1^0 i11$MyMonoid?(INT, +, 0) 1$MyMonoid?(INT, +, 0)i1 \end{axiom}
\begin{axiom} i1:=10.1::MyMonoid?(Float, , 1) i2:=20.2::MyMonoid?(Float, , 1) i1i2 i1i1 i1^4 i11$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, aa^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}
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 toMyRing. 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
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: \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, aa^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:=x3y3 w3:=x2+z3 \end{axiom}
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]?.
Error: export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/fricas/target/x86_64-linux-gnu/lib; LANG=en_US.UTF-8 /usr/local/lib/fricas/target/x86_64-linux-gnu/bin/fricas -nosman < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/6315008393781554935-25px.axm WARNING: redefining BOOT::|Monoid| in DEFUNdebugger invoked on a SIMPLE-CONDITION in thread #<THREAD "main thread" RUNNING {1001A08003}>: break
Checking for foreign routines FRICAS="/usr/local/lib/fricas/target/x86_64-linux-gnu" spad-lib="/usr/local/lib/fricas/target/x86_64-linux-gnu/lib/libspad.so" foreign routines found openServer result -2 FriCAS Computer Algebra System Version: FriCAS 1.3.12 built with sbcl 2.2.9.debian Timestamp: Sat 7 Jun 23:54:49 CEST 2025 ----------------------------------------------------------------------------- Issue )copyright to view copyright notices. Issue )summary for a summary of useful system commands. Issue )quit to leave FriCAS and return to shell. -----------------------------------------------------------------------------
(1) -> (1) -> (1) -> (1) -> (1) -> (1) -> <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/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5748985099523682154-25px001.spad using old system compiler. ------------------------------------------------------------------------ initializing NRLIB MONOID for Monoid compiling into NRLIB MONOID
;;; *** |Monoid| REDEFINED Time: 0 SEC.
Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.
restarts (invokable by number or by possibly-abbreviated name): 0: [CONTINUE] Return from BREAK. 1: [ABORT ] Exit from the current thread.
(|JoinInner| (#(NIL (((|t#1| #) T (ELT % 6)) ((|t#2| #) T (ELT % 6))) (((|associative| |t#1|) T) ((|identity| |t#2|) T)) (|Category|) (NIL NIL NIL) NIL))) error finding frame source: Bogus form-number: the source file has probably changed too much to cope with. source: NIL 0]
! You can't use `macro parameter character #' in horizontal mode.
l.210 #
include "axiom"
Missing $ inserted.
<inserted text>
$
l.225 ^
:(%,NonNegativeInteger) -> %; ++ a^0 = 1, a*a^n = a^(n+1)
(/usr/share/texlive/texmf-dist/tex/latex/jknapltx/ursfs.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
Extra }, or forgotten $.
l.228 }
== add {
Missing $ inserted.
<inserted text>
$
l.232 Missing } inserted.
<inserted text>
}
l.232
Overfull \hbox (98.90425pt too wide) in paragraph at lines 220--232
[]\T1/cmr/m/n/12 MyMonoid(S:SetCategory, m:(S,S)->S, u:S): with as-so-cia-tive
(S,m); iden-tity(S,m,u); *:(1: $[]\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 coerce \OT1
/cmr/m/n/12 : \OML/cmm/m/it/12 S\OMS/cmsy/m/n/12 ^^@ \OML/cmm/m/it/12 > coerce
\OT1/cmr/m/n/12 :== \OML/cmm/m/it/12 add[]$
Missing $ inserted.
<inserted text>
$
l.240 odd?(n::Integer) => return x(xx)^
shift(n,-1);
Extra }, or forgotten $.
l.242 }
;
Missing $ inserted.
<inserted text>
$
l.243
Overfull \hbox (32.35893pt too wide) in paragraph at lines 236--243
[]\T1/cmr/m/n/12 -- Re-peated squar-ing (x:import from In-te-ger,NonNegativeInt
eger; (n = 0) => re-turn 1; odd?(n::Integer) => re-turn x(xx)$[]\OML/cmm/m/it
/12 hift\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 n; \OMS/cmsy/m/n/12 ^^@\OT1/cmr/m/n/1
2 1); \OML/cmm/m/it/12 return\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x \OMS/cmsy/m/n/
12 ^^C
[6]
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 252.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 261.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 270.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 279.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 288.
You can't use `macro parameter character #' in horizontal mode.
l.290 #
include "axiom"
You can't use `macro parameter character #' in horizontal mode.
l.291 #
library MyMonoid "mymonoid.ao";
Overfull \hbox (24.54361pt too wide) in paragraph at lines 294--297
[]\T1/cmr/m/n/12 define in-verse(S:SetCategory, m:(S,S)->S, inv:S->S, u:S): Cat
-e-gory == with de-fault ForAll(a:S):Boolean == m(inv(a),a)=u and m(a,inv(a))=
u;
Missing $ inserted.
<inserted text>
$
l.305 ^
:(%,NonNegativeInteger) -> %; ++ a^0 = 1, a*a^n = a^(n+1)
Extra }, or forgotten $.
l.308 }
== MyMonoid(S,m,u) add {
Missing $ inserted.
<inserted text>
$
l.312
Missing } inserted.
<inserted text>
}
l.312
[7] [8]
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 320.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 325.
You can't use `macro parameter character #' in horizontal mode.
l.327 #
include "axiom"
You can't use `macro parameter character #' in horizontal mode.
l.328 #
library MyMonoid "mymonoid.ao";
You can't use `macro parameter character #' in horizontal mode.
l.330 #
library MyGroup "mygroup.ao";
Missing $ inserted.
<inserted text>
$
l.343 ^
:(%,NonNegativeInteger) -> %; ++ a^0 = 1, a*a^n = a^(n+1)
Extra }, or forgotten $.
l.346 }
== add {
Missing $ inserted.
<inserted text>
$
l.350
Missing } inserted.
<inserted text>
}
l.350
Missing $ inserted.
<inserted text>
$
l.358 odd?(n::Integer) => return x+(x+x)^
shift(n,-1);
Extra }, or forgotten $.
l.360 }
;
Missing $ inserted.
<inserted text>
$
l.361
Overfull \hbox (42.02386pt too wide) in paragraph at lines 354--361
[]\T1/cmr/m/n/12 -- Re-peated squar-ing (x:import from In-te-ger,NonNegativeInt
eger; (n = 0) => re-turn 0; odd?