[Axiom-mail] AXIOM documentation

[Alan Hutchinson]

Dear Sirs
I have downloaded and installed the precompiled form of Axiom on Linux.
Thank you for it.

I am trying to understand the documentation.  Below are some notes
based on Chapter 5 of the book.  The system seems to be based on a
directed graph whose nodes are Axiom objects and whose edges are of
two sorts which could be called
member
  a is a member of b if b is a domain (or subdomain?) and a's type is b
refines
  c refines d if all members of c are members of d and in addition
                 all operations of c are operations of d.
Is this right?
Probably not quite, since c may have operations with the same names as
operations in d but different interpretations, in which case c would
not refine d.

In the book, Figure 1 shows a bit of this graph for the "refines"
relation and for some basic domains of algebra.  Could someone please
draw a similar graph with nodes including
  Type
  Category
  Domain
  Any
  SetCategory
  Symbol
  Variable ?
These are the obscurest objects.  Someone has tried to explain them
in bookvol1 Chapter 5, but it is hard.  See the notes below.

The next issue is how to extend this graph.  It seems easy to add a
new node X with "member" edges:
  if X is to be a domain of class C then use C's natural constructor:
    X := C(...)
  if X is any other type of object of some type T then declare
    X : T := ...
I have not yet worked out how to refine a domain.  There is a hint on
page 14 of the book: Complex(R) defines its exports with
  "Ring with ... if R has Field then Field ..."
The precompiled distribution doesn't seem to include source code for
built-in categories such as Complex, and I don't know how to get much
further.  I haven't yet found a full account of the syntax used to
declare a category such as Complex.  The word
  with
does not have an entry in the Glossary or in bookvol1's index.

Please forgive me if these matters have simple answers.  I haven't
read all the documentation, but I have looked at it for a day or so.
This looks like a really powerful package, but learning how to take
full advantage of it is not simple.
Best wishes
Alan Hutchinson

------------------

DOMAINS, CATEGORIES
===================
from "bookvol1" section 5.1

An object which is a class (with attributes?) of objects is called
a "domain" or "subdomain".

Each basic object is a member of a unique domain
called its "type". (p 169)
-- What does "basic" mean?
   Note: the polynomial (x+3) is a member of a domain. (p 169)
A "subdomain" S of a domain D is
the subclass (with all the attributes of D plus others?)
of objects in D satisfying a certain "membership predicate",
say p_S. (p 171)
-- This implies that most subdomains are not domains, since
   every member x of S is also a member of D but (if x is "basic"?)
   x is a member of just one unique domain.
-- Note: the terms "object" and "basic" are not in the index.

Each (sub)domain is an object.
There is a domain of all domains and subdomains.  It is called TYPE.

A type whose objects are domains is called a "category". (p 172)
-- surely, this should be
   A type each of whose objects is a domain or a subdomain
   is called a "category".

A function whose values are domains is called a "constructor".

Each (sub)domain has a name.  The name begins with a capital letter.
This name is also the name of a constructor function which constructs
(sub?)domains of the (sub)domain with this name.

The "has" operator is true of a domain D and a category C iff D is a 
member of C
.
-- might D be a subdomain? (p 173)

(13) -> Object has Type
 13) ->
   Object is not a valid type.
(13) -> SetCategory has Type
(13) ->
   (13)  true
                                                                Type: 
Boolean
(14) -> SetCategory has SetCategory
(14) ->
   (14)  true
                                                                Type: 
Boolean
(15) -> Type has SetCategory
(15) ->
   (15)  false
                                                                Type: 
Boolean
(16) -> )show SetCategory
 SetCategory  is a category constructor
 Abbreviation for SetCategory is SETCAT
 This constructor is exposed in this frame.
 Issue )edit /home/axiom/mnt/linux/../../src/algebra/SETCAT.spad to see 
algebra
source code for SETCAT

------------------------------- Operations --------------------------------
 ?=? : (%,%) -> Boolean                coerce : % -> OutputForm
 hash : % -> SingleInteger             latex : % -> String
 ?~=? : (%,%) -> Boolean

So it seems that SetCategory is a category of all domains whose members
can be printed and which can be tested for equality; and furthermore
all such domains can be printed and tested for equality.
Type is not such a domain.
Are there any others?

(16) -> File(SetCategory) has SetCategory
 16) ->
   File SetCategory is not a valid type.
(16) -> File(Type) has SetCategory
 16) ->
   File Type is not a valid type.
(16) -> File(Polynomial(Integer)) has SetCategory
   (16)  true
                                                                Type: 
Boolean
(17) -> )show File
 File S: SetCategory  is a domain constructor
 Abbreviation for File is FILE
 This constructor is exposed in this frame.
 Issue )edit /home/axiom/mnt/linux/../../src/algebra/FILE.spad to see 
algebra so
urce code for FILE

------------------------------- Operations --------------------------------
 ?=? : (%,%) -> Boolean                close! : % -> %
 coerce : % -> OutputForm              hash : % -> SingleInteger
 iomode : % -> String                  latex : % -> String
 name : % -> FileName                  open : (FileName,String) -> %
 open : FileName -> %                  read! : % -> S
 reopen! : (%,String) -> %             write! : (%,S) -> S
 ?~=? : (%,%) -> Boolean
 readIfCan! : % -> Union(S,"failed")

Correction:
files can be printed and tested for equality but File(S) is not a 
SetCategory.
Conjecture:
SetCategory is the category of domains whos objects all have
complete internal representations within Axiom.
Note:
if this is so then the predicate ?=? may fail.

The type of all categories is "Category" (p 174) but
(19) -> )show Category
      ...
              Category is not the name of a known type constructor.
(19) -> )show Type
 Type  is a category constructor
 Abbreviation for Type is TYPE
 ...
------------------------------- Operations --------------------------------
 ... (None) ...