Index

Relational Semantics

The idea behind relational semantics is that we define rules for a transition relation which allows each phrase to evaluate to its result in one step. This is in contrast to structured transition semantics where the same evaluation would require far more transitions (except for atomic phrases). We develop a relational semantics for the language IMP as an example.

Relational Semantics for IMP

Our transition relation for IMP is ⇒⊆(Phrases×Memories)×Results. In the case of expressions, the set Results will be all elements of the form (c,M) where c is a constant and M is a memory. For programs, the set Results will be the set of memories. We can now define the terminal transition system (Γ,⇒,T) where Γ= Phrases×Memories∪T, T=Results, and γ⇒γ' implies that γ'∈Γ.

Expressions
Constant c,M ⇒ c,M
Variable xi,M ⇒ ci,M where M=c0,c1,...
Composite e1,M ⇒ n1,M' e2,M' ⇒ n2,M''
--------------------------
     e1 op e2,M ⇒ n3,M''      where n3=n1 op n2
Programs
Null null,M ⇒ M
Assignment   e,M ⇒ n,M'
-----------------
xi:=e,M ⇒ M'{n/i} Here M'{n/i} means memory location i contains value n.
Sequence p1,M ⇒ M' p2,M' ⇒ M''
----------------------
   (p1;p2),M ⇒ M''
Conditional
  1.   b,M ⇒ true,M' p1,M' ⇒ M''
    ----------------------------
    if b then p1 else p2,M ⇒ M''
  2.   b,M ⇒ false,M' p2,M' ⇒ M''
    ----------------------------
    if b then p1 else p2,M ⇒ M''
Iteration
  1. b,M ⇒ true,M' p,M' ⇒ M'' while b do p,M'' ⇒ M'''
    --------------------------------------------------
               while b do p,M ⇒ M'''
  2.    b,M ⇒ false,M'
    --------------------
    while b do p,M ⇒ M'

Proof of Phrase Equivalence

Two programs, p1 and p2, can be defined as equivalent, p1≈p2, if for all memories, M, M': 

	
p1,M ⇒ M' ⇔ p2,M ⇒ M'

As an example of this, here is the proof that p1;(p2;p3)≈(p1;p2);p3:

