[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
02 Mar 2006 20:23:54 +0100 
"Bill Page" <address@hidden> writes:
 On February 27, 2006 11:08 AM Gabriel Dos Reis wrote:

 >...
 >
 > Ralf Hemmecke <address@hidden> writes:
 > ...
 >  One reason for having Monoid and AbelianMoniod (one with "*" and
 >  the other with "+") is that neither SPAD nor Aldor allows to
 >  rename functions during inheritance.
 >
 > yes, that is true for many (all?) objectoriented languages. I can
 > understand the language limitation, but that is hardly an excuse for
 > chosing in advance that "+" is for Abelian monoid and "*" for
 > nonAbelian ones.
 >

 I don't see why renaming is necessary.
Me neither, but I guess it is a solution. But a solution that I
think brings greater confusion.
 >  Note that one would have to say something like
 > 
 >  define Monoid(
 >  *: (%, %) > %;
 >  1: %
 >  ): Category == ...
 > 
 >  define Group(
 >  *: (%, %) > %,
 >  inv: % > %,
 >  1: %
 >  ): Category == ...
 > 
 >  define Ring(.....): Category == with {
 >  Monoid(*, 1);
 >  Group(+, , 0);
 >  }
 >
 > Ring should be both Monoid and Group, whether they shoud be
 > categories, I don't really know.
 >

 In Axiom (SPAD) we can write:

 Monoid(m:Symbol,u:Symbol): Category == with
 m: (%,%) > % ++ returns the product of x and y
 u: () > % ++ unit
The reason I previously said I did not see why Monoid should be a
category is that the operation is already passed in as a parameter, so
there would nothing to implement "inside" in the Monoid.
However, upon discussion with a colleague, it appears that having to
pass in all the required properties (e.g. operation, neutral element,
etc.) will not be practical from software engineering point of view.
Indeed, there would be a redundancy in the system. The underlying type
and the operation suffice to uniquely define the structure. So that
means, the other parameters are somehow "function" of the essential
parameters. That implies that indeed Monoid will be a category which
domains will implement by supplying the value for the neutral element.
Same reasoning for Group where the type and the operation suffice to
define the inverse and the neutral element.
[...]
 > I believe this is something solvable  at least, that can be
 > approximated to a good extent  in a type system based on
 > predicate system directly available at the programming level.
 > We've been developing such an idea to build a type system for
 > C++ template arguments, see
 >
 > http://public.research.att.com/~bs/popl06.pdf
 >
 > presented at POPL this year.

 I think the predicates here are what Axiom calls "axioms" such as:

 associative(m) ++ m(a,m(b,c)) = m(m(a,b),c)
 identity(u) ++ m(a,u) = m(u,a) = a
 inverse(m,inv) ++ m(inv(a),a) = m(a,inv(a)) = u
 commutative(m) ++ m(a,b) = m(b,a)
 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))
The predicate as I use it was in the general sense; for example, in
the system Monoid is be predicate. That is consistent with the theory
of "qualified types", of which type classes (Haskell) are examplar.
But, I suspect that use of predicate also integrates yours.
 In Axiom right now the only thing we can do with axioms is to
 test them, e.g.

 R:=Ring(+,,"0"::Symbol,*,"1"::Symbol)
 ...
 if R has commutative(+) then

 but one could easily imagine adding more complex predicates
 which could still be evaluated at compile time. (Remember that
 Axiom and Aldor are intended to be statically typed languages.)
yes, I know Aldor is a statically typed language; in the predicate
system I'm talking about Rin would be a predicate  it says that a
combination of certain symbols are stated to conform to "Ring"
property. Again, this is "obvious" from the qualified theory point of
view.
 > Notice that the "post facto extenstion" of Aldor is a starting
 > point, but it still does not help solving that issue..

 As I understand it, post facto extension allows for the
 iterative definition of a type, i.e. adding and/or refining
 new functions.
Yes!
 I am not sure how this might apply in the
 example of the Ring above, but I think there are more
 interesting types that must be defined by mutual recursion
 and in that case post facto extension seems very natural.
 Could you give some examples of how else you think this can
 be used?
Suppose I started with a monoid M = Monoid(T, foo), then later prove
or discover that it really is Abelian. When ipso fact extension, I
could say
M has commutative(operation.M)
the point here is that I do not need to have all properties that M
might have handy before defining it. I can add those properties on the
go.
 > The make the approach practical for large libraries in
 > Axiom/Aldor I believe some form of deduction of category/domain
 > argument deduction would needed. However, Axiom/Aldor types
 > being dependent, that be challenging. Anyway, I have searched
 > the literature for the descirption of Axiom/Adlor type system
 > as implemented, I have found nothing that could assist me.
 >

 Have you looked at the papers by Erik Poll and Simon Thompson
 such as:
I had read two of the papers you pointed out (that was in 2004). But
none of them helped me find clarify the problem I was after.
I'll read the third one.
Thanks!
 Gaby
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, (continued)
 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
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/14
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/02
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures,
Gabriel Dos Reis <=
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/04
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13
 RE: [Axiomdeveloper] Curiosities with Axiom mathematical structures, Page, Bill, 2006/03/13