"Bill Page" <[EMAIL PROTECTED]> writes:
> In Axiom (SPAD) we can write:
>
> Monoid(m:Symbol,u:Symbol): Category == with
> m: (%,%) -> % ++ returns the product of x and y
> u: () -> % ++ unit
> associative(m) ++ m(a,m(b,c)) = m(m(a,b),c)
> identity(u) ++ m(a,u) = m(u,a) = a
>
> Group(m:Symbol,inv:Symbol,u:Symbol): Category == Monoid(m,u) with
> inv: % -> % ++ inverse
> inverse(m,inv) ++ m(inv(a),a) = m(a,inv(a)) = u
>
> AbelianGroup(m:Symbol,inv:Symbol,u:Symbol): Category
> == Group(m,inv,u) with
> commutative(m) ++ m(a,b) = m(b,a)
>
> Ring(s:Symbol,inv:Symbol,z:Symbol, m:Symbol,u:Symbol): Category
> == Join(AbelianGroup(s,inv,z),Monoid(m,u)) with
> distributes(m,s) ++ m(a,s(b,c)) = s(m(a,b),m(a,c))
> ++ m(s(a,b),c) = s(m(a,c),m(b,c))
>
> Then we can write:
>
> )sh Ring(+,-,"0"::Symbol,*,"1"::Symbol)
> Ring(+,-,"0"::Symbol,*,"1"::Symbol) has commutative(+)
>
> See the example at http://wiki.axiom-developer.org/SandBoxMonoid
That's very interesting. I would have thought that it's not possible to use a
parameter as the name of an operation. Is this possible in Aldor, too? (I'd
guess so)
Ooops, I just tried to implement a domain:
)abbrev category MYMON MyMonoid
MyMonoid(m:Symbol): Category == with
m: (%,%) -> % ++ returns the product of x and y
square: % -> %
add
square a == m(a,a)
)abb domain WORDS Words
Words: Exports == Implementation where
Exports ==> MyMonoid("c"::Symbol) with
coerce: String -> %
Implementation == add
Rep := String
coerce(a: String): % == a
c(a:%, b:%):% == concat(a::Rep, b::Rep)
but square won't work then: Axiom is looking for an operation m, which does not
exist, of course.
How about Aldor?
Martin
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
