[Top][All Lists]

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

RE: [Axiom-developer] Axiom domains and Aldor return types

From: Bill Page
Subject: RE: [Axiom-developer] Axiom domains and Aldor return types
Date: Sun, 16 Jan 2005 02:39:04 -0500

On Friday, January 14, 2005 4:04 PM William Sit wrote:
> ... 
> I think something like F(a:A)==F(a):B(a) should simply be 
> called a program or routine! It is neither a function nor
> a functor in the strict mathematical sense.

I agree.

> > Is there a way that this "Aldor function" can be written
> > in Aldor that syntactically respects the same distinction?
> > If so, then perhaps we should just consider the way Aldor
> > allows this to be written as a kind of abbreviation that
> > happens to look like the notation for a function.
> I think Aldor treats the two levels equally, that is, domain 
> constructors and "function" are the treated the same. Axiom
> does not and  restricts "function" to a real mathematical
> function while leaving domain (or even category and package)
> constructors a bit more general by allowing dependent signatures.

I have argued that this is a good thing because allowing dependent
"signatures" is really better represented mathematically as a
functor, i.e. something that provides new objects as well as
operations (functions) on these objects. I think it is correct
to think of an Axiom domain constructor as a functor (of a specific
kind) in the sense of category theory. I continue this view in
response to another comment below.

> This allowed dependence is even more general than F(a:A)==F(a):B(a),
> for example, one can have F(a:A,b:B(a),c:C(a,b))==F(a,b,c):D(a,b,c).
> Such dependence is not allowed for functions in Axiom but allowed
> in Aldor. In other words, the source does not have to be "rectangular"
> but can be any "area" (or "solid") with bounding "curves" ("surfaces").
> Metaphorically, Aldor allows integration over any solid, Axiom only
> over a cuboid. If you think about this calculus analogy, you can see
> that Aldor is a much more powerful language.

>From a category theory perspective this is like allow "partial
functions", i.e. functions defined only over a subset of its domain.
This is possible but it turns out not to be a "more powerful
language". Sometimes a language can be more powerful because of
it's restrictions rather than it's apparent flexibility. Generality
can compromise expressiveness. So in the category SET (actually
a specific type of category called a topos) the morphisms (functions)
are taken to be total. But that is a very long story and maybe
you already know it or we can talk more about it later.

> > BTW, chapters 11 Packages, 12 Categories and 13 Domains of the
> > Axiom book are very useful but I find the orientation rather
> > confusing - perhaps it is just the "age" of the terminology
> > that is used in these chapters that makes reading a little hard.
> > I think it would be great if these could be re-written in a
> > more modern "categorical" manner similar to the way you wrote
> > your previous message. Are there any papers that you could
> > reference that attempt to do this? Is there some corresponding
> > part of the Aldor documentation that would be useful for me
> > to re-read?
> Well, I tried to look up something from the web for my email 
> on functors, and I got a nice one for you:

Well, this article by Baez seems to be just about category theory.

What I was looking for was some documentation about the specific
use of the word "functor" in the context of Aldor (and possibily
Axiom). I am aware that this usage differs (to greater or lesser
extent) from the normal usage in category theory per se.

> Actually, I was attempting to explain why something like Integer
> is a category and I remembered that category theorist think of a
> group as a category but forgot how. The above article explains
> that. But applying the same to Axiom does not work! Try it.

I am not sure exactly what you mean by it "does not work".

I agree however that what Axiom calls a "category" is not quite
the same thing as what category theory calls a category. This
is an unfortunate confusion of terminology of course given that
Axiom is specifically intended to be a tool to implement in computer
form much of the mathematics that is now routinely formalized using
the methods of category theory. One reason of course is that the
development of Axiom occurred more or less in parallel with modern
category theory so there are many ideas in common but also
many differences as ideas once implement by computer become
somewhat more permanent than ideas freely expressed by creative

There are other newer programming languages, such as Haskel and
Ocaml which specifically take an approach which is more in line
with modern category theory than is Axiom. My impression was
that Aldor also may have attempted to move in this direction.
That is why I was asking about the use of the word functor in

Some previous discussion of these issues on the axiom-developer
email list:

> From:         Bill Page
> Subject:      RE: [Axiom-developer] categorical design
> Date:         Thu, 9 Oct 2003 22:54:30 -0400
> BTW, if I haven't already mentioned it here (or even if
> I have ... <grin> ) I would like to recommend a good and
> easily available book on category theory and type systems.
> See the book
>   Categories Types and Structures
>   by Asperti and Longo
>   MIT Press, 1991
> Now available for download at:
> Cheers,
> Bill Page.

And about Axiom and category theory elsewhere

The Axiom computer algebra system applied to computational category theory
Ronald Brown
(joint work with W. Dreckmann(Bangor and Stockholm))

Date: July 18th (Thursday)
Time: 16:25-16:45
The Axiom language is based on what are called: (Axiom) categories,
domains, packages, objects. An `Axiom category' consists essentially
of a signature. The representation of objects, implementation of
operations, and expression as output form, is carried out in the
domain constructors. The advantages of the Axiom language and system
are discussed, and illustrated in terms of the code for directed graphs,
free categories, and the category of finite sets. It is argued that
this type of system allows for the development of code for the
interaction of examples and abstract algebraic systems, and code which
is relatively easily modified, and sufficiently general to cope with
new examples. That is, the code approximates more than is usual to
the standard ways of writing mathematics.


And a relatively new paper by Saul Youssef specifically about Aldor
and category theory:

Prospects for Category Theory in Aldor
Saul Youssef
Center for Computational Science
Boston University
October 16, 2004
Ways of encorporating category theory constructions and results
into the Aldor language are discussed. The main features of Aldor
which make this possible are identied, examples of categorical
construtions are provided and a suggestion is made for a foundation
for rigorous results.


Bill Page.

reply via email to

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