diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 82fe76f..cf3a630 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -66,14 +66,6 @@ Proc. International Computing Symposium, Bonn, Germany, 1970 pp394-419
``LPL: LISP programming language''\\
IBM Research Report, RC3062 Sept 1970
-\bibitem[Buchberger 85]{BC85} Buchberger, Bruno; Caviness, Bob F. (eds)\\
-EUROCAL '85: European Conference on Computer Algebra, Linz, Austria,
-April 1-3, 1985;
-proceedings, volume 204 of Lecture Notes in Computer Science. Springer-Verlag,
-Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985,
-ISBN 0-387-15983-5 (vol. 1), 0-387-15984-3 (vol. 2) LLCN QA155.7.E4 E86 1985
-Two volumes
-
\bibitem[Broadbery 95]{BGDW95} Broadbery, P. A.; G{\'o}mez-D{\'\i}az, T.;
Watt, S. M.\\
``On the implementation of dynamic evaluation''\\
@@ -104,11 +96,33 @@ IT 255, Oct 1993
``AXIOM, A Functional Language with Object Oriented Development''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-\bibitem[Boulanger 95]{Bou95} Boulanger, J.L.\\
-``Object oriented method for Axiom''\\
+\begin{adjustwidth}{2.5em}{0pt}
+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 modeling the
+mathematical world (Hierarchy) and provides a running with
+mathematical sense. (All objects are functions). We present many
+problems of running and development in Axiom. We can note that Aiom is
+the only system of this category.
+\end{adjustwidth}
+
+\bibitem[Boulanger 94]{Bou94} Boulanger, J.L.\\
+``Object Oriented Method for Axiom''\\
ACM SIGPLAN Notices, 30(2) pp33-41 February 1995 CODEN SINODQ ISSN 0362-1340\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+Axiom is a very powerful computer algebra system which combines two
+language 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 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
+{\sl coerce}, {\sl retract}, or {\sl convert} which permit the type
+evolution. These notions introduce the concept of multi-view.
+\end{adjustwidth}
+
\bibitem[Bronstein 87]{Bro87} Bronstein, Manuel\\
``Integration of Algebraic and Mixed Functions''\\
in [Wit87], p18
@@ -150,16 +164,6 @@ Elektronik, 43(15) pp107-110, July 1994, CODEN EKRKAR ISSN 0013-5658
``Multimedia tools for communicating mathematics''\\
Springer-Verlag ISBN 3-540-42450-4 p58
-\bibitem[Boulme 00]{BHR00} Boulm\'e, S.; Hardin, T.; Rioboo, R.\\
-``Polymorphic Data Types, Objects, Modules and Functors,: is it too much?''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
-\bibitem[Boulme 01]{BHHMR01}
-Boulm\'e, S.; Hardin, T.; Hirschkoff, D.; M\'enissier-Morain, V.; Rioboo, R.\\
-``On the way to certify Computer Algebra Systems''\\
-Calculemus-2001\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
\bibitem[Brown 94]{BT94} Brown, R.; Tonks, A.\\
``Calculations with simplicial and cubical groups in AXIOM''\\
Journal of Symbolic Computation 17(2) pp159-179 February 1994
@@ -169,6 +173,26 @@ CODEN JSYCEH ISSN 0747-7171
``Domains of data and domains of terms in AXIOM''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+The main new concept we wish to illustrate in this paper is a
+distinction between ``domains of data'' and ``domains of terms'', and
+its use in the programming of certain mathematical structures.
+Although this distinction is implicit in much of the programming work
+that has gone into the construction of Axiom categories and domains,
+we believe that a formalisation of this is new, that standards and
+conventions are necessary and will be useful in various other
+contexts. We shall show how this concept may be used for the coding of
+free categories and groupoids on directed graphs.
+\end{adjustwidth}
+
+\bibitem[Buchberger 85]{BC85} Buchberger, Bruno; Caviness, Bob F. (eds)\\
+EUROCAL '85: European Conference on Computer Algebra, Linz, Austria,
+April 1-3, 1985;
+proceedings, volume 204 of Lecture Notes in Computer Science. Springer-Verlag,
+Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985,
+ISBN 0-387-15983-5 (vol. 1), 0-387-15984-3 (vol. 2) LLCN QA155.7.E4 E86 1985
+Two volumes
+
\bibitem[Buhl 05]{Buh05} Buhl, Soren L.\\
``Some Reflections on Integrating a Computer Algebra System in R''\\
\verb|www.math.auc.dk/~slb/kurser/software/RCompAlg.pdf|
@@ -261,12 +285,32 @@ Pott, Sandra\\
a Java Driven Viewpoint: a Comparative Review''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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 there 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 thos 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.
+\end{adjustwidth}
+
\bibitem[Conrad (b)]{CFMPxxb} Conrad, Marc; French, Tim; Maple, Carsten;
Pott, Sandra\\
``Mathematical Use Cases lead naturally to non-standard Inheritance
Relationships: How to make them accessible in a mainstream language?''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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.
+\end{adjustwidth}
+
\bibitem[Cuypers]{CHK} Cuypers, Hans; Hendriks, Maxim; Knopper, Jan Willem\\
``Interactive Geometry inside MathDox''\\
\verb|www.win.tue.nl/~hansc/MathDox_and_InterGeo_paper.pdf|
@@ -343,6 +387,11 @@ IBM Corporation, Yorktown Heights, NY
\bibitem[Davenport 88]{DST88} Davenport, J.H.; Siret, Y.; Tournier, E.\\
Computer Algebra: Systems and Algorithms for Algebraic Computation.
Academic Press, New York, NY, USA, 1988, ISBN 0-12-204232-9
+\verb|staff.bath.ac.uk/masjhd/masternew.pdf|
+
+\bibitem[Davenport 14]{Dav14} Davenport, James H.\\
+``Computer Algebra textbook''\\
+\verb|staff.bath.ac.uk/masjhd/JHD-CA.pdf|
\bibitem[Davenport 89]{Dav89} Davenport, J.H. (ed)\\
EUROCAL '87 European Conference on Computer Algebra Proceedings
@@ -381,6 +430,14 @@ Grove, IL, USA and Oxford, UK December 1992\\
\verb|http://www.nag.co.uk/doc/TechRep/axiomtr.html|\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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 its users and programmers. In these
+lecture notes, we will explain, by example, the methodology that the
+author uses for programming substantial bits of mathematics in Axiom.
+\end{adjustwidth}
+
\bibitem[Davenport 92c]{DT92} Davenport, J. H.; Trager, B. M.\\
``Scratchpad's view of algebra I: Basic commutative algebra''\\
DISCO 90 Capri, Italy April 1990 ISBN 0-387-52531-9 pp40-54\\
@@ -399,6 +456,15 @@ Downer's Grove, IL, USA and Oxford, UK, August 1993\\
``The Unknown in Computer Algebra''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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 examples $x^p \ne 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.
+\end{adjustwidth}
+
\bibitem[Davenport 00]{Dav00} Davenport, James\\
``13th OpenMath Meeting''
James H. Davenport
@@ -433,6 +499,19 @@ and Laine, M. and Valkeila, E. pp1-12 University of Helsinki, Finland (1994)
In Gianni [Gia89], pp440-446 ISBN 3-540-51084-2
LCCN QA76.95.I57 1998 Conference held jointly with AAECC-6
+\bibitem[Dingle 94]{Din94} Dingle, Adam; Fateman, Richard\\
+``Branch Cuts in Computer Algebra''\\
+1994 ISSAC, Oxford (UK), July 1994\\
+\verb|www.cs.berkeley.edu/~fateman/papers/ding.ps|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Many standard functions, such as the logarithms and square root
+functions, cannot be defined continuously on the complex
+plane. Mistaken assumptions about the properties of these functions
+lead computer algebra systems into various conundrums. We discuss how
+they can manipulate such functions in a useful fashion.
+\end{adjustwidth}
+
\bibitem[DLMF]{DLMF}.\\
``Digital Library of Mathematical Functions''\\
\verb|http://dlmf.nist.gov/software/#T1|
@@ -443,59 +522,87 @@ Vancouver, BC, Canada: proceedings of the 1999 International Symposium on
Symbolic and Algebraic Computation. ACM Press, New York, NY 10036, USA, 1999.
ISBN 1-58113-073-2 LCCN QA76.95.I57 1999
-\bibitem[Dos Reis 11]{DR11}
-\bibitem[Dos Reis 12]{DR12} Dos Reis, Gabriel; Matthews, David; Li, Yue\\
-``Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants
-and Computer Algebra System Framework''\\
-Calculemus (2011) Springer
-\verb|paradise.caltech.edu/~yli/paper/oa-polyml.pdf|
-
+\bibitem[Dos Reis 12]{DR12} Dos Reis, Gabriel\\
``A System for Axiomatic Programming''\\
Proc. Conf. on Intelligent Computer Mathematics, Springer (2012)
\verb|www.axiomatics.org/~gdr/liz/cicm-2012.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+We present the design and implementation of a system for axiomatic
+programming, and its application to mathematical software
+construction. Key novelties include a direct support for user-defined
+axiom establishing local equality between types, and overload
+resolution based on equational theories and user-defined local
+axioms. We illustrate uses of axioms, and their organization into
+concepts, in structured generic programming as practiced in
+computational mathematical systems.
+\end{adjustwidth}
+
\bibitem[Doye 97]{Doy97} Doye, Nicolas James\\
``Order Sorted Computer Algebra and Coercions''\\
Ph.D. Thesis University of Bath 1997\\
\verb|axiom-wiki.newsynthesis.org/public/refs/doye-aldor-phd.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+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 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 coerion algorithm in Axiom.
+\end{adjustwidth}
+
\bibitem[Doye 99]{Doy99} Doye, Nicolas J.\\
``Automated coercion for Axiom''\\
In Dooley [Doo99], pp229-235
ISBN 1-58113-073-2 LCCN QA76.95.I57 1999 ACM Press\\
\verb|http://www.acm.org/pubs/contents/proceedings/issac/309831|
-\bibitem[Dominguez]{DRxx} Dom\'inguez, C\'esar; Rubio, Julio\\
+\bibitem[Dominguez 01]{DR01} Dom\'inguez, C\'esar; Rubio, Julio\\
``Modeling Inheritance as Coercion in a Symbolic Computation System''
ISSAC 2001 ACM 1-58113-417-7/01/0007\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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.
+\end{adjustwidth}
+
\bibitem[Dunstan 97]{Dun97} Dunstan, Martin; Ursula, Martin; Linton, Steve\\
``Embedded Verification Techniques for Computer Algebra Systems''\\
Grant citation GR/L48256 Nov 1, 1997-Feb 28, 2001\\
\verb|www.cs.st-andrews.ac.uk/research/output/detail?output=ML97.php|
-\bibitem[Dunstan 98]{Dun98} Dunstan, Martin; Kelsey, Tom; Linton, Steve;
-Martin, Ursula\\
-``Lightweight Formal Methods For Computer Algebra Systems''\\
-\verb|www.cs.st-andrews.ac.uk/~tom/pub/issac98.pdf|\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
-\bibitem[Dunstan 99]{Dun99} Dunstan, Martin; Kelsey, Tom; Martin, Ursula;
-Linton, Steve\\
-``Formal Methods for Extensions to CAS''\\
-FM 99, Toulouse, France, Sept 20-24, 1999, p1758-1777
-
-\bibitem[Dunstan 99a]{Dun99a} Dunstan, MN\\
-``Larch/Aldor - A Larch BISL for AXIOM and Aldor''\\
-PhD Thesis, 1999\\
-\verb|www.cs.st-andrews.uk/files/publications/Dun99.php|\\
-\verb|axiom-portal.newsynthesis.org/refs/articles/mnd-sep99-thesis.pdf|
-
-\bibitem[Dunstan (a)]{Dunxx} Dunstan, Martin N.\\
-``Adding Larch/Aldor Specifications to Aldor''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
\bibitem[Dunstan 01]{DGKM01} Dunstan, Martin; Gottliebsen, Hanne;
Kelsey, Tom; Martin, Ursula\\
``Computer Algebra meets Automated Theorem Proving: A Maple-PVS Interface''
@@ -539,6 +646,30 @@ In Watanabe and Nagata [WN90], pp60-67 ISBN 0-89791-401-5 LCCN QA76.95.I57 1990
4/19/2005\hfill\\
\verb|www.cs.berkeley.edu/~fateman/papers/axiom.pdf|
+\bibitem[Fateman 06]{Fat06} Fateman, R. J.\\
+``Building Algebra Systems by Overloading Lisp''\\
+\verb|www.cs.berkeley.edu/~fateman/generic/overload-small.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Some of the earliest computer algebra systems (CAS) looked like
+overloaded languages of the same era. FORMAC, PL/I FORMAC, Formula
+Algol, and others each took advantage of a pre-existing language base
+and expanded the notion of a numeric value to include mathematical
+expressions. Much more recently, perhaps encouraged by the growth in
+popularity of C++, we have seen a renewal of the use of overloading to
+implement a CAS.
+
+This paper makes three points. 1. It is easy to do overloading in
+Common Lisp, and show how to do it in detail. 2. Overloading per se
+provides an easy solution to some simple programming problems. We show
+how it can be used for a ``demonstration'' CAS. Other simple and
+plausible overloadings interact nicely with this basic system. 3. Not
+all goes so smoothly: we can view overloading as a case study and
+perhaps an object lesson since it fails to solve a number of
+fairly-well articulated and difficult design issues in CAS for which
+other approaches are preferable.
+\end{adjustwidth}
+
\bibitem[Faure 00a]{FDN00a} Faure, Christ\'ele; Davenport, James\\
``Parameters in Computer Algebra''
@@ -661,6 +792,15 @@ Journal of Symbolic Computation, Vol39, Num 5, 2005
Mathematica, MuPAD, and Reduce''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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 of 1996)
+of the current power of the different systems in a special area
+concentrates on both CPU-times and the quality of the output.
+\end{adjustwidth}
+
\bibitem[Grabmeier 91]{GHK91} Grabmeier, J.; Huber, K.; Krieger, U.\\
``Das ComputeralgebraSystem AXIOM bei kryptologischen und
verkehrstheoretischen Untersuchungen des
@@ -692,6 +832,16 @@ In Petrick [Pet71], pp42-58. LCCN QA76.5.S94 1971\\
SYMSAC'71 Proc. second ACM Symposium on Symbolic and Algebraic
Manipulation pp45-48
+\begin{adjustwidth}{2.5em}{0pt}
+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.
+\end{adjustwidth}
+
\bibitem[Griesmer 72a]{GJ72a} Griesmer, J.; Jenks, R.\\
``Experience with an online symbolic math system SCRATCHPAD''\\
in Online'72 [Onl72] ISBN 0-903796-02-3 LCCN QA76.55.O54 1972 Two volumes
@@ -721,6 +871,25 @@ Thesis, Swiss Federal Institute of Technology Z\"urich 1996
Diss. ETH No. 11432\\
\verb|www.cybertester.com/data/gruntz.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+This thesis presents an algorithm for computing (one-sided) limits
+within a symbolic manipulation system. Computing limtis 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 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.
+\end{adjustwidth}
+
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Hassner 87]{HBW87} Hassner, Martin; Burge, William H.;
@@ -803,11 +972,24 @@ In Fitch [Fit84], pp123-147. ISBN 0-387-13350-X LCCN QA155.7.E4 I57 1984
\bibitem[Jenks 86]{JWS86} Jenks, Richard D.; Sutor, Robert S.;
Watt, Stephen M.\\
-``Scratchpad II: an abstract datatype system for mathematical computation''\\
+``Scratchpad II: An Abstract Datatype System for Mathematical Computation''\\
Research Report RC 12327 (\#55257), Iinternational Business Machines, Inc.,
Thomas J. Watson Research Center, Yorktown Heights, NY, USA, 1986 23pp
\verb|www.csd.uwo.ca/~watt/pub/reprints/1987-ima-spadadt.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+Scratchpad II is an abstract datatype language and system that is
+under development in the Computer Algebra Group, Mathematical Sciences
+Department, at the IBM Thomas J. Watson Research Center. Some features
+of APL that made computation particularly elegant have been borrowed.
+Many different kinds of computational objects and data structures are
+provided. Facilities for computation include symbolic integration,
+differentiation, factorization, solution of equations and linear
+algebra. Code economy and modularity is achieved by having
+polymorphic packages of functions that may create datatypes. The use
+of categories makes these facilities as general as possible.
+\end{adjustwidth}
+
\bibitem[Jenks 87]{JWS87} Jenks, Richard D.; Sutor, Robert S.;
Watt, Stephen M. \\
``Scratchpad II: an Abstract Datatype System for Mathematical Computation'' \\
@@ -932,6 +1114,28 @@ Concept: Applications to Research in Algebra''\\
$21^{st}$ Nordic Congress of Mathematicians 1992\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+One way in which mathematicians deal with infinite amounts of data is
+symbolic representation. A simple example is the quadratic equation
+\[x = \frac{-b\pm\sqrt{b^2-4ac}}{2a}\]
+a formula which uses symbolic representation to describe the solutions
+to an infinite class of equations. Most computer algebra systems can
+deal with polynomials with symbolic coefficients, but what if symbolic
+exponents are called for (e.g. $1+t^i$)? What if symbolic limits on
+summations are also called for, for example
+\[1+t+\ldots+t^i=\sum_j{t^j}\]
+The ``Scratchpad Concept'' is a theoretical ideal which allows the
+implementation of objects at this level of abstraction and beyond in a
+mathematically consistent way. The Axiom computer algebra system is an
+implementation of a major part of the Scratchpad Concept. Axiom
+(formerly called Scratchpad) is a language with extensible
+parameterized types and generic operators which is based on the
+notions of domains and categories. By examining some aspects of the
+Axiom system, the Scratchpad Concept will be illustrated. It will be
+shown how some complex problems in homologicial algebra were solved
+through the use of this system.
+\end{adjustwidth}
+
\bibitem[Lambe 93]{Lam93} Lambe, Larry\\
``On Using Axiom to Generate Code''\\
(preprint) 1993\\
@@ -942,6 +1146,18 @@ $21^{st}$ Nordic Congress of Mathematicians 1992\\
$3^{rd}$ International Conf. on Expert Systems in Numerical Computing 1993\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+The Axiom language is based on the notions of ``categories'',
+``domains'', and ``packages''. These concepts are used to build an
+interface between symbolic and numeric calculations. In particular, an
+interface to the NAG Fortran Library and Axiom's algebra and graphics
+facilities is presented. Some examples of numerical calculations in a
+symbolic computational environment are also included using the finite
+element method. While the examples are elementary, we believe that
+they point to very powerful methods for combining numeric and symbolic
+computational techniques.
+\end{adjustwidth}
+
\bibitem[Lebedev 08]{Leb08} Lebedev, Yuri\\
``OpenMath Library for Computing on Riemann Surfaces''\\
PhD thesis, Nov 2008 Florida State University\\
@@ -960,10 +1176,6 @@ June 29, 1996 \\
``The Dynamic Real Closure implemented in Axiom''\\
\verb|lecerf.perso.math.cnrs.fr/software/drc/drc.ps|
-\bibitem[Leeuwen]{Leexx} van Leeuwen, Andr\'e M.A.\\
-``Representation of mathematical object in interactive books''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
\bibitem[Levelt 95]{Lev95} Levelt, A. H. M. (ed)\\
ISSAC '95: Proceedings of the 1995 International
Symposium on Symbolic and Algebraic Computation: July 10-12, 1995, Montreal,
@@ -989,6 +1201,11 @@ Systems''\\
ISSAC 2011
\verb|www.axiomatics.org/~gdr/concurrency/oa-conc-issac11.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+This paper proposes a non-intrusive automatic parallelization
+framework for typeful and property-aware computer algebra systems.
+\end{adjustwidth}
+
\bibitem[Linton 93]{Lin93} Linton, Steve\\
``Vector Enumeration Programs, version 3.04''\\
\verb|www.cs.st-andrews.ac.uk/~sal/nme/nme_toc.html#SEC1|
@@ -1080,19 +1297,63 @@ CACM August 1971 Vol 14 No. 8 pp527-537
Services''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+OpenMath is a widely recognized 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 interfae
+domain ExpresstionTree is used to achieve this. We outline our Aldor
+implementation of an OpenMath translator, and describe an efficient
+extention 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.
+\end{adjustwidth}
+
\bibitem[Naylor 95]{N95} Naylor, Bill\\
``Symbolic Interface for an advanced hyperbolic PDE solver''\\
\verb|www.sci.csd.uwo.ca/~bill/Papers/symbInterface2.ps|
-\bibitem[Naylor 00a]{N00} Naylor, Bill\\
-``Polynomial GCD Using Straight Line Program Representation''\\
-PhD. Thesis, University of Bath, 2000\\
-\verb|www.sci.csd.uwo.ca/~bill/thesis.ps|
+\begin{adjustwidth}{2.5em}{0pt}
+An Axiom front end is described, which is used to generate
+mathematical objects needed by one of the latest NAG routines, to be
+included in the Mark 17 version of the NAG Numerical library. This
+routine uses powerful techniques to find the solution to Hyperbolic
+Partial Differential Equations in conservation form and in one spatial
+dimension. These mathematical objects are non-trivial, requiring much
+mathematical knowledge on the part of the user, which is otherwise
+irrelvant to the physical problem which is to be solved. We discuss
+the individual mathematical objects, considering the mathematical
+theory which is relevant, and some of the problems which have been
+encountered and solved during the FORTRAN generation necessary to
+realise the object. Finally we display some of our results.
+\end{adjustwidth}
\bibitem[Naylor 00b]{ND00} Naylor, W.A.; Davenport, J.H.\\
``A Monte-Carlo Extension to a Category-Based Type System''\\
\verb|www.sci.csd.uwo.ca/~bill/Papers/monteCarCat3.ps|
+\begin{adjustwidth}{2.5em}{0pt}
+The normal claim for mathematics is that all calculations are 100\%
+accurate and therefore one calculation can rely completely on the
+results of sub-calculations, hoever there exist {\sl Monte-Carlo}
+algorithms which are often much faster than the equivalent
+deterministic ones where the results will have a prescribed
+probability (presumably small) of being incorrect. However there has
+been little discussion of how such algorithms can be used as building
+blocks in Computer Algebra. In this paper we describe how the
+computational category theory which is the basis of the type structure
+used in the Axiom computer algebra system may be extended to cover
+probabilistic algorithms, which use Monte-Carlo techniques. We follow
+this with a specific example which uses Straight Line Program
+representation.
+\end{adjustwidth}
+
\bibitem[Norman 75]{Nor75} Norman, A. C.\\
``Computing with formal power series''\\
ACM Transactions on Mathematical Software, 1(4) pp346-356
@@ -1143,24 +1404,6 @@ New York, NY 10036, USA, 1971. LCCN QA76.5.S94 1971
Devlin, Keith (ed.)
Computers and Mathematics November 1993, Vol 40, Number 9 pp1203-1210
-\bibitem[Poll 99a]{P99a} Poll, Erik\\
-``The Type System of Axiom''\\
-\verb|www.cs.ru.nl/E.Poll/talks/axiom.pdf|
-
-\bibitem[Poll 99]{PT99} Poll, Erik; Thompson, Simon\\
-``The Type System of Aldor''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
-\bibitem[Poll 00]{PT00} Poll, Erik; Thompson, Simon\\
-``Integrating Computer Algebra and Reasoning through the Type System
-of Aldor''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
-\bibitem[Poll (a)]{PTxx} Poll, Erik; Thompson, Simon\\
-``Adding the axioms to Axiom. Toward a system of automated reasoning in
-Aldor''\\
-\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
-
\bibitem[Poll (b)]{Polxx} Poll, Erik\\
``The type system of Axiom''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
@@ -1183,12 +1426,38 @@ A281 1986 ACM order number 505860
July 1993\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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.
+
+Consider the following system of O.D.E.'s
+\[
+\begin{array}{rcl}
+\frac{dx_1}{dt} & = & \left(1+\frac{cos t}{2+sin t}\right)x_1\\
+\frac{dx_2}{dt} & = & x_1 - x_2
+\end{array}
+\]
+This is a very simple system: $x_1$ is actually uncoupled from $x_2$
+\end{adjustwidth}
+
\bibitem[Rioboo 92]{Rio92} Rioboo, R.\\
``Real algebraic closure of an ordered field, implementation in Axiom''\\
In Wang [Wan92], pp206-215 ISBN 0-89791-489-9 (soft cover)
0-89791-490-2 (hard cover) LCCN QA76.95.I59 1992\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+Real algebraic numbers appear in many Computer Algebra problems. For
+instance the determination of a cylindrical algebraic decomposition
+for an euclidean 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).
+\end{adjustwidth}
+
\bibitem[Roesner 95]{Roe95} Roesner, K. G.\\
``Verified solutions for parameters of an exact solution for
non-Newtonian liquids using computer algebra'' Zeitschrift fur Angewandte
@@ -1231,27 +1500,94 @@ In ACM [ACM89], pp17-25 ISBN 0-89791-325-6 LCCN QA76.95.I59 1989
SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic
Manipulation) 2591) pp10-23 Jan. 1991 CODEN SIGSBZ ISSN 0163-5824
+\bibitem[Seiler 94]{Sei94} Seiler, Werner Markus\\
+``Analysis and Application of the Formal Theory of Partial Differential
+Equations''\\
+PhD thesis, School of Physics and Materials, Lancaster University (1994)\\
+\verb|www.mathematik.uni-kassel.de/~seiler/Papers/Diss/diss.ps.gz|
+
+\begin{adjustwidth}{2.5em}{0pt}
+An introduction to the formal theory of partial differential equations
+is given emphasizing the properties of involutive symbols and
+equations. An algorithm to complete any differential equation to an
+involutive one is presented. For an involutive equation possible
+values for the number of arbitrary functions in its general solution
+are determined. The existence and uniqueness of solutions for analytic
+equations is proven. Applications of these results include an
+analysis of symmetry and reduction methods and a study of gauge
+systems. It is show that the Dirac algorithm for systems with
+constraints is closely related to the completion of the equation of
+motion to an involutive equation. Specific examples treated comprise
+the Yang-Mills Equations, Einstein Equations, complete and Jacobian
+systems, and some special models in two and three dimensions. To
+facilitate the involved tedious computations an environment for
+geometric approaches to differential equations has been developed in
+the computer algebra system Axiom. The appendices contain among others
+brief introductions into Carten-K\"ahler Theory and Janet-Riquier Theory.
+\end{adjustwidth}
+
\bibitem[Seiler 94a]{Sei94a} Seiler, W.M.\\
``Completion to involution in AXIOM''\\
in Calmet [Cal94] pp103-104
-\bibitem[Sieler 94b]{Sie94b} Seiler, W.M.\\
+\bibitem[Sieler 94b]{Sei94b} Seiler, W.M.\\
``Pseudo differential operators and integrable systems in AXIOM''\\
Computer Physics Communications, 79(2) pp329-340 April 1994 CODEN CPHCBZ
ISSN 0010-4655\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+An implementation of the algebra of pseudo differential operators in
+the computer algebra system Axiom is described. In several exmaples
+the application of the package to typical computations in the theory
+of integrable systems is demonstrated.
+\end{adjustwidth}
+
\bibitem[Seiler 95]{Sei95} Seiler, W.M.\\
``Applying AXIOM to partial differential equations''\\
Internal Report 95-17, Universit\"at Karlsruhe, Fakult\"at f\"ur Informatik
1995\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+We present an Axiom environment called JET for geometric computations
+with partial differential equations within the framework of the jet
+bundle formalism. This comprises expecially 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 implementations are described and
+applications are given. An appendix contains tables of all exported
+functions.
+\end{adjustwidth}
+
\bibitem[Seiler 95b]{SC95} Seiler, W.M.; Calmet, J.\\
``JET -- An Axiom Environment for Geometric Computations with Differential
Equations''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+JET is an environment within the computer algebra system Axiom to
+perform such computations. The current implementation emphasises 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.
+\end{adjustwidth}
+
+\bibitem[Seiler 97]{Sei97} Seiler, Werner M.\\
+``Computer Algebra and Differential Equations: An Overview''\\
+\verb|www.mathematik.uni-kassel.di/~seiler/Papers/Postscript/CADERep.ps.gz|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We present an informal overview of a number of approaches to
+differential equations which are popular in computer algebra. This
+includes symmetry and completion theory, local analysis, differential
+ideal and Galois theory, dynamical systems and numerical analysis. A
+large bibliography is provided.
+\end{adjustwidth}
+
\bibitem[Seiler (a)]{Seixx} Seiler, W.M.\\
``DETools: A Library for Differential Equations''\\
\verb|iaks-www.ira.uka.de/iaks-calmet/werner/werner.html|
@@ -1285,11 +1621,18 @@ Symposium on Applied Computing, Kansas City Convention Center, March 1-3, 1992
pp1243-1247. ACM Press, New York, NY 10036, USA, 1992. ISBN 0-89791-502-X
LCCN QA76.76.A65 S95 1992
-\bibitem[Smith 07]{SDJ-7} Smith, Jacob; Dos Reis, Gabriel; Jarvi, Jaakko\\
+\bibitem[Smith 07]{SDJ07} Smith, Jacob; Dos Reis, Gabriel; Jarvi, Jaakko\\
``Algorithmic differentiation in Axiom''\\
ACM SIGSAM ISSAC Proceedings 2007 Waterloo, Canada 2007 pp347-354
ISBN 978-1-59593-743-8
+\begin{adjustwidth}{2.5em}{0pt}
+This paper describes the design and implementation of an algorithmic
+differentiation framework in the Axiom computer algebra system. Our
+implementation works by transformations on Spad programs at the level
+of the typed abstract syntax tree.
+\end{adjustwidth}
+
\bibitem[SSC92]{SSC92}.\\
``Algorithmic Methods For Lie Pseudogroups''
In N. Ibragimov, M. Torrisi and A. Valenti, editors, Proc. Modern Group
@@ -1327,6 +1670,19 @@ in the Scratchpad II interpreter''\\
Research report RC 12595 (\#56575),
IBM Thomas J. Watson Research Center, Yorktown Heights, NY, USA, 1987, 11pp
+\begin{adjustwidth}{2.5em}{0pt}
+The Scratchpad II system is an abstract datatype programming language,
+a compiler for the language, a library of packages of polymorphic
+functions and parameterized 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 intepreter and how it attempts to provide a user
+friendly and relatively weakly typed front end for the strongly typed
+programming language.
+\end{adjustwidth}
+
\bibitem[Sutor 88]{Su88} Sutor, Robert S.\\
``A guide to programming in the scratchpad 2 interpreter''\\
IBM Manual, March 1988
@@ -1337,10 +1693,35 @@ IBM Manual, March 1988
``Logic and dependent types in the Aldor Computer Algebra System''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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 {\sl 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.
+\end{adjustwidth}
+
\bibitem[Thompson (a)]{TTxx} Thompson, Simon; Timochouk, Leonid\\
``The Aldor\-\- language''\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+This paper introduces the \verb|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. \verb|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 \verb|Aldor--|; a general discussion of overloading and how the
+overloading in \verb|Aldor--| fits into the general scheme; examples
+of logic within \verb|Aldor--| and notes on the implementation of the
+system.
+\end{adjustwidth}
+
\bibitem[Touratier 98]{Tou98} Touratier, Emmanuel\\
``Etude du typage dans le syst\`eme de calcul scientifique Aldor''\\
Universit\'e de Limoges 1998\\
@@ -1428,7 +1809,8 @@ Symbolic and Algebraic Computation, ISSAC'91, July 15-17, 1991, Bonn, Germany,
ACM Press, New York, NY 10036, USA, 1991 ISBN 0-89791-437-6
LCCN QA76.95.I59 1991
-\bibitem[Watt 94a]{Wat94a} Watt, Stephen M., et. al.\\
+\bibitem[Watt 94a]{Wat94a} Watt, Stephen M.; Dooley, S.S.; Morrison, S.C.;
+Steinback, J.M.; Sutor, R.S.\\
``A\# User's Guide''\\
Version 1.0.0 O($\epsilon{}^1$) June 8, 1994
@@ -1447,6 +1829,11 @@ Steinbach, J.M.; Morrison, S.C.; Sutor, R.S.\\
``AXIOM Library Compiler Users Guide''\\
The Numerical Algorithms Group (NAG) Ltd, 1994
+\bibitem[Watt 01]{Wat01} Watt, Stephen M.; Broadbery, Peter A.; Iglio, Pietro;
+Morrison, Scott C.; Steinbach, Jonathan M.\\
+``FOAM: A First Order Abstract Machine Version 0.35''\\
+IBM T. J. Watson Research Center (2001)
+
\bibitem[Weber 93]{Web93} Weber, A.\\
``On coherence in computer algebra''\\
In Miola [Mio93], pp95-106 ISBN 3-540-57235-X LCCN QA76.9.S88I576 1993
@@ -1456,6 +1843,20 @@ In Miola [Mio93], pp95-106 ISBN 3-540-57235-X LCCN QA76.9.S88I576 1993
ISSAC 94 ACM 0-89791-638-7/94/0007\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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.
+\end{adjustwidth}
+
\bibitem[Wei-Jiang 12]{WJ12} Wei-Jiang\\
``Top free algebra System''\\
\verb|wei-jiang.com/it/software/top-free-algebra-system-bye-mathematica-bye-maple|
@@ -1493,6 +1894,14 @@ Oxford University Press (2000) ISBN0-19-512516-9
October 2004\\
\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+\begin{adjustwidth}{2.5em}{0pt}
+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
+constructions are provided and a suggestion is made for a foundation
+for rigorous results.
+\end{adjustwidth}
+
\bibitem[Yun 83]{Yun83} Yun, David Y.Y.\\
``Computer Algebra and Complex Analysis''\\
Computational Aspects of Complex Analysis pp379-393
@@ -1942,6 +2351,21 @@ Design and Implementation of Symbolic Computation Systems (DISCO 90)
A. Miola, (ed) vol 429 of Lecture Notes in Computer Science
Springer-Verlag, pp56-60
+\begin{adjustwidth}{2.5em}{0pt}
+Computer algebra systems of the new generation, like Scratchpad, are
+characterized by a very rich type concept, which models the
+relationship between mathematical domains of computation. To use these
+systems interactively, however, the user should be freed of type
+information. A type inference mechanism determines the appropriate
+function to call. All known models which allow to define a semantics
+for type inference cannot express the rich ``mathematical'' type
+structure, so presently type inference is done heuristically. The
+following paper defines a semantics for a subproblem thereof, namely
+coercion, which is based on rewrite rules. From this definition, and
+efficient coercion algorith for Scratchpad is constructed using graph
+techniques.
+\end{adjustwidth}
+
\bibitem[Fox 68]{Fox68} Fox L.; Parker I B.\\
``Chebyshev Polynomials in Numerical Analysis''\\
Oxford University Press. (1968)
@@ -2114,6 +2538,27 @@ Grove, IL, USA and Oxford, UK, 1992\\
``Limit computation in computer algebra''\\
\verb|algo.inria.fr/seminars/sem92-93/gruntz.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+The automatic computation of limits can be reduced to two main
+sub-problems. The first one is asymptotic comparison where one must
+decide automatically which one of two functions in a specified class
+dominates the other one asymptotically. The second one is asymptotic
+cancellation and is usually exemplified by
+\[e^x[exp(1/x+e^{-x})-exp(1/x)],\quad{}x \leftarrow \infty\]
+
+In this example, if the sum is expanded in powers of $1/x$, the
+expansion always yields $O(x^{-k})$, and this is not enough to
+conclude.
+
+In 1990, J.Shackell found an algorithm that solved both these problems
+for the case of $exp-log$ functions, i.e. functions build by recursive
+application of exponential, logarithm, algebraic extension and field
+operations to one variable and the rational numbers. D. Gruntz and
+G. Gonnet propose a slightly different algorithm for exp-log
+functions. Extensions to larger classes of functions are also
+discussed.
+\end{adjustwidth}
+
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Hache 95]{HL95} Hach\'e, G.; Le Brigand, D.\\
@@ -3059,6 +3504,23 @@ Math. Tables Aids Comput. 10 91--96. (1956)
\subsection{Special Functions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibitem[Corless 05]{Corl05} Corless, Robert M.; Jeffrey, David J.;
+Watt, Stephen M.; Bradford, Russell; Davenport, James H.\\
+``Reasoning about the elementary functions of complex analysis''\\
+\verb|www.csd.uwo.ca/~watt/pub/reprints/2002-amai-reasoning.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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 simplification, 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 theorem proving than
+the original problem of complex-variable analysis.
+\end{adjustwidth}
+
\subsubsection{Exponential Integral $E_1(x)$} %%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Segletes 98]{Se98} Segletes, S.B.\\
@@ -3121,7 +3583,46 @@ J. Symbolic Computation (1990) Vol 9 pp429-455\hfill{}\\
\begin{adjustwidth}{2.5em}{0pt}
This paper analyzes the Euclidean algorithm and some variants of it
for computing the greatest common divisor of two univariate polynomials
-over a finite field.
+over a finite field. The minimum, maximum, and average number of
+arithmetic operations both on polynomials and in the ground field
+are derived.
+\end{adjustwidth}
+
+\bibitem[Naylor 00a]{N00} Naylor, Bill\\
+``Polynomial GCD Using Straight Line Program Representation''\\
+PhD. Thesis, University of Bath, 2000\\
+\verb|www.sci.csd.uwo.ca/~bill/thesis.ps|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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 evalution strategies and algorithms which are
+dependant on these follows, the major algorith which is dependant on
+evaluation and which is central to our theis 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
+structure 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 compare
+their advantages and disadvantages. The final two chapters describe
+some of the results we have obtained from this research and 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.
\end{adjustwidth}
\bibitem[Shoup 93]{ST-PGCD-Sh93} Shoup, Victor\\
@@ -3156,12 +3657,49 @@ The first and second algorithms are deterministic, the third is
probabilistic.
\end{adjustwidth}
+\bibitem[Wang 78]{Wang78} Wang, Paul S.\\
+``An Improved Multivariate Polynomial Factoring Algorithm''\\
+Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
+\verb|www.ams.org/journals/mcom/1978-32-144/S0025-5718-1978-0568284-3/|
+\verb|S0025-5718-1978-0568284-3.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+A new algorithm for factoring multivariate polynomials over the
+integers based on an algorithm by Wang and Rothschild is described.
+The new algorithm has improved strategies for dealing with the known
+problems of the original algorithm, namely, the leading coefficient
+problem, the bad-zero problem and the occurence of extraneous factors.
+It has an algorithm for correctly predetermining leading coefficients
+of the factors. A new and efficient p-adic algorith named EEZ is
+described. Basically it is a linearly convergent variable-by-variable
+parallel construction. The improved algorithm is generally faster and
+requires less store than the original algorithm. Machine examples with
+comparative timing are included.
+\end{adjustwidth}
+
\subsection{Category Theory} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Baez 09]{Baez09} Baez, John C.; Stay, Mike\\
``Physics, Topology, Logic and Computation: A Rosetta Stone''\\
\verb|arxiv.org/pdf/0903.0340v3.pdf|
+\begin{adjustwidth}{2.5em}{0pt}
+In physics, Feynman diagrams are used to reason about quantum
+processes. In the 1980s, it became clear that underlying these
+diagrams is a powerful analogy between quantum physics and
+topology. Namely, a linear operator behaves very much like a
+``cobordism'': a manifold representing spacetime, going between two
+manifolds representing space. But this was just the beginning: simiar
+diagrams can be used to reason about logic, where they represent
+proofs, and computation, where they represent programs. With the rise
+of interest in quantum cryptography and quantum computation, it became
+clear that there is an extensive network of analogies between physics,
+topology, logic and computation. In this expository paper, we make
+some of these analogies precise using the concept of ``closed
+symmetric monodial category''. We assume no prior knowledge of
+category theory, proof theory or computer science.
+\end{adjustwidth}
+
\subsection{Proving Axiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\
@@ -3181,7 +3719,191 @@ students, and engineers interested in formal methods and the
development of zero-fault software.
\end{adjustwidth}
-\bibitem[Hardin 13]{Hard14} Hardin, David S.; McClurg, Jedidiah R.;
+\bibitem[Boulme 00]{BHR00} Boulm\'e, S.; Hardin, T.; Rioboo, R.\\
+``Polymorphic Data Types, Objects, Modules and Functors,: is it too much?''\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Abstraction is a powerful tool for developers and it is offered by
+numerous features such as polymorphism, classes, modules, and
+functors, $\ldots$ A working programmer may be confused by this
+abundance. We develop a computer algebra library which is being
+certificed. Reporting this experience made with a language (Ocaml)
+offering all these features, we argue that the are all needed
+together. We compare several ways of using classes to represent
+algebraic concepts, trying to follow as close as possible mathematical
+specification. Thenwe 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.
+\end{adjustwidth}
+
+\bibitem[Boulme 01]{BHHMR01}
+Boulm\'e, S.; Hardin, T.; Hirschkoff, D.; M\'enissier-Morain, V.; Rioboo, R.\\
+``On the way to certify Computer Algebra Systems''\\
+Calculemus-2001\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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
+mathematical properties to be truly handled at the programming level.
+
+The FOC project, started at the fall of 1997, is aimed to build a
+programming environment for the development of certified symbolic
+computation. The working languages are Coq and Ocaml. In this paper,
+we present first the motivations of the project. We then explain why
+and how our concern for proving properties of programs has led us to
+certain implementation choices in Ocaml. This way, the sources express
+exactly the mathematical dependencies between different structures.
+This may ease the achievement of proofs.
+\end{adjustwidth}
+
+\bibitem[Danielsson 06]{Dani06} Danielsson, Nils Anders; Hughes, John;
+Jansson, Patrik; Gibbons, Jeremy\\
+``Fast and Loose Reasoning is Morally Correct''\\
+ACM POPL'06 January 2005, Charleston, South Carolina, USA
+
+\begin{adjustwidth}{2.5em}{0pt}
+Functional programmers often reason about programs as if they were
+written in a total language, expecting the results to carry over to
+non-toal (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.
+\end{adjustwidth}
+
+\bibitem[Davenport 12]{Davenp12} Davenport, James H.; Bradford, Russell;
+England, Matthew; Wilson, David\\
+``Program Verification in the presence of complex numbers, functions with
+branch cuts etc.''\\
+\verb|arxiv.org/pdf/1212.5417.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In considering the reliability of numerical programs, it is normal to
+``limit our study to the semantics dealing with numerical precision''.
+On the other hand, there is a great deal of work on the reliability of
+programs that essentially ignores the numerics. The thesis of this
+paper is that there is a class of problems that fall between these
+two, which could be described as ``does the low-level arithmeti
+implement the high-level mathematics''. Many of these problems arise
+because mathematics, particularly the mathematics of the complex
+numbers, is more difficult than expected: for example the complex
+function log is not continuous, writing down a program to compute an
+inverse function is more complicated than just solving an equation,
+and many algebraic simplification rules are not universally valid.
+
+The good news is that these problems are {\sl theoretically} capable
+of being solved, and are {\sl practically} close to being solved, but
+not yet solved, in several real-world examples. However, there is
+still a long way to go before implementations match the theoretical
+possibilities.
+\end{adjustwidth}
+
+\bibitem[Dolzmann 97]{Dolz97} Dolzmann, Andreas; Sturm, Thomas\\
+``Guarded Expressions in Practice''\\
+\verb|redlog.dolzmann.de/papers/pdf/MIP-9702.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Computer algebra systems typically drop some degenerate cases when
+evaluating expressions, e.g. $x/x$ becomes 1 dropping the case
+$x=0$. We claim that it is feasible in practice to compute also the
+degenerate cases yielding {\sl guarded expressions}. We work over real
+closed fields but our ideas about handling guarded expressions can be
+easily transferred to other situations. Using formulas as guards
+provides a powerful tool for heuristically reducing the combinatorial
+explosion of cases: equivalent, redundant, tautological, and
+contradictive cases can be detected by simplification and quantifier
+elimination. Our approach allows to simplify the expressions on the
+basis of simplification knowledge on the logical side. The method
+described in this paper is implemented in the REDUCE package GUARDIAN,
+which is freely available on the WWW.
+\end{adjustwidth}
+
+\bibitem[Dos Reis 11]{DR11} Dos Reis, Gabriel; Matthews, David; Li, Yue\\
+``Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants
+and Computer Algebra System Framework''\\
+Calculemus (2011) Springer
+\verb|paradise.caltech.edu/~yli/paper/oa-polyml.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This paper presents an ongoing effort to integrate the Axiom family of
+computer algebra systems with Poly/ML-based proof assistants in the
+same framework. A long term goal is to make a large set of efficient
+implementations of algebraic algorithms available to popular proof
+assistants, and also to bring the power of mechanized formal
+verification to a family of strongly typed computer algebra systems at
+a modest cost. Our approach is based on retargeting the code generator
+of the OpenAxiom compiler to the Poly/ML abstract machine.
+\end{adjustwidth}
+
+\bibitem[Dunstan (a)]{Dunxx} Dunstan, Martin N.\\
+``Adding Larch/Aldor Specifications to Aldor''\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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-checkable and may be used for a variety
+of purposes ranging from compiler optimizations to verification
+condition (VC) generation. In this report we highlight the options
+available and describe the changes which would need to be made to
+the compiler to make use of this technology.
+\end{adjustwidth}
+
+\bibitem[Dunstan 98]{Dun98} Dunstan, Martin; Kelsey, Tom; Linton, Steve;
+Martin, Ursula\\
+``Lightweight Formal Methods For Computer Algebra Systems''\\
+\verb|www.cs.st-andrews.ac.uk/~tom/pub/issac98.pdf|\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Demonstrates 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. There are examples of
+abstract specifications of Axiom primitives.
+\end{adjustwidth}
+
+\bibitem[Dunstan 99a]{Dun99a} Dunstan, MN\\
+``Larch/Aldor - A Larch BISL for AXIOM and Aldor''\\
+PhD Thesis, 1999\\
+\verb|www.cs.st-andrews.uk/files/publications/Dun99.php|\\
+\verb|axiom-portal.newsynthesis.org/refs/articles/mnd-sep99-thesis.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In this thesis we investigate the use of lightweight formal methods
+and verification conditions (VCs) to help improve the reliability of
+components constructed within a computer algebra system. We follow the
+Larch approach to formal methods and have designed a new behavioural
+interface specification language (BISL) for use with Aldor: the
+compiled extension language of Axiom and a fully-featured programming
+language in its own right. We describe our idea of lightweight formal
+methods, present a design for a lightweight verification condition
+generator and review our implementation of a prototype verification
+condition generator for Larch/Aldor.
+\end{adjustwidth}
+
+\bibitem[Dunstan 00]{Dun00} Dunstan, Martin; Kelsey, Tom; Martin, Ursula;
+Linton, Steve\\
+``Formal Methods for Extensions to CAS''\\
+FM 99, Toulouse, France, Sept 20-24, 1999, p1758-1777
+
+\bibitem[Hardin 13]{Hard13} Hardin, David S.; McClurg, Jedidiah R.;
Davis, Jennifer A.\\
``Creating Formally Verified Components for Layered Assurance with an LLVM to ACL2 Translator''\\
\verb|www.jrmcclurg.com/papers/law_2013_paper.pdf|
@@ -3200,9 +3922,122 @@ Greve, David A.; McClurg, Jedidiah R.\\
``Development of a Translator from LLVM to ACL2''\\
\verb|arxiv.org/pdf/1406.1566|
+\begin{adjustwidth}{2.5em}{0pt}
+In our current work a library of formally verified software components
+is to be created, and assembled, using the Low-Level Virtual Machine
+(LLVM) intermediate form, into subsystems whose top-level assurance
+relies on the assurance of the individual components. We have thus
+undertaken a project to build a translator from LLVM to the
+applicative subset of Common Lisp accepted by the ACL2 theorem
+prover. Our translator produces executable ACL2 formal models,
+allowing us to both prove theorems about the translated models as well
+as validate those models by testing. The resulting models can be
+translated and certified without user intervention, even for code with
+loops, thanks to the use of the def::ung macro which allows us to
+defer the question of termination. Initial measurements of concrete
+execution for translated LLVM functions indicate that performance is
+nearly 2.4 million LLVM instructions per second on a typical laptop
+computer. In this paper we overview the translation process and
+illustrate the translator's capabilities by way of a concrete example,
+including both a functional correctness theorem as well as a
+validation test for that example.
+\end{adjustwidth}
+
+\bibitem[Poll 99a]{P99a} Poll, Erik\\
+``The Type System of Axiom''\\
+\verb|www.cs.ru.nl/E.Poll/talks/axiom.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This is a slide deck from a talk on the correspondence between
+Axiom/Aldor types and Logic.
+\end{adjustwidth}
+
+\bibitem[Poll 99]{PT99} Poll, Erik; Thompson, Simon\\
+``The Type System of Aldor''\\
+\verb|www.cs.kent.ac.uk/pubs/1999/874/content.ps|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This paper gives a formal description of -- at least a part of --
+the type system of Aldor, the extension language of the Axiom.
+In the process of doing this a critique of the design of the system
+emerges.
+\end{adjustwidth}
+
+\bibitem[Poll (a)]{PTxx} Poll, Erik; Thompson, Simon\\
+``Adding the axioms to Axiom. Toward a system of automated reasoning in
+Aldor''\\
+\verb|citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This paper examines the proposal of using the type system of Axiom to
+represent a logic, and thus to use the constructions of Axiom to
+handle the logic and represent proofs and propositions, in the same
+way as is done in theorem provers based on type theory such as Nuprl
+or Coq.
+
+The paper shows an interesting way to decorate Axiom with pre- and
+post-conditions.
+
+The Curry-Howard correspondence used is
+\begin{verbatim}
+PROGRAMMING LOGIC
+Type Formula
+Program Proof
+Product/record type (...,...) Conjunction
+Sum/union type \/ Disjunction
+Function type -> Implication
+Dependent function type (x:A) -> B(x) Universal quantifier
+Dependent product type (x:A,B(x)) Existential quantifier
+Empty type Exit Contradictory proposition
+One element type Triv True proposition
+\end{verbatim}
+\end{adjustwidth}
+
+\bibitem[Poll 00]{PT00} Poll, Erik; Thompson, Simon\\
+``Integrating Computer Algebra and Reasoning through the Type System
+of Aldor''\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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-Howeard isomorphism. We give
+a number of example applications of the logi we construct and explain
+a prototype implementation of a modified type-checking system written
+in Haskell.
+\end{adjustwidth}
+
\subsection{Interval Arithmetic} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\bibitem [Lambov 06]{Lambov06} Lambov, Branimir\\
+\bibitem[Boehm 86]{Boe86} Boehm, Hans-J.; Cartwright, Robert; Riggle, Mark;
+O'Donnell, Michael J.\\
+``Exact Real Arithmetic: A Case Study in Higher Order Programming''\\
+\verb|dev.acm.org/pubs/citations/proceedings/lfp/319838/p162-boehm|
+
+\bibitem[Briggs 04]{Bri04} Briggs, Keith\\
+``Exact real arithmetic''\\
+\verb|keithbriggs.info/documents/xr-kent-talk-pp.pdf|
+
+\bibitem[Fateman 94]{Fat94} Fateman, Richard J.; Yan, Tak W.\\
+``Computation with the Extended Rational Numbers and an Application to
+Interval Arithmetic''\\
+\verb|www.cs.berkeley.edu/~fateman/papers/extrat.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Programming languages such as Common Lisp, and virtually every
+computer algebra system (CAS), support exact arbitrary-precision
+integer arithmetic as well as exect rational number computation.
+Several CAS include interval arithmetic directly, but not in the
+extended form indicated here. We explain why changes to the usual
+rational number system to include infinity and ``not-a-number'' may be
+useful, especially to support robust interval computation. We describe
+techniques for implementing these changes.
+\end{adjustwidth}
+
+\bibitem[Lambov 06]{Lambov06} Lambov, Branimir\\
``Interval Arithmetic Using SSE-2''\\
in Lecture Notes in Computer Science, Springer ISBN 978-3-540-85520-0
(2006) pp102-113
@@ -3242,6 +4077,41 @@ This website hosts various ways of visualizing algorithms. The hope is
that these kind of techniques can be applied to Axiom.
\end{adjustwidth}
+\bibitem[Leeuwen]{Leexx} van Leeuwen, Andr\'e M.A.\\
+``Representation of mathematical object in interactive books''\\
+\verb|axiom-wiki.newsynthesis.org/public/refs/articles.html|
+
+\begin{adjustwidth}{2.5em}{0pt}
+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
+{\sl application descriptions}, it is shown how the translation from
+the internal to an external representation and {\sl vice versa} can be
+achieved. Hereby a formalisation of the concept of {\sl 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.
+\end{adjustwidth}
+
+\bibitem[Soiffer 91]{Soif91} Soiffer, Neil Morrell\\
+``The Design of a User Interface for Computer Algebra Systems''\\
+\verb|www.eecs.berkeley.edu/Pubs/TechRpts/1991/CSD-91-626.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This thesis discusses the design and implementation of natural user
+interfaces for Computer Algebra Systems. Such an interface must not
+only display expressions generated by the Computer Algebra System in
+standard mathematical notation, but must also allow easy manipulation
+and entry of expressions in that notation. The user interface should
+also assist in understanding of large expressions that are generated
+by Computer Algebra Systems and should be able to accommodate new
+notational forms.
+\end{adjustwidth}
+
\bibitem[Victor 11]{Vict11} Victor, Bret\\
``Up and Down the Ladder of Abstraction''\\
\verb|worrydream.com/LadderOfAbstraction|
diff --git a/changelog b/changelog
index a888ba0..a0bea18 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140630 tpd src/axiom-website/patches.html 20140630.02.tpd.patch
+20140630 tpd books/bookvolbib.pamphlet add special sections, abstracts
20140630 tpd src/axiom-website/patches.html 20140630.01.tpd.patch
20140630 tpd src/input/wangeez.input Paul Wang's EEZ test polynmials
20140629 tpd src/axiom-website/patches.html 20140629.06.tpd.patch
diff --git a/patch b/patch
index 64b8a48..b577f52 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,5 @@
-src/input/wangeez.input Paul Wang's EEZ test polynmials
+books/bookvolbib.pamphlet add special sections, abstracts
-These are the test polynomials for the EEZ polynomial factorization
-algorithm proposed by Paul Wang in his paper ``An Improved Multivariate
-Polynomial Factoring Algorithm'' \cite{Wang78}
+Special sections have been added as we begin to concentrate the
+research in specific areas. Abstracts are added to improve the
+amount of useful inforamation.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index cc0e387..ba9cae6 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4516,6 +4516,8 @@ books/bookvol10.3 add information to SingleInteger
books/tangle.c improve the debugging output (DEBUG==3)
20140630.01.tpd.patch
src/input/wangeez.input Paul Wang's EEZ test polynmials
+20140630.02.tpd.patch
+books/bookvolbib.pamphlet add special sections, abstracts