On the Existence of Cook Semantics
Arie de Bruin · SIAM Journal on Computing · 1984
In [SIAM J. Comput., 7 (1978), pp. 70–90] Cook defines the operational semantics of a programming language in the following way; a function is introduced which takes a program R and a state $\sigma $ and yields a possibly infinite row of intermediate states as a result. This row is meant to be the trace resulting from executing program R starting in state $\sigma $. This function is characterized by a number of equations. However it is not immediately clear whether these equations have a solution. In this paper we show for a simple language, the most sophisticated feature of which is that it has parameterless procedures,that the corresponding equations have a unique solution. The techniques used here can also be applied to other languages described in the same way, for instance to the language in Cook’s paper.