Articles

No albums or photos uploaded yet.

Etude du typage dans le sytème de calcul scientifique Aldor (Study of types in the Aldor scientific computation system) — by Bill Page — last modified Nov 18, 2005 07:29 PM

Apparu vers le milieu des années 70, le langage de calcul formel Axiom [13], initialement Scratchpad, faisait montre de caractéristiques peu communes dans l'univers des langages de calcul formel, comparativement aux langages contemporains ou ultérieurs tels Reduce, Macsyma, Mathematica, Maple, Magma, Mupad. Aldor est le successeur direct du langage Axiom. Comme tous les langages de calcul formel, il autorise la manipulation des objets de base du calcul mathématique : entiers, flottants, booléens, chaînes de caractères, etc, en programmation impérative ou fonctionnelle. ( Appearing towards the middle of the seventies, the Axiom language of formal calculation [13], initially Scratchpad, displayed not very common characteristics in the world of languages of formal calculation, compared with the contemporary or subsequent languages such as Reduce, Macsyma, Mathematica, Maple, Magma, Mupad. Aldor is the direct successor of language Axiom. As all the languages of formal calculation, it allows the handling of basic objects of mathematical counting: integer, floating point, boolean, character strings, etc, in imperative or functional programming. )

Applying AXIOM to Partial Differential Equations — by Bill Page — last modified Nov 18, 2005 07:29 PM

We present an AXIOM environment called JET for geometric computations with partial differential equations within the framework of the jet bundle formalism. This comprises especially the completion of a given differential equation to an involutive one according to the Cartan-Kuranishi Theorem and the setting up of the determining system for the generators of classical and non-classical Lie symmetries. Details of the implementation are described and examples of applications are given. An appendix contains tables of all exported functions.

On the way to certify Computer Algebra Systems — by Bill Page — last modified Sep 19, 2005 02:50 PM

ABSTRACT (max 200 words): "The Foc project aims at supporting, within a coherent software system, the entire process of mathematical computation, starting with proved theories, ending with certified implementations of algorithms. In this paper, we explain our design requirements for the implementation, using polynomials as a running example. Indeed, proving correctness of implementations depends heavily on the way this design allows due mathematical properties to be truly handled at the programming level. " DATE: 1997 AUTHORS:S. Boulmé, T. Hardin, D. Hirschko V. Ménissier-Morain, and R. Rioboo Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie (Paris 6), 8, rue du Capitaine Scott, 75015 Paris, France. EMAIL: "Therese.Hardin@lip6.fr"

A New Algebra System — by Bill Page — last modified Aug 29, 2007 06:28 AM

The thesis of this note is that, in order to achieve uniform semantics between compiled and interpreted code, and to avoid exposing all sorts of internal hacks to the user, we require a model for the semantics of the new algebra system. Among the requirements of this model are that it be: 1. Simple 2. Powerful 3. Related to a user's perception of the system. It is not necessary that it be efficient. I propose, as I believe others have done, the Alist model for computer algebra systems, in which a domain is conceived of as a set of values (about which little more will be said), a set of attributes (I do not fully understand these, but believe that they will follow much the same lines as operations) and a set of operations. The set of operations lists all the operations that can be performed on elements of the domain, and the user is invited to view the system as searching this list for an operation of the appropriate signature, and then applying it.

Approaching Inheritance from a “Natural” Mathematical Perspective and from a Java Driven Viewpoint — by Bill Page — last modified Jun 21, 2005 05:44 PM

Approaching Inheritance from a “Natural” Mathematical Perspective and from a Java Driven Viewpoint: a Comparative Review. Marc Conrad/1, Tim French/1, Carsten Maple/1, and Sandra Pott/2 1/ University of Luton, LU1 3JU, UK marc.conrad@luton.ac.uk, tim.french@luton.ac.uk, carsten.maple@luton.ac.uk 2/ University of York, YO10 5DD, UK sp23@york.ac.uk Abstract. It is well-known that few object-oriented programming languages allow objects to change their nature at run-time. There have been a number of reasons presented for this, but it appears that their is a real need for matters to change. In this paper we discuss the need for object-oriented programming languages to reflect the dynamic nature of problems, particularly those arising in a mathematical context. It is from this context that we present a framework that realistically represents the dynamic and evolving characteristic of problems and algorithms.

Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire — by Bill Page — last modified May 24, 2007 04:08 PM

