axiom-developer
[Top][All Lists]
Advanced

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

[Axiom-developer] [Axiom Language]


From: Bill Page
Subject: [Axiom-developer] [Axiom Language]
Date: Wed, 28 Sep 2005 20:56:55 -0500

Changes http://wiki.axiom-developer.org/AxiomLanguage/diff
--

??changed:
-Axiom has both an "interpreter":AxiomInterpreter and a built-in
-"compiler":ProgrammingAxiom.
Axiom has both an interactive language or
"interpreter":AxiomInterpreter for user interactions and
a programming language "compiler":ProgrammingAxiom
for building library modules.

++added:

  Like Modula 2, PASCAL, FORTRAN, and Ada, the programming
language emphasizes strict type-checking. Unlike these
languages, types in Axiom are dynamic objects: they are
created at run-time in response to user commands.

  The Axiom interactive language is oriented towards
ease-of-use. The Axiom interpreter uses type-inferencing
to deduce the type of an object from user input. Type
declarations can generally be omitted for common types
in the interactive language.

  The Axiom compiler language (version 1 of the language
is called SPAD, version 2 of the language is called [Aldor])
on the other hand is based on strong static types that must
be explicitly specified by the programmer.

Type Inference in the Interpreter

??changed:
-Axiom is very strict with types (meaning: where the operation
-takes place). The division of 1+2 by 3 takes place in
-Fraction Integer (field of rational numbers) and that is
-where the answer should be, even if it is 1. Most people
-would automatically "retract" this to the integer 1. But in
-general, there is no natural way to do so (why not retract
-1 to a natural number, for example?).  So Axiom provides the
-user a way to "coerce" an answer to another type. You can coerce
-1 to any of many, many types, for example, as a polynomial,
-or even as a matrix (or the unit element of any ring).
Axiom is very strict with types (meaning: that it must be
completely unambiguous where each operation takes place).
The division of 1+2 by 3 takes place in Fraction Integer
(field of rational numbers) and that is where the answer will
be, even if it is 1. Most people would automatically "retract"
this to the integer 1. But in general, there is no natural
way to do so (why not retract 1 to a natural number, for
example?).  So Axiom provides the user a way to "coerce" an
answer to another type. You can coerce 1 to any of many,
many types, for example, as a polynomial, or even as a
matrix (or the unit element of any ring).

++added:
Types of Objects, Domains, and Categories

  In Axiom the concept of "Type" is universally applied at
all levels.

  From the Axiom Book: Appendix B Glossary

  - The type of any category is the unique symbol Category.

  - The type of a domain is any category to which the domain
    belongs.

  - The type of any other object is either the (unique) domain
    to which the object belongs or a subdomain of that domain.

  - The type of objects is in general not unique.

  From the Axiom Book: Technical Introduction

    Every Axiom object is an instance of some domain. That
domain is also called the type of the object. Thus the
typeOf -1 is inferred by the interpret to be Integer and
the typeOf the variable x:Integer is declared to be Integer.
Similarly the typeOf "daniel" is String. The type of an
object, however, is not unique. The type of integer 7 is
not only Integer but also NonNegativeInteger, PositiveInteger,
and possibly, in general, any other *subdomain* of the
domain Integer.

Domains are defined by Axiom by programs of the form::

  Name(Parameters): JoinCategorys
    with Exports == Extends
      add Rep == RepDomain
        Implementation 

The Name of each domain is used to refer to the collection
of its instances. For example, Integer denotes "the integers",
Float denotes "the floating point numbers" etc. For example::

  Fraction(S: IntegralDomain): QuotientFieldCategory S with
       if S has canonical and S has GcdDomain
         and S has canonicalUnitNormal
           then canonical
    == LocalAlgebra(S, S, S) add
      Rep:= Record(num:S, den:S)
      coerce(d:S):% == [d,1]
      zero?(x:%) == zero? x.num

Thus the type of Fraction Integer is 'QuotientFieldCategory
Integer with canonical'. The axiom 'canonical' means that
equal elements of the domain are in fact identical.

We also say that the domain Fraction(s) *extends* the domain
LocalAlgebera(S,S,S). Domains can extend each other in a
circular mutually recursive manner so in general the extends
relationship fors a directed graph with cycles.

Fractions are represented as the domain Record(num:S, den:S).

In Axiom domains and subdomains are themselves objects that
have types. The type of a domain or subdomain is called a
category. Categories are described by programs of the form::

   Name(...): Category == JoinCategorys
     with Exports
      add Imports
        Implementation 

The type of every category is the distinguished symbol
Category. The category Name is used to denote the collection
of domains of that type. For example, category Ring denotes
the class of all rings.

For example::

  QuotientFieldCategory(S: IntegralDomain): Category ==
    Join(Field, Algebra S, RetractableTo S, FullyEvalableOver S,
         DifferentialExtension S, FullyLinearlyExplicitRingOver S,
           Patternable S, FullyPatternMatchable S) with
      _/     : (S, S) -> %
         ++ d1 / d2 returns the fraction d1 divided by d2.
      numer  : % -> S
         ++ numer(x) returns the numerator of the fraction x.
      denom  : % -> S
      ...
      if S has PolynomialFactorizationExplicit then
        PolynomialFactorizationExplicit
   add
      import MatrixCommonDenominator(S, %)
      numerator(x) == numer(x)::%
      denominator(x) == denom(x) ::%
      ...

Categories say nothing about representation. Domains, which
are instances of category types, specify representations.

Categories form hierarchies (technically, directed-acyclic
graphs). A simplified hierarchical world of algebraic
categories is shown below. At the top of this world is
SetCategory, the class of algebraic sets. The notions of
parents, ancestors, and descendants is clear. Thus ordered
sets (domains of category OrderedSet) and rings are also
algebraic sets. Likewise, fields and integral domains are
rings and algebraic sets. However fields and integral
domains are not ordered sets::

  SetCategory +---- Ring ---- IntegralDomain ---- Field
              |
              +----  Finite    ---+
              |                    \
              +---- OrderedSet -----+ OrderedFinite

  Figure 1. A simplified category hierarchy.



--
forwarded from http://wiki.axiom-developer.org/address@hidden




reply via email to

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