# 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.