SMC Machine

We can use a terminal transition system to describe the semantics of a programming language. Here we show how an interpreter for the language IMP can be given without writing this interpreter in another language. This is done by designing the interpreter as an abstract machine which is defined as a terminal transition system.

SMC Machine Configuration

The state of the machine consists of three components

The value stack will contain the results of evaluation and phrases which have been deferred.

The memory M=c0,c1,c2,... contains the current values of the variables x0,x1,x2,.... The memory has been made infinite to avoid placing a bound on the number of variables.

The control stack holds phrases whose execution has not begun.

SMC Machine Transition Rules

The transition relation between configurations is . It is defined by the rules below. In these rules the concatenation operator (:) is used to build stacks. The empty stack is ε and X:ε=X is a stack of one element.

Rules for expressions

Constant⟨S, M, c:C⟩⇒⟨c:S, M, C⟩
Variable⟨S, M, xi:C⟩⇒⟨ci:S, M, C⟩ where M=c0,c1,c2,...
Composite⟨S, M, (e1 op e2):C⟩⇒⟨S, M, e1:e2:op:C⟩
Operator⟨n1:n2:S, M, op:C⟩⇒⟨n3:S, M, C⟩ where n3 is the evaluation of n1 op n2

Rules for programs

Null⟨S, M, null:C⟩⇒⟨S, M, C⟩
Assignment⟨S, M, (Xi:=e):C⟩⇒⟨i:S, M, e:assign:C⟩
Sequence⟨S, M, (p1;p2):C⟩⇒⟨S, M, p1:p2:C⟩
Conditional⟨S, M, (if b then p1 else p2):C⟩⇒⟨p1:p2:S, M, b:if:C⟩
Iteration⟨S, M, (while b do p):C⟩⇒⟨b:p:S, M, b:while:C⟩

Rules for assign, if and while

Assign⟨n:i:s:S, M, assign:C⟩⇒⟨S, M{n/i}, C⟩
If⟨true:p1:p2:S, M, if:C⟩⇒⟨S, M, p1:C⟩
⟨false:p1:p2:S, M, if:C⟩⇒⟨S, M, p2:C⟩
While⟨true:b:p:S, M, while:C⟩⇒⟨S, M, p:(while b do p):C⟩
⟨false:b:p:S, M, while:C⟩⇒⟨S, M, C⟩

The notation M{n/i} means the ith memory value is set to n.


We've defined a set of configurations and the transition relation but we've not defined the set of terminal configurations. We can define this set to be all the configurations of the form ⟨ε, M, ε⟩. Provided the program p terminates, it will always be the case that ⟨ε, M, p⟩⇒*⟨ε, M, ε⟩.

The SMC transition system is monogenic.

We can define an evaluation function, EVAL:Programs→(Memories→Memories), which is a partial function over Memories: EVAL(p)(M) = M' if ⟨ε, M, p;⟩⇒*⟨ε, M', ε⟩, otherwise the result is undefined. The fact that the transition system is monogenic means that this is a proper function.


The following is an implementation of the SMC machine written in Barry's Prolog. It should run on any ISO compliant Prolog system.

%%% Configure the operators.
:- op(0, xfx, =>).
:- op(800, xfx, =>).

%%% smc_constant(+C)
%%% Succeeds if C is an SMC constant
smc_constant(C) :-

%%% smc_mem_get(+M, +A, -V)
%%% V is the value stored in memory M at address A.
smc_mem_get(M, A, V) :-
	(member(A-V, M)
	V = 0),

%%% smc_mem_put(+Min, +A, +V, Mout)
%%% Store the value V in memory Min at address A giving Mout.
smc_mem_put(Min, A, V, Mout) :-
	(del(A-_, Min, Mmid)
	Mmid = Min),
	Mout = [A-V|Mmid].

%%% +State1 => -State2
%%% '=>'/2 is the transition relation for the SMC machine.
(S, M, [Constant|C]) => ([Constant|S], M, C) :-                       % Constant
(S, M, [var(I)|C]) => ([Value|S], M, C) :-                            % Variable
	smc_mem_get(M, var(I), Value).
(S, M, [E|C]) => (S, M, [E1, E2, Op|C]) :-                            % Composite
	E =.. [Op, E1, E2],
	member(Op, [+, -, *, /, =, <, >]).
([N2, N1|S], M, [Op|C]) => (S, M, [Value|C]) :-                       % Operator
	member(Op, [+, -, *, /]),
	Expression =.. [Op, N1, N2],
	Value is Expression.
([N2, N1|S], M, [Op|C]) => ([Value|S], M, C) :-                       % Operator
	member(Op, [=, <, >]),
	Call =.. [Op, N1, N2],
	(call(Call) -> Value = true ; Value = false).
(S, M, [null|C]) => (S, M, C).                                        % Null
(S, M, [assign(var(I), E)|C]) => ([var(I)|S], M, [E, assign|C]).      % Assignment
(S, M, [(P1;P2)|C]) => (S, M, [P1,P2|C]).                             % Sequence
(S, M, [if(B,P1,P2)|C]) => ([P1,P2|S], M, [B, if|C]).                 % Conditional
(S, M, [while(B,P1)|C]) => ([B, P1|S], M, [B, while|C]).              % Iteration
([N,var(I)|S], M1, [assign|C]) => (S, M2, C) :-                       % Assign
	smc_mem_put(M1, var(I), N, M2).
([true, P1, _|S], M, [if|C]) => (S, M, [P1|C]).                       % If
([false, _, P2|S], M, [if|C]) => (S, M, [P2|C]).                      % If
([true, B, P1|S], M, [while|C]) => (S, M, [P1,while(B, P1)|C]).       % While
([false, _, _|S], M, [while|C]) => (S, M, C).                         % While

%%% run_smc(+S1, -S2)
%%% S1 =>* S2
run_smc(Input, Output) :-
	Input => Mid,
	run_smc(Mid, Output).
run_smc(Output, Output).

%%% test_smc(+P, -M)
%%% M is the result (memory) of executing program P.
%%% Example:
%%% | ?- test_smc(assign(var(1), 3+4), M).
%%% M = [var(1)-7] ? 
%%% % yes
%%% test_smc(if(2<3, assign(var(1), 1), assign(var(1), 0)), M).
%%% test_smc(while(var(1)<5, (assign(var(1), var(1)+1); assign(var(2), var(2)+2))), M).
test_smc(Program, Memory) :-
	run_smc(([], [], [Program]), ([], Memory, [])).


R. Burstall. Language Semantics and Implementation. Course Notes. 1994.