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.
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.
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. 
denotes the value of the contents of register
x in machine state 
.
2. 
denotes the state vector that is
obtained from the state vector by changing the
contents of register x to 
leaving the other registers unaffected.
These functions satisfy the following relations:
Now we can define the semantics of the object language by
which gives the state vector that results from executing an instruction and
which gives the state vector that results from executing the program p
with state vector .
The following lemma is easily proved.
