Technical background and overview

Simon Thompson, John Shackell and Erik Poll

Axiom and Aldor

Axiom is a computer algebra system; Aldor is the library compiler for Axiom. It will also form a part of the successor to Maple V, which is to be a new-generation PSE jointly supported by Waterloo Maple and the Numerical Algorithms Group.

The type system of Axiom/Aldor

Axiom/Aldor is unusual among computer algebra systems in being strongly typed: every item in the system has a type and the type-correctness of Axiom programs can be verified at compile time, an obvious benefit for the user of the system. To accommodate the various types encountered in CA systems, the type system needs to contain a number of powerful primitives; in order for the type system to be usable it is augmented with facilities for overloading, coercions and so forth which together interact to give a complexity to the system. Beyond this, various aspects of the system rely on a non-type-checked macro mechanism, and there are other complicating aspects which we survey briefly now.

Axiom/Aldor is intended to support symbolic mathematics, and so in particular to represent algebraic structures, such as monoids, groups and so forth. These appear as `categories' in Axiom/Aldor, where a category is specified by giving a signature of functions over a carrier set `%' as in the example
```
Monoid : Category == BasicType with {
 * : (%,%) -> %;
 1 : %; }
```
This states that for a structure over a type `%' to be a monoid it has to supply two bindings; in other words a Category describes a signature. The first name in the signature is `*' and is a binary operation over the type `%'; the second is an element of `%'. Implementations of a category are only accessible by means of the operations of the signature, and so are very much like abstract data types.
Axiom/Aldor contains dependent types, as exemplified by a function like
```
vectorSum : (n:Integer)->Vector(n)->Double
```
When vectorSum is applied, the type of its result depends upon the value of its argument, so that, for example, the application vectorSum(42) is a function expecting an argument of type Vector(42).
A final feature of the Axiom/Aldor is that types can be treated as values, so that the type Type is itself a type and so the system allows functions over types, such as the function which taking a type ty to a type of queues over ty, say, or a type of fields F to the category of vector spaces over F.

The type system of Axiom/Aldor is discussed in more detail in this paper.

Dependent types and logic

In the last fifteen years a number of theorem proving systems - including Lego, Coq and others - have been designed to exploit the Curry-Howard correspondence between logic and programming. Under this correspondence, logical propositions can be seen as types, and proofs can be seen as members of these types. Central to this correspondence are dependent types, which allow the representation of predicates and quantification. A summary of the correspondence follows.

Programming		Logic
Type		Formula
Program		Proof
Product/record	`(...,...)`	Conjunction
Sum/union	`...\/...`	Disjunction
Function type	`...->...`	Implication
Dependent function type	`(x:A)->B(x)`	Universal formula
Dependent product type	`(x:A,B(x))`	Existential formula
Empty type	`Exit`	Contradiction
One element type	`Triv`	True proposition

Predicates (that is dependent types) can be constructed in a number of different ways. In Axiom/Aldor the `less than' predicate over the natural numbers can be given an naive definition by primitive recursion.

lessThan(n:Nat,m:Nat) : Type ==
    if m=0 then       Exit
    else (if n=0 then Triv 
                 else lessThan(n-1,m-1));

We discuss other possible approaches below.

If we identify propositions with types, then the process of proof becomes one of defining the appropriate functions (or other values) which represent proofs, so that a proof of the transitivity of lessThan will be an expression of type

(n:Nat,m:Nat,k:Nat) -> lessThan(n,m) -> lessThan(m,k) -> lessThan(n,k)

Integrating a logic in Axiom/Aldor

We have shown that Axiom/Aldor has a complex type system with dependent types, and that dependent types have been used to represent logics in various theorem proving systems. We therefore propose to use the type system of Axiom/Aldor to represent a logic.

In order for this to operate successfully, we will need to make modifications to the implementation of dependent types in Axiom/Aldor, as we outline now. Consider the lessThan predicate defined (in Axiom/Aldor) earlier, and suppose that we form the expression lessThan(9,3), which represents the proposition `9<3'; we expect this to be manifestly false, and evaluating the expression will indeed lead to Exit, the type which is uninhabited, and which thus contains no proofs of `9<3'. Unfortunately, as Axiom/Aldor is currently implemented, there is no evaluation of Type expressions, and so any proposition formed in the same way as lessThan(9,3) will remain unevaluated. In order to integrate a logic we need to incorporate evaluation of type expressions into Axiom/Aldor.

Inductive types

A second approach to defining predicates introduces a predicate inductively as a generalisation of the algebraic types like list and trees which appear in modern functional languages like Haskell and SML.

We might define the less than predicate `<' of type Nat -> Nat -> Type by saying that there are two constructors - axioms, that is - for the type of the following signature

ZeroLess : (n:Nat) -> (O < S n)
SuccLess : (m:Nat) -> (n:Nat) -> ((m < n) -> (S m < S n))

This approach leads to a powerful style of proof which has been used extensively in the type theory community, see, for instance, Paulin's work.

Termination and consistency

It is possible to write in Axiom/Aldor expressions whose evaluation fails to terminate; if one of these appears as part of a Type expression then a type checker evaluating such expressions will not terminate. In type theory systems such as Lego, the definition mechanism is such that only terminating functions can be defined. There is also a body of work on defining terminating sub-languages of existing programming languages, an example being Turner's recent work on elementary strong functional programming.

The restriction to terminating (well-founded) recursions is also necessary for consistency of the logic. For the logic to be consistent, we need to require that not all types are inhabited, which is clearly related to the power of the recursion schemes allowed in Axiom/Aldor. One approach is to expect users to check this for themselves: we would expect this to be replaced by some automated or machine-assisted checking of termination, which ensures that partially- or totally-undefined proofs are not permitted.

Consistency also depends on the strength of the type system itself; a sufficiently powerful type system will be inconsistent as shown by Girard's paradox.

Applying the logic

Given an integrated logic as discussed above, we seek to apply the logic. We envisage applying the logic in various ways which we sketch here.

Pre- and Post-conditions

A more expressive type system allows programmers to give more accurate types to functions, expressing their logical pre- and post-conditions. An example is the function which indexes the elements of a vector, which can be defined to reflect the fact that it only gives a result when the index value is in range; its type is

(m:Nat) -> (n:Nat) -> (Vector(n) -> (m < n) -> Double)

The extra argument - a proof that m is less than n - becomes a proof obligation which must be discharged - or at least noted - when the function is applied to elements m and n.

We discuss examples of pre- and post-conditions from the case study of symbolic asymptotics in below.

Adding axioms to Axiom/Aldor categories

In introducing the types we gave the category of monoids, Monoid. Using `==' for the identity predicate we can add the appropriate logical properties to the signature in Monoid:

leftUnit  : (g:%) -> (1*g == g);
rightUnit : (g:%) -> (g*l == g);
assoc : (g:%,h:%,j:%) -> (g*(h*j) == (g*h)*j);

The Axiom/Aldor operations over categories, such as extension and join, will lift to become operations of extension and join over the extended `logical' categories like the example here.

Different degrees of rigour

One can interpret the obligations given above with differing degrees of rigour. Using the pretend function - which changes the type of a value - we can conjure up proofs of the logical requirements of Monoid; even in this case they appear as important documentation of requirements, and they are related to the lightweight formal methods work at St Andrews.

Alternatively we can build fully-fledged proofs as in the numerous implementations of constructive type theories mentioned above, or we can indeed adopt an intermediate position of proving properties seen as `crucial' while asserting the validity of others.

Last modified 16 April 1999.