Coreless, Jeffrey, Watt, Bradford, Davenport: Reasoning about the elementary functions of complex analysis. 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.
Emmanuel Touratier: Etude du typage dans le syteme de calcul scientifique Aldor (Study of types in the Aldor scientific computation system)
W. M. Seiler: Applying AXIOM to Partial Differential Equations 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.
S. Boulme, T. Hardin, D. Hirschko V. Menissier-Morain, and R. Rioboo: On the way to certify Computer Algebra Systems 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.
J. H. Davenport: A New Algebra System 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.
Marc Conrad, Tim French, Carsten Maple, and Sandra Pott: Approaching Inheritance from a "Natural" Mathematical Perspective and from a Java Driven Viewpoint 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.
Erik Meijer, Maarten Fokkinga, Ross Paterson: Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire 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.
Nicolas Robidoux: Does Axiom Solve Systems of O.D.E.'s Like Mathematica? 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.
James Davenport, Christle Faure: The "Unknown" in Computer Algebra 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.
Saul Youssef: Prospects for Category Theory in Aldor 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.
Utilisation de logiciels libres pour la realization do TP MT26
akman-vicious.pdf (Book Review - Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena by Jon Barwise and Lawrence Moss)
Simon Thompson: Logic and Dependent Types in the Aldor Computer Algebra System 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. The logic is used to provide an axiomatisation of a number of familiar Aldor categories as well as a type of vectors.
William Naylor, Julian Padget: From Untyped to Polymorphically Typed Objects in Mathematical Web Services 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.
Balint Joo, Tony Kennedy: Possible Enhancements for Aldordoc 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, one 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.
Larry Lambe: Next Generation Computer Algebra Systems
Werner M. Seiler: Pseudo Differential Operators and Integrable Systems in AXIOM 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.
Stephen M. Watt, Peter A. Broadbery, Samuel S. Dooley, Pietro Iglio, Scott C. Morrison, Jonathan M. Steinbach, Robert S. Sutor: A First Report on the A# Compiler
Erik Poll, Simon Thompson: Adding the axioms to Axiom - Towards a system of automated reasoning in Aldor 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.
Larry Lambe and Richard Luczak: Object-Oriented Mathematical Programming and Symbolic/Numeric Interface
Renaud Rioboo: Real Algebraic Closure of an Ordered Field, Implementation in Axiom 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).
J. H. Griesmer, R. D. Jenks: SCRATCHPAD/1 AN INTERACTIVE FACILITY FOR SYMBOLIC MATHEMATICS 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.
W. M. Seiler and J. Calmet: JET - An AXIOM Environment for Geometric Computations with Differential Equations 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.
Jean-Louis Boulanger: Object Oriented Method for Axiom. 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.
Cezar Dominguez, Julio Rubio: Modeling Inheritance as Coercion in a Symbolic Computation System 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.
Andreas Weber: Algorithms for Type Inference with Coercions This paper presents algorithms that perform a type inference for a type system occurring in the context 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.
Robert S. Sutor, Richard D. Jenks: The Type Inference and Coercion Facilities in the Scratchpad II Interpreter 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.
Martin Dunstan, Tom Kelsey, Steve Linton, Ursula Martin: Lightweight Formal Methods For Computer Algebra Systems 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.
Hans-Gert Graebe: About the Polynomial System Solve Facility of Axiom, Macsyma, Maple, Mathematica, MuPAD, and Reduce 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.
Andre M.A. van Leeuwen: Representation of mathematical objects in interactive books 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.
Richard D. Jenks, Barry M. Trager: How to Make AXIOM Into a Scratchpad) Scratchpad was a computer algebra system developed in the early 1970s. Like M&M (Maple and Mathematica) 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 rewrite rule 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 that evolved into AXIOM. 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.
Erik Poll and Simon Thompson: The Type System of Aldor 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.
Jean Louis Boulanger: Object Oriented Method for Axiom Jean Louis Boulanger: Object Oriented Method for Axiom 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.
Jean Louis Boulanger: AXIOM, A Functional Language with Object Oriented Development 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 is the only system of this category.
Jean Louis Boulanger: AXIOM, Langage fonctionnel a developpement objet.
Ronald Brown, Winfried Dreckmann: Domains of data and domains of terms in AXIOM This paper discusses the advantages of the AXIOM symbolic computation system, and illustrates them with some AXIOM 2.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.
Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons: Fast and Loose Reasoning is Morally Correct 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.
J.H. Davenport: How does one program in the AXIOM System 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.
A. D. Kennedy: Semantics of Categories in Aldor 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.
Nicolas James Doye: Order Sorted Computer Algebra and Coercions 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.
Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton: Formal Methods for Extensions to CAS
Hans-J. Boehm, Robert Cartwright, Mark Riggle: Exact Real Arithmetic: A Case Study in Higher Order Programming 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.
Stephen M. Watt, Peter A. Broadbery, Pietro Iglio, Scott C. Morrison, Jonathan M. Steinbach: FOAM: A First Order Abstract Machine (Version 0.35)
foamManual.pdf Pete Huerter, Stephen M. Watt: New FOAM documentation
Martin Dunstan, Tom Kelsey, Steve Linton, Ursula Martin: Lightweight Formal Methods For Computer Algebra Systems 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^Lcation. We give examples of abstract specifications of AXIOM primitives, and provide an interface between these abstractions and Aldor code.
Erik Poll, Simon Thompson: Integrating Computer Algebra and Reasoning through the Type System of Aldor 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.
Dominik Gruntz: On Computing Limits in a Symbolic Manipulation System 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.
S. Boulme, T. Hardin, R. Rioboo: Polymorphic Data Types, Objects, Modules and Functors, : is it too much? 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) 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.
Marc Conrada, Tim French, Carsten Maple, Sandra Pott: Mathematical Use Cases lead naturally to non-standard Inheritance Relationships: How to make them accessible in a mainstream language? 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.
A. D. Kennedy: Memory Allocation in Aldor 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.
Martin N. Dunstan: Larch/Aldor---A Larch BISL For AXIOM and Aldor PhD thesis.
Martin N. Dunstan: Adding Larch/Aldor Specifications to Aldor 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.
Erik Poll: The type system of Axiom
Simon Thompson and Leonid Timochouk: The Aldor-- language 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.