Frameworks for Reasoning about Syntax that Utilize Quotation and
Evaluation
Abstract
It is often useful, if not necessary, to reason about the syntactic structure
of an expression in an interpreted language (i.e., a language with a
semantics). This paper introduces a mathematical structure called a syntax
framework that is intended to be an abstract model of a system for reasoning
about the syntax of an interpreted language. Like many concrete systems for
reasoning about syntax, a syntax framework contains a mapping of expressions in
the interpreted language to syntactic values that represent the syntactic
structures of the expressions; a language for reasoning about the syntactic
values; a mechanism called quotation to refer to the syntactic value of an
expression; and a mechanism called evaluation to refer to the value of the
expression represented by a syntactic value. A syntax framework provides a
basis for integrating reasoning about the syntax of the expressions with
reasoning about what the expressions mean. The notion of a syntax framework is
used to discuss how quotation and evaluation can be built into a language and
to define what quasiquotation is. Several examples of syntax frameworks are
presented.