Abstract We develop a calculus for lazy functional programming based on recursion operators associated with data type deffinitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's "Introduction to Functional Programming" can be expressed using these operators.

Polynomial GCD Using Straight Line Program Representation — by Bill Page — last modified Sep 07, 2006 06:27 AM

Bill Naylor (PhD Thesis University of Bath, 2000): Summary: This thesis is concerned with calculating polynomial greatest common divisors using straight line program representation. In the Introduction chapter, we introduce the problem and describe some of the traditional representations for polynomials, we then talk about some of the general subjects central to the thesis, terminating with a synopsis of the category theory which is central to the AXIOM computer algebra system used during this research. The second chapter is devoted to describing category theory. We follow with a chapter detailing the important sections of computer code written in order to investigate the straight line program subject. The following chapter on evaluation strategies and algorithms which are dependant on these follows, the major algorithm which is dependant on evaluation and which is central to our thesis being that of equality checking. This is indeed central to many mathematical problems. Interpolation, that is the determination of coefficients of a polynomial is the subject of the next chapter. This is very important for many straight line program algorithms, as their non-canonical sttructure implies that it is relatively difficult to determine coefficients, these being the basic objects that many algorithms work on. We talk about three separate interpolation techniques and compar their advantages and disadvantages. The final two chapters describe some of the results we have obtained from this research an finally conclusions we have drawn as to the viability of the straight line program approach and possible extensions. Finally we terminate with a number of appendices discussing side subjects encountered during the thesis. Download 07-Sep-2006: http://www.cs.bath.ac.uk/~wn/thesis.ps.gz

Does Axiom Solve Systems of O.D.E.'s Like Mathematica? — by Bill Page — last modified Feb 10, 2005 08:18 PM

If I were demonstrating Axiom and were asked this question my reply would be "No, but I am not sure that this is a bad thing", and I would illustrate this with the following example.

The "Unknown" in Computer Algebra — by Bill Page — last modified Sep 19, 2006 07:14 AM

Computer algebra systems have to deal with the confusion between "programming variables" and "mathematical symbols". We claim that they should also deal with "unknowns", i.e. elements whose values are unknown, but whose type is known. For example $x^p \ne x$ if $x$ is a symbol but $x^p=x$ if $x\in \mathrm{GF}(p)$. We show how we have extended Axiom do deal with this concept. Download 18-Sep-2006: http://lists.nongnu.org/archive/html/axiom-developer/2004-06/dviwYbMdboRdU.dvi PDF format: http://wiki.axiom-developer.org/public/TheUnknownInComputerAlgebra.pdf

Utilisation de logiciels libres pour la réalization do TP MT26 — by Bill Page — last modified Nov 18, 2005 07:29 PM

 

Book Review - Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena by Jon Barwise and Lawrence Moss — by Bill Page — last modified Jun 23, 2005 04:48 PM

From http://cogprints.org/336/ "To a greater or lesser degree, every scientific advance marks some departure from the common sense that preceded it." These words of Irving M. Copi (Copi, 1979, p.195) apparently summarize the nature of Vicious Circles in the most concise fashion. Following the steps of Aczel's ground-breaking monograph (Aczel, 1988) which marked a departure from the `common sense' that is attributed to classical set theory, this new book (abbreviated as VC in the sequel) of Jon Barwise and Larry Moss not only offers an introduction to the revolutionary and fascinating topic of non-wellfounded sets (a.k.a. hypersets) but also becomes the most authoritative source for any serious researcher (mathematician, philosopher, or computer scientist alike) who wants to understand and further pursue this timely topic." And in a footnote the reviewer write: "It is hard to tell why circularity has always been regarded with doubt in mathematical circles. One reason may be that circular arguments or structures are thought to be diffcult to grasp, most probably due to our educational make-up in linear thinking. On a more personal note: I tend to think that popular works such as Escher's drawings may have helped to create the illusion that circularity invites nonsense."

Logic and Dependent Types in the Aldor Computer Algebra System — by Bill Page — last modified Nov 18, 2005 07:29 PM

