next up previous
Next: The object language. Up: CORRECTNESS OF A COMPILER Previous: Introduction

The source language

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 s1(e) and s2(e).

The semantics is given by the formula


where val(e) gives the numerical value of an expression e representing a constant, tex2html_wrap_inline343 gives the value of the variable e in the state vector tex2html_wrap_inline347 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 tex2html_wrap_inline349 is a predicate applicable to expressions, and suppose that for all expressions e we have


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

John McCarthy
Wed Sep 29 13:40:01 PDT 1999