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

A value stack S∈Phrases^*
A memory M∈Constants^∞
A control stack C∈(Phrases∪Operations∪{if, assign, while})^*

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

The memory M=c₀,c₁,c₂,... contains the current values of the variables x₀,x₁,x₂,.... 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, x_i:C⟩⇒⟨c_i:S, M, C⟩` where `M=c₀,c₁,c₂,...`
Composite	`⟨S, M, (e₁ op e₂):C⟩⇒⟨S, M, e₁:e₂:op:C⟩`
Operator	`⟨n₁:n₂:S, M, op:C⟩⇒⟨n₃:S, M, C⟩` where `n₃` is the evaluation of `n₁ op n₂`

Rules for programs

Null	`⟨S, M, null:C⟩⇒⟨S, M, C⟩`
Assignment	`⟨S, M, (X_i:=e):C⟩⇒⟨i:S, M, e:assign:C⟩`
Sequence	`⟨S, M, (p₁;p₂):C⟩⇒⟨S, M, p₁:p₂:C⟩`
Conditional	`⟨S, M, (if b then p₁ else p₂):C⟩⇒⟨p₁:p₂: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:p₁:p₂:S, M, if:C⟩⇒⟨S, M, p₁:C⟩` `⟨false:p₁:p₂:S, M, if:C⟩⇒⟨S, M, p₂: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 i^th memory value is set to n.

Notes

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.

Implementation

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) :-
	number(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
	smc_constant(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
	compound(E),
	E =.. [Op, E1, E2],
	member(Op, [+, -, *, /, =, <, >]).
([N2, N1|S], M, [Op|C]) => (S, M, [Value|C]) :-                       % Operator
	number(N1),
	number(N2),
	member(Op, [+, -, *, /]),
	Expression =.. [Op, N1, N2],
	Value is Expression.
([N2, N1|S], M, [Op|C]) => ([Value|S], M, C) :-                       % Operator
	number(N1),
	number(N2),
	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_constant(N),
	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, [])).

References

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