AXIOM documentation

Alan Hutchinson <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.user
Message-ID <[email protected]>
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) ...
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.