[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structu
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures |
Date: |
Fri, 10 Mar 2006 00:39:47 +0100 |
User-agent: |
Thunderbird 1.5 (X11/20051201) |
On 03/09/2006 08:27 PM, William Sit wrote:
Martin:
Good work (I'm impressed :-).
Sorry, but I am not so much. I've already pointed out one problem in my
last mail and Bill saw another.
I think your solution is in fact the way
mathematicians build up algebraic structures: first define the underlying set
and the basic operations, then prove that the axioms of certain algebraic
structure are satisfied. Here you declare (rather than prove) these using
Aldor's 'extend' mechanism.
OK, that is why "extend" is so great. But look at
define MyMonoid(T: Type, m: (T, T) -> T): Category == with {
square: T-> T;
default {square(t: T): T == m(t, t)}
}
(Didn't I write that?)
If you define
extend DomA: MyMonoid(DomA, f) == add;
then f must already be an operation in the exports of DomA. Well, we can
do this.
define CatA: Category == with {
f: (%, %) -> %;
}
DomA: CatA == add {f(x: %, y: %): % == ...}
Now we can extend DomA by MyMonoid(DomA, f$DomA).
Then DomA has the exports
f: (%, %) -> %;
square: DomA -> DomA;
That is a bit funny, because the type of DomA involves DomA.
The beauty of your solution is that the notation (naming of the operations) is
defined in the domain itself and then the algebraic properties declared by
extension.
The slight disadvantage is that these structural operations must be listed with
each domain, and there is no default way (yet). So perhaps in MyMonoid, with
parameters, there can be a default syntax, such as:
MyMonoid(T:Type, default{*:(T,T)->T)}):Category
Well, did you forget "== with;" here?
MyDualMonoid(T:Type, default{*:(T,T)->T, o:(T,T)->T}):Category ==
with{MyMonoid(T); MyMonoid(T, o)};
That does not look bad, but it will not work as expected if you used
"Category". If you later declare something of type MyDualMonoid(..) it
will only export two more symbols that can be checked through "has",
namely "MyDualMonoid" and "MyMonoid". But see my last BINGO mail.
There must be another mechanism to achieve the desired behaviour. Via
categories that does not work.
MyAbelianMonoid(T:Type, default{+:(T,T)->T}):Category ==
with{commutative(+); MyMonoid(T, +), ...};
Oh, "commutative(+)" is not declared. Aldor does not allow such
attributes. "commutative(+)" must be a category. And since one cannot
specify + without giving it a type, one would have to write something
like "commutative(T, +)".
MyRing(T:Type, default{*:(T,T)->T, +:(T,T)->T}:Category ==
with{MyAbelianMonoid(T), MyMonoid(T), ...};
MyCommutativeRing(T:Type, default{*:(T,T)->T, +:(T,T)->T}:Category ==
with{MyAbelianMonoid(T), MyAbelianMonoid(T,*), ...};
(the above omits the units for the operations, which could be added easily) so
that
extend MyInteger: MyRing(MyInteger) == add;
would make sense.
Anyway, to me this all looks like specifying properties through tags.
We should, maybe rather write
MyMonoid(T:Type, default{*:(T,T)->T)}): Property == properties;
MyDualMonoid(T:Type, default{*:(T,T)->T, o:(T,T)->T}):Property ==
properties{MyMonoid(T); MyMonoid(T, o)};
where I have just replaced Category by Property and "with" by "properties".
But all this is unsatisfactory, since if Aldor should allow properties,
I would rather prefer to write some predicate logic formula than just
declaring names for the properties.
Maybe adding the ability to Aldor to express properties by logical
formulas that could also be used by proof checkers, that would be some
step forward.
Ralf
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, (continued)
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/03
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/04
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/07
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/07
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/08
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
- [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/09
- Re: [Axiom-developer] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
- Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
- Re: [Axiom-developer] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
- Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- RE: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Bill Page, 2006/03/09
- Re: [Axiom-developer] BINGO,Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
- Re: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/10
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/10
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/14