[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Ralf Hemmecke 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
Tue, 14 Mar 2006 15:55:48 +0100 
Useragent: 
Thunderbird 1.5 (X11/20051201) 
On 03/14/2006 01:37 AM, Gabriel Dos Reis wrote:
Ralf Hemmecke <address@hidden> writes:
 Integer is a name for a structure with carrier set

 {0, 1, 1, 2, 2, ...}

 and operations {+, *, 0, 1, ...}.

 Integer is certainly not the carrier set alone.
Well, actually, it is a convention what Integer should stand for.
For some people it might just be enough to consider Integer as an
abbreviation for the multiplicative structure ({0,1,1,...}, (*, 1)}
for other people (ie in other contexts) it might be the ring structure.
And very common in algebra, the carrier set is often denoted by the same
symbol as the whole algebraic structure. (I guess the latter it too
ambiguous to be mapped to a programming language?)
Indeed. It is a type, e.g. set equipped with minimal operations that
let us implement abstractions on top of it. Just an abstract data
type can be implemented in terms of another one, an algebraic
structure cane be constructed in terms of another one.
 How would you mathematically express that the integers belong to the
 category of monoids? You would probably say that

 F(Integer) is an object in the category of monoids
I would do it by assertion.
What does that mean?
But I will refrain from needlessly emphasizing on the the carrier set
>  as F(Integer).
Oh, I hope you understood that F was meant to be a (forgetful) functor
in the categorial sense whose result would be an object in the category
of monoids.
So, if you like you could say
define MyMonoid: Category == with {*:(%,%)>%;1:%}
 axioms still missing :(
MonoidStructure(T: Type)(binop:(T,T)>T, unit:T): Monoid == T add {
Rep == T; import from T;
(x: %) * (y: %): % == per(binop(rep x, rep y);
1: % == per unit;
}
That IS Aldor syntax and it would compile. So in Aldor term F from above
would be something like
F = G(binop, unit)
for that to work it should be possible to write G as
MonoidStructure(binop:(T,T)>T, unit:T): (T: Type) > Monoid ...
where the operations would have to be specified before the type is
given. I don't think that is possible in a programming language.
HOWEVER, the above code would ALWAYS return something of type Monoid,
since it is a type constructor in Aldor and not a forgetful functor in
the mathematical sense. For me the question would be, how could one
write forgetful functors in Aldor?
Oh, it just came to my mind, we can have forgetful functors.
Let's take Integer. According to what it has been extended it has a
definite type (some Aldor category). Basically, if one says
MyInteger: with {+: (%, %)>%; 0: %;} == Integer add;
then MyInteger is like Integer (same carrier set) but everything
forgotten except + and 0.
Well, then now it remains the question how one could match the names
+, 0 with *,1 in Monoid when asking "MyInteger has Monoid".
But there are 2 problems here.
1) How to match + and the binary operation from Monoid?
2) My specification above probably forgets to much. After all it also
forgets the properties of + and 0. So it could never be a monoid.
Unfortunately, Axiom/Aldor does not allow axioms (and I would like to
see arbitrary predicate logic formulas not just declarative syntax).
Ralf
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, (continued)
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/14
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/14
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/08
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/08
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/08
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/09
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13