  Algorithms like those for differentiating functional expressions manipulate
the syntactic structure of mathematical expressions in a mathematically
meaningful way. A formalization of such an algorithm should include a
specification of its computational behavior, a specification of its
mathematical meaning, and a mechanism for applying the algorithm to actual
expressions. Achieving these goals requires the ability to integrate reasoning
about the syntax of the expressions with reasoning about what the expressions
mean. A syntax framework is a mathematical structure that is an abstract model
for a syntax reasoning system. It contains a mapping of expressions to
syntactic values that represent the syntactic structures of the expressions; a
language for reasoning about syntactic values; a quotation mechanism to refer
to the syntactic value of an expression; and an evaluation mechanism to refer
to the value of the expression represented by a syntactic value. We present and
compare two approaches, based on instances of a syntax framework, to formalize
a syntax-based mathematical algorithm in a formal theory T. In the first
approach the syntactic values for the expressions manipulated by the algorithm
are members of an inductive type in T, but quotation and evaluation are
functions defined in the metatheory of T. In the second approach every
expression in T is represented by a syntactic value, and quotation and
evaluation are operators in T itself.
