Next: The Limitations of Machines Up: Towards a Mathematical Science Previous: Abstract Syntax of Programming

# Semantics

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 .

Next: The Limitations of Machines Up: Towards a Mathematical Science Previous: Abstract Syntax of Programming

John McCarthy
Tue May 14 13:32:03 PDT 1996