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

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.

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)