axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Martin Rubey
Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures
Date: 04 Mar 2006 08:46:46 +0100
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.4

address@hidden (Page, Bill) writes:

> We are talking about categories here, so this does not have
> any effect on the Axiom interpreter. Every function that the
> interpreter calls in located in some package or domain and
> if necessary the function can be selected based on the package
> or domain name. 

This is not true. Don't forget about default functions, for example powering in
the case of monoids!

Martin

PS: The more I think of it, the better I find the proposed solution of passing
the appropriate functions to the category. For example, along the following
lines. Of course, this code does *not* work currently. Rather, it is a proposal
for a possible extension of Aldor.

-------------------------------------------------------------------------------
)abbrev category MYMON MyMonoid
MyMonoid(m: (%,%)->%): Category == with
       square: % -> %
     add
       square a == m(a,a)

)abb domain WORD Word
Word: Exports == Implementation where

  Exports == with

    coerce: String -> %
    c: (%, %) -> %
    MyMonoid(c) -- in case of several different operations "c", we would need
                -- to provide the full signature, of course.
    
  Implementation == add

    Rep := String
    coerce(a: String): % == a
    c(a, b) == concat(a::Rep, b::Rep)
-------------------------------------------------------------------------------

This "solution" has two advantages: 

* we don't need any new syntax
* it also deals with the problem of implementing axioms, for example,
  "commutative" would simply be a category - without any exports.

I wonder whether this would be difficult to implement.

Martin





reply via email to

[Prev in Thread] Current Thread [Next in Thread]