The abstract analytic syntax of the source expressions is given by the table:

which asserts that the expressions comprise constants, variables and binary
sums, that the predicates *isconst*, *isvar*, and *issum* enable one to
classify each expression and that each sum *e* has summands *s*1(*e*) and
*s*2(*e*).

The semantics is given by the formula

where val(*e*) gives the numerical value of an expression *e* representing
a constant, gives the value of the variable *e* in the state
vector and + is some binary operation. (It is natural to regard +
as an operation that resembles addition of real numbers, but our
results do not depend on this).

For our present purposes we do not have to give a synthetic syntax for the source language expressions since both the interpreter and the compiler use only the analytic syntax. However, we shall need the following induction principle for expressions:

Suppose is a predicate applicable to expressions, and suppose that
for all expressions *e* we have

Then we may conclude that is true for all expressions *e*.

Wed Sep 29 13:40:01 PDT 1999