next up previous
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 tex2html_wrap_inline707 is the number which t denotes. If tex2html_wrap_inline711 is a number tex2html_wrap_inline713 is the symbolic expression denoting this number. We have the obvious relations

  1. tex2html_wrap_inline715
  2. tex2html_wrap_inline717
  3. tex2html_wrap_inline719

Now we can define the meaning of terms by saying that the value of a term for a state vector tex2html_wrap_inline559 is given by

eqnarray340

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

displaymath368

which gives the value tex2html_wrap_inline723 of the state vector after the ALGOL program tex2html_wrap_inline725 has stopped, given that it was started at its beginning and that the state vector was initially tex2html_wrap_inline559 . 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

displaymath701

giving the effect of operating the machine program p on a machine vector x.

2. An invertible representation tex2html_wrap_inline731 of a state vector as a machine vector is given.

3. A function tex2html_wrap_inline733 translating source programs into machine programs is given.

The correctness of the translation is defined by the equation

displaymath702

It should be noted that tex2html_wrap_inline735 is an abstract function and not a machine program. In order to describe compilers, we need another abstract invertible function, tex2html_wrap_inline737 , 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 tex2html_wrap_inline739 .


next up previous
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