RE: [Axiom-developer] Curiosities with Axiom mathematical structures

[Bill Page]

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?) object-oriented languages.  I can
> understand the language limitation, but that is hardly an excuse for
> chosing in advance that "+" is for Abelian monoid and "*" for
> non-Abelian ones.
>

I don't see why renaming is necessary.
 
> | 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
       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

> | 
> | OK, that is not well thought of...
> | 
> | Anyway, there is not way to do this in Aldor, yet. At least 
> | nobody has told me so far.

It is possible to write the above definitions in Aldor.

> | 
> | If such renaming could be implemented into the Aldor language
> | that would make it even better suited for mathematics. However, 
> | then there is need that someone implements these ideas into the
> | compiler. Who?

Could you explain what you mean by "renaming" and how it might
be used to express mathematics?

> 
> I'm not sure renaming is a good solution, at least if I was going
> to solve this issue I would not go there. However, I do believe
> that expressing mathematical structures in a way that reflect
> mathematical properties and understanding is essential.

I agree.

> 
> 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))

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.)

> 
> 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. 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?

> 
> 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:

Adding the axioms to Axiom - Towards a system of automated reasoning
in Aldor

Abstract:
A number of combinations of theorem proving and computer algebra
systems have been proposed; in this paper we describe another
namely a way to incorporate a logic in the computer algebra system
Axiom. We examine the type system of Aldor - the Axiom Library
Compiler - and show that with some modifications we can use the
dependent types of the system to model a logic using the Curry-Howard
isomorphism. We give a number of example applications of the logic
we construct.

http://portal.axiom-developer.org/refs/articles/axiom-content.pdf/view

Logic and Dependent Types in the Aldor Computer Algebra System

Abstract:
We show how the Aldor type system can represent propositions of
first-order logic, by means of the `propositions as types'
correspondence. The representation relies on type casts (using
pretend) but can be viewed as a prototype implementation of a
modified type system with type evaluation reported elsewhere [9].
The logic is used to provide an axiomatisation of a number of
familiar Aldor categories as well as a type of vectors.

http://portal.axiom-developer.org/refs/articles/aldor-calc2000.pdf/view

Integrating Computer Algebra and Reasoning through the Type System of Aldor

Abstract:
A number of combinations of reasoning and computer algebra systems
have been proposed; in this paper we describe another, namely a way
to incorporate a logic in the computer algebra system Axiom. We examine
the type system of Aldor - the Axiom Library Compiler - and show that
with some modifications we can use the dependent types of the system
to model a logic, under the Curry-Howard isomorphism. We give a number
of example applications of the logic we construct and explain a prototype
implementation of a modified type-checking system written in Haskell. 

http://portal.axiom-developer.org/refs/articles/frocos2000.pdf/view

---------

Regards,
Bill Page.