Computer algebra
Software
Commercial
The “big three” commercial CAS:
- Mathematica
- Maple
- Char et al, 1983: The design of Maple (doi)
- Magma : mostly abstract algebra
- Bosma, Cannon, Playoust, 1997: The Magma algebra system I: User language
(doi, pdf)
- Uses universal algebra and category theory (in idiosyncratic terminology) to create a type system for computer algebra
- No sequel to this paper, title notwithstanding
- Bibliography of Magma papers
- Bosma, Cannon, Playoust, 1997: The Magma algebra system I: User language
(doi, pdf)
Open source
- Maxima (Lisp): descended from Macsyma, the first general-purpose CAS
- Axiom (Lisp): descended from IBM’s Scratchpad I and II
- SymPy (Python)
- SageMath (Python): mostly a frontend to other CAS
For specialized software for groups, see the page on computational group theory.
Programming languages
Term rewriting is a model of computation and term rewriting languages (LtU ) are closely related to computer algebra.
- OBJ : Rewriting system based on essentially algebraic theories
- Pure : Practical, dynamically typed rewriting language
Literature
General
- Geddes et al, 1992: Algorithms for Computer Algebra
- Wester, ed., 1999: Computer Algebra: A Practical Guide (toc )
Theoretical limits
Richardson’s theorem says that the fundamental problem of computer algebra—determining whether two expressions in a single real variable are equal—is undecidable.
- Poonen, 2014: Undecidable problems: a sampler (arxiv), Sec. 9: Analysis
- Matiyasevich, 1993: Hilbert’s 10th Problem, Sec 9.2: Equations,
inequalities, and identities in real variables
- Proves a version of Richardson’s theorem by reduction from Hilbert’s 10th problem
Design
- Fateman, 1990: Advances and trends in the design and construction of algebraic manipulation systems (doi, pdf)
- Watt, 2009: On the future of computer algebra systems at the threshold of 2010
(pdf)
- Watt, 2007: What happened to languages for symbolic mathematical computation? (pdf)
- Norvig, 1992: Paradigms of Artificial Intelligence Programming: Case Studies
in Common Lisp
- Ch. 8-9: Ruled-based simplification
- Ch. 15 Canonical forms & Ch. 20: Unification
Term rewriting
A long list of surveys on term rewriting, compiled by Nachum Dershowtiz and Laurent Vigneron.
Books:
- Wechler, 1992: Universal Algebra for Computer Science, Ch. 2: Reductions
- Mitchell, 1996: Foundations of Programming Languages, Sec 3.7: Rewrite systems
- Baader & Nipkow, 1999: Term Rewriting and All That
- Terese, 2003: Terming Rewriting Systems
- “Terese” is a pseudonym of the editors, Marc Bezem, Jan Willem Klop, and Roel de Vrijer, and other contributing authors
- “Lite version” is online
Papers:
- Winkler, 1989: Knuth-Bendix procedure and Buchberger algorithm: a synthesis (doi)
Unification and matching
(For higher-order unification, see lambda calculus)
Unification:
- Baader & Nipkow, 1999, Ch 4. Equational problems
- Baader & Snyder, 2001: Unification theory, Ch. 8 in Handbook of Automated Reasoning (doi)
- Knight, 1989: Unification: A multidisciplinary survey (doi)
- Goguen, 1989: What is unification? A categorical view of substitution, equation, and solution (pdf)
- Baader & Ghilardi, 2010: Unification in modal and description logics (doi, pdf)
Pattern matching (considered as special case of unification, see Baader & Nipkow, 1999, p. 78):
- Krebber, 2017, master’s thesis: Non-linear associative-commutative many-to-one pattern matching with sequence variables (arxiv)
Data structures
- Geddes et al, 1992: Ch. 3: Normal forms and algebraic representations
- Monagan & Pierce, 2014: The design of Maple’s sum-of-products and POLY data structures for representing mathematical objects (doi)