We show how the Aldor type system can represent propositions of first-order logic, by means of the `propositions as types' correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an axiomatisation of a number of familiar Aldor categories as well as a type of vectors.

Possible Enhancements for Aldordoc — by Bill Page — last modified Jul 21, 2006 02:11 AM

Authors: Balint Joo, Tony Kennedy. Aldordoc is an application, that extracts documentation from Aldor programs -- in particular .asy files. It produces XML output which can then be converted to various display formats, oun of the current supported being HTML. The appearance of the HTML output however is quite basic, and it is to be embedded into Aldor documentation comments. This document investigates some of these issues. Download 21-Jul-2006: http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/discussion/aldordoc.pdf

Next Generation Computer Algebra Systems — by Bill Page — last modified Nov 18, 2005 07:29 PM

AXIOM and the Scratchpad Concept: Applications to Research in Algebra Larry Lambe Presented to the 21st Nordic Congress of Mathematicians, June, 1992, Lulea, Sweden

Pseudo Differential Operators and Integrable Systems in AXIOM — by Bill Page — last modified Nov 18, 2005 07:29 PM

An implementation of the algebra of pseudo differential operators in the computer algebra system AXIOM is described. In several examples the application of the package to typical computations in the theory of integrable systems is demonstrated.

A First Report on the A# Compiler — by Bill Page — last modified Nov 18, 2005 07:29 PM

Stephen M. Watt Peter A. Broadbery Samuel S. Dooley Pietro Iglio Scott ~C. Morrison* Jonathan M. Steinbach Robert S. Sutor IBM Thomas J. Watson Research Center P.O. BIDX 218, Yorktown Heights, NY 10598 USA

Adding the axioms to Axiom - Towards a system of automated reasoning in Aldor — by Bill Page — last modified Nov 18, 2005 07:29 PM

A number of combinations of theorem proving and computer algebra systems have been proposed; in this paper we describe another namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor - the Axiom Library Compiler - and show that with some modifications we can use the dependent types of the system to model a logic using the Curry-Howard isomorphism. We give a number of example applications of the logic we construct.

Object-Oriented Mathematical Programming and Symbolic/Numeric Interface — by Bill Page — last modified Nov 18, 2005 07:29 PM

The Axiom language is based on the notions of packages, domains and categories.

Real Algebraic Closure of an Ordered Field, Implementation in Axiom — by Bill Page — last modified Nov 18, 2005 07:29 PM

Real algebraic numbers appear in many Computer Algebra problems. For instance the determination of a cylindrical algebraic decomposition for an euclidian space requires computing with real algebraic numbers. This paper describes an implementation for computations with the real roots of a polynomial. This process is designed to be recursively used, so the resulting domain of computation is the set of all real algebraic numbers. An implementation for the real algebraic closure has been done in Axiom (previously called Scratchpad).

SCRATCHPAD 1 AN INTERACTIVE FACILITY FOR SYMBOLIC MATHEMATICS — by Bill Page — last modified Nov 18, 2005 07:29 PM

The SCRATCHPAD/1 system is designed to provide an interactive symbolic computational facility for the mathematician user. The system features a user language designed to capture the style and succinctness of mathematical notation, together with a facility for conveniently introducing new notations into the language. A comprehensive system library incorporates symbolic capabilities provided by such systems as SIN, MATHLAB, and REDUCE.

JET - An AXIOM Environment for Geometric Computations with Differential Equations — by Bill Page — last modified Nov 18, 2005 07:29 PM

Geometric methods play an important role in the analysis of nonlinear differential equations. For example, symmetry methods provide the more or less only systematic approach to the construction of solutions. However, most geometric computations tend to be very tedious. Thus the use of computer algebra systems considerably helps in the application of these methods. JET is an environment within the computer algebra system AXIOM to perform such computations. The current implementation emphasizes the two key concepts involution and symmetry. It provides some packages for the completion of a given system of differential equations to an equivalent involutive one based on the Cartan- Kuranishi theorem and for setting up the determining equations for classical and non-classical point symmetries.

Object Oriented Method for Axiom. — by Bill Page — last modified Nov 18, 2005 07:29 PM

Axiom is a very powerful computer algebra system which combines two languages paradigms (functional and OOP). Mathematical world is complex and mathematician use abstraction to design it. This paper presents some aspects of the object oriented development in Axiom. The axiom programming is based on several new tools for object oriented development, it uses two levels of class and some operations such that coerce, retract or convert which permit the type evolution. These notions introduce the concept of multi-view.

Modeling Inheritance as Coercion in a Symbolic Computation System — by Bill Page — last modified Mar 03, 2006 08:01 AM

In this paper the analysis of the data structures used in a symbolic computation system, called Kenzo, is undertaken. We deal with the specification of the inheritance relationship since Kenzo is an object-oriented system, written in CLOS, the Common Lisp Object System. We focus on a particular case, namely the relationship between simplicial sets and chain complexes, showing how the order-sorted algebraic specifications formalisms can be adapted, through the "inheritance as coercion" metaphor, in order to model this Kenzo fragment.

Algorithms for Type Inference with Coercions — by Bill Page — last modified Mar 03, 2006 08:05 AM

This paper presents algorithms that perform a type inference for a type system occurring in thecontext of computer algebra. The type system permits various classes of coercions between types and the algorithms are complete for the precisely defined system, which can be seen as a formal description of an important subset of the type system supported by the computer algebra program AXIOM. Previously only algorithms for much more restricted cases of coercions have been described or the frameworks used have been so general that the corresponding type inference problems were known to be undecidable.

The Type Inference and Coercion Facilities in the Scratchpad II Interpreter — by Bill Page — last modified Aug 29, 2007 08:16 PM

The Scratchpad II system is an abstract datatype programming language, a compiler for the language, a library of packages of polymorphic functions and parametrized abstract datatypes, and an interpreter that provides sophisticated type inference and coercion facilities. Although originally designed for the implementation of symbolic mathematical algorithms, Scratchpad II is a general purpose programming language . This paper discusses aspects of the implementation of the interpreter and how it attempts to provide a user friendly and relatively weakly typed front end for the strongly typed programming language.

Lightweight Formal Methods For Computer Algebra Systems — by Bill Page — last modified Mar 03, 2006 07:52 AM

In this paper we demonstrate the use of formal methods tools to provide a semantics for the type hierarchy of the AXIOM computer algebra system, and a methodology for Aldor program analysis and verification. We give examples of abstract specifications of AXIOM primitives, and provide an interface between these abstractions and Aldor code.

About the Polynomial System Solve Facility of Axiom, Macsyma, Maple, Mathematica, MuPAD, and Reduce — by Bill Page — last modified Nov 18, 2005 07:29 PM

We report on some experiences with the general purpose Computer Algebra Systems (CAS) Axiom, Macsyma, Maple, Mathematica, MuPAD, and Reduce solving systems of polynomial equations and the way they present their solutions. This snapshot (taken in the spring 1996) of the current power of the different systems in a special area concentrates both on CPU-times and the quality of the output.

Representation of mathematical objects in interactive books — by Bill Page — last modified Jun 21, 2005 06:01 PM

Andre M.A. van Leeuwen CWI, Dept. AM Kruislann 413 1098 SJ Amsterdam The Netherlands e-mail: leeuw@cwi.nl Abstract We present a model for the representation of mathematical objects in structured electronic documents, in a way that allows for interaction with applications such as computer algebra systems and proof checkers. Using a representation that reflects only the intrinsic information of an object, and storing application-dependent information in so-called application descriptions, it is shown how the translation from the internal to an external representation and vice versa can be achieved. Hereby a formalisation of the concept of context is introduced. The proposed scheme allows for a high degree of application integration, e.g., parallel evaluation of subexpressions (by different computer algebra systems), or a proof checker using a computer algebra system to verify an equation involving a symbolic computation.

How to Make AXIOM Into a Scratchpad — by Bill Page — last modified Nov 30, 2005 12:25 AM

Scratchpad [GrJe71] was a computer algebra system developed in the early 1970s. Like M&M (Maple [CGG91ab] and Mathematical [W01S92]) and other systems today, Scratchpad had one principal representation for mathematical formulae based on “expression trees”. Its user interface design was based on a pattern-matching paradigm with infinite rewriterule semantics, providing what we believe to be the most natural paradigm for interactive symbolic problem solving. Like M&M, however, user programs were interpreted, often resulting in poor performance relative to similar facilities coded in standard programming languages such as FORTRAN and C. Scratchpad development stopped in 1976 giving way to a new system design ([ JenR79], [JeTr81]) that evolved into AXIOM [JeSu92]. AXIOM has a strongly-typed programming language for building a library of parameterized types and algorithms, and a type-inferencing interpreter that accesses the library and can build any of an infinite number of types for interactive use.

The Type System of Aldor — by Bill Page — last modified Nov 18, 2005 07:29 PM

This paper gives a formal description of - at least a part of - the type system of Aldor, the extension language of the computer algebra system AXIOM. In the process of doing this a critique of the design of the system emerges.

Object Oriented Method for Axiom — by Bill Page — last modified Mar 03, 2006 07:14 AM

Axiom is a very powerful computer algebra system which combines two languages paradigms (functional and OOP). Mathematical world is complex and mathematicien use abstraction to design it. This paper presents some aspects of the object oriented development in Axiom. The axiom programming is based on several new tools for object oriented development, it uses two levels of class and some operations such that coerce: retract or convert which permit the type evolution. These notions introduce the concept of multi-view.

Object Oriented Method for Axiom. — by Bill Page — last modified May 24, 2007 04:09 PM

Axiom is a very powerful computer algebra system which combines two languages paradigms (functional and OOP). Mathematical world is complex and mathematicians use abstraction to design it. This paper presents some aspects of the object oriented development inAxiom. The axiom programming is based on several new tools for object oriented development, it uses two levels of class and some operations such that coerce, retract or convert which permit the type evolution. These notions introduce the concept of multi-view.

AXIOM, A Functional Language with Object Oriented Development — by Bill Page — last modified Mar 03, 2006 07:47 AM

We present in this paper, a study about the computer algebra system Axiom, which gives up many very interesting Software engineering concepts. This language is a functional language with an Object Oriented Development. This feature is very important for modelling the mathematical sens (All objects are functions). We present many problems of running and development in Axiom. We can note that Axiom\1 isthe only system of this category.

AXIOM, Langage fonctionnel à développement objet. — by Bill Page — last modified Aug 29, 2007 08:30 PM

Abstract: Nous profitons de cet article pour présenter une étude que nous avons faite d'un langage dédié au calcul formel qui présente des concepts de génie logiciel très intéressants. Ce langage est un langage fonctionnel dont le développement est orienté objet, ceci a pour première conséquence de trés bonnes capacités pour modéliser les mathématiques (Hiérarchie) et une exécution claire au sens mathématique (Tout est fonction). Nous soulignerons les faiblesses du modèle au travers d'une analyse du comportement de l'exécution et des problèmes de développements. Il faut noter que le langage Axiom est toujours le seul de sa catégorie.

Domains of data and domains of terms in AXIOM — by Bill Page — last modified Jun 20, 2007 05:33 PM

Abstract: This paper discusses the advantages of the AXIOM symbolic computation system, and illustrates them with some AXIOM2.0 code for directed graphs and free categories and groupoids on directed graphs. In order to implement the latter, we have to make a distinction between domains of data and domains of terms, where, for example, the first gives the data for a finite directed graph, whereas the latter converts this data into an object of Axiom category DirectedGraphCategory, where the terms range over the objects and arrows of the directed graph. --- The symbolic computation package AXIOM provides a high level programming language with several advantages for the coding of new mathematical structures and for manipulating with them. In this sense it could be said to make a contribution to "structural computation". This term reflects how the development of computation has paralleled that of mathematics, with, in turn, numbers, symbols, and now structures. Structures in AXIOM are formed using what AXIOM calls "categories" and "domains". It is in the construction of domains that the real work of programming AXIOM takes place. A domain is a type which defines a collection of exported symbols, which may denote types, constants and functions.

Fast and Loose Reasoning is Morally Correct — by Bill Page — last modified May 24, 2007 04:07 PM

Abstract: Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning. Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values. It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.

How does one program in the AXIOM System — by Bill Page — last modified Nov 18, 2005 07:29 PM

J.H. Davenport, School of Mathematical Sciences, University of Bath. Abstract: AXIOM is a computer algebra system superficially like many others, but fundamentally different in its internal construction, and therefore in the possibilities it offers to users and programmers. In these lecture notes we will explain, by example, the methodology that the author uses to programming substantial bits of mathematics in AXIOM.

Semantics of Categories in Aldor — by Bill Page — last modified Jul 21, 2006 02:07 AM

Author: A. D. Kennedy. We consider some questions about the semantics of Aldor regarding the way that types can be considered on an equal footing with any other objects in the language. After a digression into the relationship between Aldor categories and mathematical categories, we shall discuss the more practical issue of the limitations of the define keyword and what the compiler should do about them. Download 21-Jul-2006: http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/discussion/define.pdf

Order Sorted Computer Algebra and Coercions — by Bill Page — last modified Sep 13, 2005 08:50 AM

Nicolas James Doye University of Bath 1997. Abstract: Computer algebra systems are large collections of routines for solving mathematical problems algorithmically, efficiently and above all, symbolically. The more advanced and rigorous computer algebra systems ,for example Axiom, use the concept of strong types based on order-sorted algebra and category theory to ensure that operations are only applied to expressions when they "make sense". In cases where Axiom uses notions which are not covered by current mathematics we shall present new mathematics which will allow us to prove that all such cases are reducible to cases covered by the current theory. On the other hand, we shall also point out all the cases where Axiom deviates undesirably from the mathematical ideal. Furthermore we shall propose solutions to these deviations. Strongly typed systems ,especially of mathematics, become unusable unless the system can change the type in a way a user expects. We wish any type change expected by a user to be automated, "natural" and unique. "Coercions" are normally viewed as "natural type changing maps" -- this thesis shall rigorously define the word "coercion" in the context of computer algebra systems. We shall list some assumptions so that we may prove new results so that all coercions are unique -- this concept is called "coherence". We shall give an algorithm for automatically creating all coercions in type system which adheres to a set of assumptions. We shall prove that this is an algorithm and that it always returns a coercion when one exists. Finally, we present a demonstration implementation of this automated coercion algorithm in Axiom.

Formal Methods for Extensions to CAS — by Bill Page — last modified Apr 12, 2006 03:52 PM

Slides

Exact Real Arithmetic: A Case Study in Higher Order Programming — by Bill Page — last modified Jun 15, 2005 01:24 PM

Hans-J. Boehm, Robert Cartwright, Mark Riggle, Rice University. Two methods for implementing exact real arithmetic are explored. One method is based on formulating real numbers as functions that map rational tolerances to rational approximations. This approach, which was developed by constructive mathematicians as a concrete formalization of the real numbers, has lead to a surprisingly successful implementation. The second method formulates real numbers as potentially infinite sequences of digits, evaluated on demand. This approach has frequently been advocated by proponents of lazy functional languages in the computer science community. Ironically, it leads to much less satisfactory implementations. We discuss the theoretical problems involved in both methods, give algorithms for the basic arithmetic operations, and give an empirical comparison of the two techniques. We conclude with some general observations about the lazy evaluation paradigm and its implementation. 1986 ACM.

FOAM: A First Order Abstract Machine (Version 0.35) — by Bill Page — last modified Aug 08, 2006 09:06 AM

Autors: Stephen M. Watt, Peter A. Broadbery, Pietro Iglio, Scott C. Morrison, Jonathan M. Steinbach. Download 08-Aug-2006: http://www.aldor.org/docs/foam.pdf

Lightweight Formal Methods For Computer Algebra Systems — by Bill Page — last modified Nov 18, 2005 07:29 PM

In this paper we demonstrate the use of formal methods tools to provide a semantics for the type hierarchy of the AXIOM computer algebra system, and a methodology for Aldor program analysis and verication. We give examples of abstract specications of AXIOM primitives, and provide an interface between these abstractions and Aldor code.

Integrating Computer Algebra and Reasoning through the Type System of Aldor — by Bill Page — last modified Feb 28, 2006 09:25 PM

A number of combinations of reasoning and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor - the Axiom Library Compiler - and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct and explain a prototype implementation of a modified type-checking system written in Haskell.

On Computing Limits in a Symbolic Manipulation System — by Bill Page — last modified Apr 20, 2007 04:31 PM

Abstract. This thesis presents an algorithm for computing (one-sided) limits within a symbolic manipulation system. Computing limits is an important facility as limits are used both by other functions such as the definite integrator and to get directly some qualitative information about a given function. The algorithm we present is very compact, easy to understand and easy to implement. It also overcomes the cancellation problem other algorithms suffer from. These goals were achieved using a uniform method, namely by expanding the whole function into a series in terms of its most rapidly varying subexpression instead of a recursive bottom up expansion of the function. In the latter approach exact error terms have to be kept with each approximation in order to resolve the cancellation problem, and this may lead to an intermediate expression swell. Our algorithm avoids this problem and is thus suited to be implemented in a symbolic manipulation system. After discussing older approaches which are still prevalent in current computer algebra systems we present our algorithm in the context of exp-log functions. The algorithm is then compared with other approaches to compute limits of exp-log functions. We show then how the algorithm can be extended to larger classes of functions. This extension has been designed in the spirit of symbolic manipulation systems, i.e. we have tried to find an algorithm which can easily be implemented in today's computer algebra systems. Although a very pragmatic approach is used for this extension, it turns out that many functions can be covered. Furthermore we present an algorithm for computing hierarchical asymptotic series, which is based on our limit computation algorithm. This algorithm is discussed and results are presented. In a final chapter we focus on some particular problems which appear during an actual implementation in a symbolic manipulation system. We show an implementation of the algorithm in Maple and compare it on a set of examples with other implementations of limit algorithms in other symbolic manipulation systems.

Polymorphic Data Types, Objects, Modules and Functors, : is it too much? — by Bill Page — last modified Nov 18, 2005 07:29 PM

Abstraction is a powerful tool for developers and it is offered by numerous features such as polymorphism, classes, modules and functors, . . . A working programmer may be confused with this abundance. We develop a computer algebra library which is being certified. Reporting this experience made with a language (Ocaml [7]) offering all these features, we argue that they are all needed together. We compare several ways of using classes to represent algebraic concepts, trying to follow as close as possible mathematical specification. Then we show how to combine classes and modules to produce code having very strong typing properties. Currently, this library is made of one hundred units of functional code and behaves faster than analogous ones such as Axiom.

Mathematical Use Cases lead naturally to non-standard Inheritance Relationships — by Bill Page — last modified Jun 21, 2005 05:35 PM

Mathematical Use Cases lead naturally to non-standard Inheritance Relationships: How to make them accessible in a mainstream language? Marc Conrada, Tim French/a, Carsten Maple/a, Sandra Pott/b a/University of Luton, LU1 3JU, UK b/University of York, YO10 5DD, UK ABSTRACT Conceptually there is a strong correspondence between Mathematical Reasoning and Object-Oriented techniques. We investigate how the ideas of Method Renaming, Dynamic Inheritance and Interclassing can be used to strengthen this relationship. A discussion is initiated concerning the feasibility of each of these features.

Memory Allocation — by Bill Page — last modified Jul 21, 2006 01:54 AM

Author: Thomas Ashby. A short document to outline the memory allocation problems peculiar to the Paraldor project. Download 21-Jul-2006: http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/discussion/memory-addendum.ps

Memory Allocation in Aldor — by Bill Page — last modified Jul 21, 2006 01:58 AM

Author: A. D. Kennedy. We propose that the mod of memory allocation in Aldor should be another "orthogonal" property to be associated with objects. We discuss the reasons for this in the context of large-scale numerical computations using Aldor (the Paraldor project), and we consider what changes might be required in the compiler. Download 21-Jul-2006: http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/discussion/memory.pdf

Larch/Aldor---A Larch BISL For AXIOM and Aldor — by Bill Page — last modified Sep 18, 2006 02:03 AM

PhD thesis of Martin Dunstan. Download 14-Apr-2006: http://www.dcs.st-andrews.ac.uk/~mnd/publications/

Adding Larch/Aldor Specifications to Aldor — by Bill Page — last modified Sep 18, 2006 02:01 AM

Martin Dunstan: Adding Larch/Aldor Specifications to Aldor Abstract: We describe a proposal to add Larch-style annotations to the Aldor programming language, based on our PhD research. The annotations are intended to be machine-chackable and may be used for a variety of purposes ranging from compiler optimisations to verification condition (VC) generation. In this report we higlight the options available and describe the changes which would need to be made to the compiler to make use of this technology. Download 14-Apr 2006: http://www.dcs.st-andrews.ac.uk/~mnd/publications/

The type system of Axiom — by Bill Page — last modified Oct 19, 2005 12:03 PM

Slides by: Erik Poll Radboud University of Nijmegen

The Aldor-- language — by Bill Page — last modified Oct 19, 2005 11:52 AM

Abstract: This paper introduces the Aldor-- language, which is a functional programming language with dependent types and a powerful, type-based, overloading mechanism. The language is built on a subset of Aldor, the ‘library compiler’ language for the Axiom computer algebra system. Aldor-- is designed with the intention of incorporating logical reasoning into computer algebra computations. The paper contains a formal account of the semantics and type system of Aldor--; a general discussion of overloading and how the overloading in Aldor fits into the general scheme; examples of logic within Aldor-- and notes on the implementation of the system. ----- Simon Thompson and Leonid Timochouk Computing Laboratory, University of Kent Canterbury, CT2 7NF, UK

The Unknown in Computer Algebra — by Bill Page — last modified Nov 07, 2007 04:22 AM

James Davenport, Cristele Faure: Abstract: Computer algebra systems have to deal with the confusion between “programming variables” and “mathematical symbols”. We claim that they should also deal with “unknowns”, i.e. elements whose values are unknown, but whose type is known. For example, x^p != x if x is a symbol, but x^p = x if x in GF(p). We show how we have extended Axiom to deal with this concept.

Prospects for Category Theory in Aldor — by Ralf Hemmecke — last modified Nov 24, 2007 03:37 PM

Abstract: Ways of encorporating category theory constructions and results into the Aldor language are discussed. The main features of Aldor which make this possible are identified, examples of categorical construtions are provided and a suggestion is made for a foundation for rigorous results.

screen2.PNG — by Bill Page 2 — last modified Nov 07, 2007 06:07 AM

 

From Untyped to Polymorphically Typed Objects inMathematicalWeb Services — by Ralf Hemmecke — last modified Aug 04, 2008 08:40 AM

Bill Naylor, Julian Padget: Abstract: OpenMath is a widely recognised approach to the semantic markup of mathematics that is often used for communication between OpenMath compliant systems. The Aldor language has a sophisticated category-based type system that was specifically developed for the purpose of modelling mathematical structures, while the system itself supports the creation of small-footprint applications suitable for deployment as web services. In this paper we present our first results of how one may perform translations from generic OpenMath objects into values in specific Aldor domains, describing how the Aldor interface domain ExpressionTree is used to achieve this. We outline our Aldor implementation of an OpenMath translator, and describe an efficient extension of this to the Parser category. In addition, the Aldor service creation and invocation mechanism are explained. Thus we are in a position to develop and deploy mathematical web services whose descriptions may be directly derived from Aldor’s rich type language. Download 04-Aug-2008: http://www.cs.bath.ac.uk/~wn/Papers/aldorService.pdf

Reasoning about the elementary functions of complex analysis — by Ralf Hemmecke — last modified Mar 08, 2010 12:46 AM

Coreless, Jeffrey, Watt, Bradford, Davenport: There are many problems with the simplification of elementary functions, particularly over the complex plane. Systems tend to make "howlers"or not to simplify enough. In this paper we outline the "unwinding number" approach to such problems, and show how it can be used to prevent errors and to systematise such simplifications, even though we have not yet reduced the simplification process to a complete algorithm. The unsolved problems are probably more amenable to the techniques of artificial intelligence and theorems proving than the original problem of complex-variable analysis. Download: 08-Mar-2010: http://www.apmaths.uwo.ca/~djeffrey/Offprints/AMAI.pdf

New FOAM documentation — by Ralf Hemmecke — last modified Jun 07, 2011 02:34 PM

Pete Huerter, Stephen M. Watt: Incomplete FOAM description Download 07-Jun-2011: http://www.aldor.org/docs/foamManual.pdf

A language for computational algebra — by Richard D. Jenks IBM Research Center, Yorktown Heights, New York — last modified Nov 08, 2011 05:47 PM

This paper reports ongoing research at the IBM Research Center on the development of a language with extensible parameterized types and generic operators for computational algebra. The language provides an abstract data type mechanism for defining algorithms which work in as general a setting as possible. The language is based on the notions of domains and categories. Domains represent algebraic structures. Categories designate collections of domains having common operations with stated mathematical properties. Domains and categories are computed objects which may be dynamically assigned to variables, passed as arguments, and returned by functions. Although the language has been carefully tailored for the application of algebraic computation, it actually provides a very general abstract data type mechanism. Our notion of a category to group domains with common properties appears novel among programming languages (cf. image functor of RUSSELL) and leads to a very powerful notion of abstract algorithms missing from other work on data types known to the authors.

A Guide to Programming in BOOT — by Ralf Hemmecke — last modified Jan 12, 2012 12:14 AM

Author: Richard D. Jenks Abstract: BOOT is a high-level LISP language. The Scratchpad II Programming Language, here called SPAD was originally designed in 1981. In order to get experience with the procedural language component of SPAD, a typeless version of SPAD called BOOT was born. BOOT was then used to implement the current SPAD compiler. Download: 29-Nov-2011: http://daly.axiom-developer.org/boot.tgz (and concatenated via pdftk)