The analytic syntactic functions can be used to define
the semantics of a programming language. In order to
define the meaning of the arithmetic terms described
above, we need two more functions of a semantic
nature, one analytic and one synthetic. If the term t
is a constant then is the number which t denotes.
If
is a number
is the symbolic expression
denoting this number. We have the obvious relations
Now we can define the meaning of terms by saying
that the value of a term for a state vector is given by
We can go farther and describe the meaning of a program in a programming language as follows: The meaning of a program is defined by its effect on the state vector. Admittedly, this definition will have to be elaborated to take input and output into account.
In the case of ALGOL we should have a function
which gives the value of the state
vector after the ALGOL program
has stopped, given that it was
started at its beginning and that the state vector was initially
. We expect to publish elsewhere a recursive description of the
meaning of a small subset of ALGOL.
Translation rules can also be described formally. Namely,
1. A machine is described by a function
giving the effect of operating the machine program p on a machine vector x.
2. An invertible representation of a
state vector as a machine vector is given.
3. A function translating source
programs into machine programs is given.
The correctness of the translation is defined by the equation
It should be noted that is an abstract function
and not a machine program. In order to describe
compilers, we need another abstract invertible function,
, which gives a representation of the source
program in the machine memory ready to be translated.
A compiler is then a machine program such that
.