Assume that p1;(p2;p3),M ⇒ M''', then

  1. p1,M ⇒ M' by Sequence on assumption
  2. (p2;p3),M' ⇒ M'' by Sequence on assumption
  3. p2,M' ⇒ M'' by Sequence on (2)
  4. p3,M'' ⇒ M''' by Sequence on (2)
  5. (p1;p2),M ⇒ M'' by Sequence on (1) and (3)
  6. (p1;p2);p3,M ⇒ M''' by Sequence on (5) and (4)

So p1;(p2;p3),M ⇒ M''' implies (p1;p2);p3,M ⇒ M'''. Working the other way we can assume that (p1;p2);p3,M ⇒ M''', then deduce that p1;(p2;p3),M ⇒ M''' as follows:

  1. (p1;p2),M ⇒ M'' by Sequence on assumption
  2. p3,M'' ⇒ M''' by Sequence on assumption
  3. p1,M ⇒ M' by Sequence on (1)
  4. p2,M' ⇒ M'' by Sequence on (1)
  5. (p2;p3),M' ⇒ M''' by Sequence on (4) and (2)
  6. p1;(p2;p3),M ⇒ M''' by Sequence on (3) and (5)

Implementation

What follows is a simple interpreter for relational semantics definitions and a program for the semantics of IMP. This interpreter allows us to execute the semantics. The code makes use of details which are specific to Barry's Prolog and they will not work on other systems.

First comes the code for the interpreter. 

	
:- set_prolog_flag(collapse_multiple_minuses, on).

:- op(0, xfx, (:)).
:- op(1150, xfx, (:)).
:- op(0, xfx, (when)).
:- op(1140, xfx, (when)).
:- op(0, xfx, (---)).
:- op(1130, xfx, (---)).
:- op(0, fx, (---)).
:- op(1130, fx, (---)).

%%%
%%% demo(+Goal)
%%%
%%% Succeeds if Goal can be demonstrated.
%%%
demo('{}'(G)) :- 
	call(G).

demo((G1, G2)) :- 
	demo(G1), 
	demo(G2).

demo(Goal) :-
	(Rule: --- Goal when Whens), 
	call(Whens).

demo(Goal) :-
	(Rule: Hypothesis --- Goal when Whens), 
	call(Whens),
	demo(Hypothesis).

The semantics needs the following miscellaneous definitions. 

	
%%%
%%% +S1 => +S2 
%%%
%%% Succeeds if we can transition from S1 to S2.
%%%
:- op(0, xfx, (=>)).
:- op(700, xfx, (=>)).

%%%
%%% imp_constant(+C)
%%%
%%% Succeeds when C is an IMP constant (Boolean or integer).
%%%
imp_constant(true) :- !.
imp_constant(false) :- !.
imp_constant(C) :- integer(C).

%%%
%%% imp_variable(+X)
%%%
%%% Succeeds when X is an IMP variable.
%%%
imp_variable(var(X)) :- integer(X), X >= 0.

%%%
%%% imp_arith_operation(+Op)
%%%
%%% Succeeds when Op is an IMP binary arithmetic operation.
%%%
imp_arith_operation(Op) :- once(member(Op, [+,-,/,*])).

%%%
%%% imp_bool_operation(+Op)
%%%
%%% Succeeds when Op is an IMP binary Boolean operation.
%%%
imp_bool_operation(Op) :- once(member(Op, [<,>,=])).

%%%
%%% imp_composite(+E)
%%%
%%% Succeeds when E is an IMP composite.
%%%
imp_composite(E) :- compound(E).


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

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

Now the semantics proper. As can be seen this is almost the same format as semantics given earlier. The functor s/2 is used to encode states. 

	
%%%
%%% Relational Semantics for IMP.
%%%
constant: ------------------
           s(C,M) => s(C,M)   when imp_constant(C).

variable: ------------------
           s(X,M) => s(C,M)   when imp_variable(X), imp_mem_get(M, X, C).



composite_1:   s(E1,M1) => s(N1,M2),  s(E2,M2)=> s(N2,M3),  {E3 =.. [Op,N1,N2], N3 is E3}
            --------------------------------------------------------------------------
                             s(E,M1) => s(N3,M3)                                       when imp_composite(E), E =.. [Op,E1,E2], imp_arith_operation(Op).


composite_2:   s(E1,M1) => s(N1,M2),  s(E2,M2)=> s(N2,M3),  
               {E3 =.. [Op,N1,N2], (call(E3) -> N3 = true ; N3 = false)}
            -------------------------------------------------------------
                             s(E,M1) => s(N3,M3)                           when  imp_composite(E), E =.. [Op,E1,E2], imp_bool_operation(Op).


null: -------------------
       s(null,M) => s(M)  when true.

assignment: s(E,M1) => s(N,M2), {imp_mem_put(M2, X, N, M3)}
           -----------------------------------------------
                  s(assign(X, E), M1) => s(M3)              when imp_variable(X).


sequence: s(P1, M1) => s(M2), s(P2, M2) => s(M3)
          --------------------------------------
                   s((P1;P2), M1) => s(M3)        when true.


conditional_1: s(B,M1) => s(true,M2), s(P1, M2) => s(M3)
              -------------------------------------------
                    s(if(B, P1, P2), M1) => s(M3)        when true.

conditional_2: s(B,M1) => s(false,M2), s(P2, M2) => s(M3)
              -------------------------------------------
                    s(if(B, P1, P2), M1) => s(M3)        when true.


iteration_1: s(B,M1) => s(true,M2), s(P,M2) => s(M3), s(while(B, P), M3) => s(M4)
             ------------------------------------------------------------------
                           s(while(B, P), M1) => s(M4)                             when true.

iteration_2:   s(B,M1) => s(false,M2)
             --------------------------
              s(while(B, P), M1) => s(M2)  when true.

Finally some test code. 

	
imp_execute(Program) :-
	demo((s(Program, []) => Result)),
	format('~p evaluates to ~p~n', [Program, Result]),
	!.
imp_execute(Program) :-
	format('~p fails to evaluate~n', [Program]).

test :-
	imp_execute(1), % Constant
	imp_execute(true), % Constant
	imp_execute(var(1)), % Variable
	imp_execute(1+2), % Composite 1
	imp_execute(1<2), % Composite 2
	imp_execute(null), % Null
	imp_execute((assign(var(1), 1); assign(var(2), 2))), % Assignment, Sequence
	imp_execute(if(true, assign(var(1), true), assign(var(1), false))), % Conditional 1
	imp_execute(if(false, assign(var(1), false), assign(var(1), true))), % Conditional 1
	imp_execute(while(2<1, assign(var(1),5))), % Iteration 2
	imp_execute((assign(var(1), 0); while(var(1) > 0, (assign(var(2), var(2)+1); assign(var(1), var(1)-2))))). % Iteration 1

References

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

Index

Copyright © 2014 Barry Watson. All rights reserved.