Towards Specifying Symbolic Computation
Jacques Carette and William M. Farmer
2019
Abstract
Many interesting and useful symbolic computation algorithms manipulate
mathematical expressions in mathematically meaningful ways. Although
these algorithms are commonplace in computer algebra systems, they can
be surprisingly difficult to specify in a formal logic since they
involve an interplay of syntax and semantics. In this paper we
discuss several examples of syntax-based mathematical algorithms, and
we show how to specify them in a formal logic with undefinedness,
quotation, and evaluation.
Keywords
Symbolic computation, computer algebra systems, reasoning about
syntax, undefinedness, quotation and evaluation.