next up previous
Next: The compiler Up: CORRECTNESS OF A COMPILER Previous: The source language

The object language.

We must give both the analytic and synthetic syntaxes for the object language because the interpreter defining its semantics uses the analytic syntax and the compiler uses the synthetic syntax. We may write the analytic and synthetic syntaxes for instructions in the following table.

displaymath357

A program is a list of instructions and null(p) asserts that p is the null list. If the program p is not null then first(p) gives the first instruction and rest(p) gives the list of remaining instructions. We shall use the operation p1 * p2 to denote the program obtained by appending p2 onto the end of p1. Since we have only one level of list we can identify a single instruction with a program that has just one instruction.

The synthetic and analytic syntaxes of instructions are related by the following.

displaymath71

The * operation is associative. (The somewhat awkward form of these relations comes from having a general concatenation operation rather than just an operation that prefixes a single instruction onto a program.)

A state vector for a machine gives, for each register in the machine, its contents. We include the accumulator denoted by ac as a register. There are two functions of state vectors as introduced in [3], namely

1. tex2html_wrap_inline377 denotes the value of the contents of register x in machine state tex2html_wrap_inline381 .

2. tex2html_wrap_inline383 denotes the state vector that is obtained from the state vector tex2html_wrap_inline381 by changing the contents of register x to tex2html_wrap_inline389 leaving the other registers unaffected.

These functions satisfy the following relations:

displaymath391

displaymath395

displaymath395

Now we can define the semantics of the object language by

displaymath86

which gives the state vector that results from executing an instruction and

displaymath397

which gives the state vector that results from executing the program p with state vector tex2html_wrap_inline381 .

The following lemma is easily proved.

displaymath403


next up previous
Next: The compiler Up: CORRECTNESS OF A COMPILER Previous: The source language

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