Operational Semantics

Let’s say you have a simple program in Python.

x = 3
y = 1
while(not (x == 1)):
    y = y * x
    x = x - 1

It’s a fairly straightforward program which computes the factorial of a number, 3 in this case.

Suppose you want to prove some facts about this program. You might want to prove, beyond any reasonable doubt, that when the while loop runs with the values of x and y being 3 and 1 respectively, the value of y will be the factorial of 3, that is 6, at then end of execution. You might want to prove that the loop terminates in the first place. If you had another program calculating the factorial of number, you might want to attempt to prove whether the two programs are equivalent or not.

“But Gagan,” you might say, “ we use proofs on mathematical statements, not computer programs.” And you would be right. Well, kinda.

If you were able to rephrase the execution of programs in the form of mathematical statements, you would be able to reason about them the same way you reason about mathematical theorems, wouldn’t you? This is exactly where formal programming language semantics come in.

Semantics can be defined as the rigorous mathematical study of the meaning of computer programs. It is in contrast to syntax, which focuses solely on the grammatical structure of programs. Semantics, on the other hand, provide ways to assign formal, unambiguous meanings to syntactically valid programs. Many different approaches to programming language semantics exist. Majorly, there are 3 classes, namely operational semantics, denotional semantics and axiomatic semantics. In this post, we will limit ourselves to operational semantics, specifically natural/big-step semantics. With the use of a simple example programming language, we will understand the core ideas behind it and how it can be applied practically.

NOTE: This post assumes familiarity with some mathematical concpets such as sets, functions, relations, induction and the use of inference rules. It also includes code snippets in Coq. However, these are just a supplement for interested readers and can be skipped. The Coq file with all the code can be downloaded here.

The Language

In this post we will be using a simple imperative programming language called While. Lots of texts use similar languages; some call it While and others call it Imp. Here, we will use the language While described in the book Semantics with Applications: An Appetizer by Nielson and Nielson. Given below is the syntax for the language in BNF.

As you can see, there are a few metavariables here. n ranges over the syntactic decimal numerals \(Num\), x ranges over the set of variables \(Var\) which contains characters like x, y, z and so on, a ranges over the set of arithmetic expressions \(Aexp\), b ranges over the set of Boolean expressions \(Bexp\) and \(S\) ranges over the set of statements \(Stmt\). Variables can only be assigned arithmetic expressions and Booleans are only used for evaluationg conditional constructs. There is only one looping construct, namely the while loop (not surprising, I know). This syntax can be described in Coq with the use of inductive types.

Inductive aexp : Type :=
  | Num : nat -> aexp
  | Id : string -> aexp
  | Plus : aexp -> aexp -> aexp
  | Mult : aexp -> aexp -> aexp
  | Minus : aexp -> aexp -> aexp.

Inductive bexp : Type :=
  | True : bexp
  | False : bexp
  | Eq : aexp -> aexp -> bexp
  | Leq : aexp -> aexp -> bexp
  | Not : bexp -> bexp
  | And : bexp -> bexp -> bexp.

Inductive stmt : Type :=
  | Assign : string -> aexp -> stmt
  | Skip : stmt
  | Seq : stmt -> stmt -> stmt
  | If : bexp -> stmt -> stmt -> stmt
  | While : bexp -> stmt -> stmt.

The factorial program we saw in the beginning looks like this :-

x := 3; 
y := 1;
while ¬(x = 1) do (y := y * x; x := x - 1) 

States

Before we dive into operational semantics, we need to first look at another essential concept of programming languages, that is, the concept of states. Informally, state refers to the current condition of a system or a process. It contains information that needs to be remembered such as the values of variables. Formally, we can define state as a function from variables to values. For example, if the variables can only be assigned natural numbers, we can define state as follows :-

State is genrally a partial function because not all possible variables will be mapped but for the sake of simplicity, let us consider it to be a total function. A state, say \(s\), defines a value for every variable. The value of a variable \(x\) is written as \(s \; x\). In Coq, we can define it as follows :-

Definition total_map (A : Type) := string -> A.

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

Definition t_update {A : Type} (x : string) 
                    (v : A) (m : total_map A) :=
  fun x' => if String.eqb x x' then v else m x'.

 Notation "x '!->' v ';' m" := (t_update x v m)
                              (at level 100, v at next level, right associativity).

Definition state := total_map nat.

Operational semantics essentially deals with capturing the effect of each statement on the program state. It provides an abstraction of how the program is executed on a machine. It is an abstraction because it does not concern us with the low level details of the machine itself and is subsequently independent of machine architecture and implementation.

There are two categories of operational semantics, namely structural operational semantics (or small-step semantics) and natural semantics (big-step semantics). Roughly speaking, small-step semantics describe each induvidual step of computation while big-step semantics describe how the overall result of executions are obtained. A big-step semantics is often simpler and tends to correspond better to the action of real world interepreters. However, it gives us less control over the details of evaluation and cannot be used to reason about non-terminating programs. In this post, I only cover this approach.

However, before we attempt to understand how statements affect state, let us formalize the evaluation of the arithmetic and Boolean expressions defined above. This is done using semantic functions.

Semantic functions

Semantic functions are a way of mapping syntactic constructs to values. The simplest semantic function we will be using is the function \(\mathcal{N}\) which maps from syntactic numberals to the set of natural numbers.

Let us consider the abstract syntax of numerals to be as follows :-

\(\mathcal{N}\) can be defined compositionally.

Evaluating expressions

We shall define the meaning of arithmetic expressions using a semantic function \(\mathcal{A}\) which takes two arguments - the state and an element of \(Aexp\) and returns a value from \(\mathbb{N}\).

The definition of \(\mathcal{A}\) is given below.

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | Num n => n
  | Id x => st x
  | Plus a1 a2 => (aeval st a1) + (aeval st a2)
  | Mult a1 a2 => (aeval st a1) * (aeval st a2)
  | Minus a1 a2 => (aeval st a1) - (aeval st a2)
  end.

Similarly, we will use the semantic function \(\mathcal{B}\) to define the meaning of Boolean expressions.

Here, \(T\) is the set of truth values \(\mathbf{tt}\) and \(\mathbf{ff}\).

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | True => true
  | False => false
  | Eq a1 a2 => (aeval st a1) =? (aeval st a2)
  | Leq a1 a2 => (aeval st a1) <=? (aeval st a2)
  | Not b1 => negb (beval st b1)
  | And b1 b2 => andb (beval st b1) (beval st b2)
  end.

It is important to note that the all three of the semantic functions described above are total functions and this is a fact that can be proven using structural induction. However, I have not included the proofs for the sake of brevity (I never thought I’d be that guy, but here we are).

Natural Semantics of While

Now that we have a way of evaluating expressions, we can move onto describing the evaluation of statements. This is done a little differently from the evaluation of expressions. The operational approach to semantics defines the behaviour of the program in terms of a transition system. Transition systems are a concept used often in theoretical computer science and consist of states and transitions between them. This transition system will have two different configurations :-

(1) represents the configuration in which a statement S is to be executed from the state \(s\). (2) represents a terminal state with no more statements remaining. To describe how computation takes place, a transition relation will be defined. In natural semantics, we are only concerned with the initial and final states of execution. Transitions will be represented as follows :-

This notation indicates that when the statement S is executed from state s, the system transitions to the state s’. Hence, we can say that the transition relation specifies the relationship between initial and final states. This relation will be defined using rules for each syntactic form that a statement can take. These rules will be described as inference rules. Specifically, each rule will be of the following form :-

Here, \(S_{1}, \; ..., \; S_{n}\) are constituent statements of \(S\). Each rule has a number of premises and one conclusion. It can also have conditions to be fulfilled for the rule to be applied which are written on the right side. Rules can also have no premises and these are called axioms.

In Coq, we will use a relation which results in a proposition (Prop) instead of a function to define the evaluation of statements.

Inductive seval : state -> stmt -> state -> Prop :=

Now, let us go through each statement and look at how the relation can be defined. If you are going through the Coq snippets, observe how the cases of the relation correspond to the inference rules.

Skip

Let us start with the simplest statement, skip. All this statement does is move on to the next statement without affecting the state in any way. The inference rule for it is quite straightforward. There are no premises and it is an axiom.

The case in Coq :-

  | E_Skip : forall (st : state), seval st (Skip) st

Sequence (Seq)

Dealing with sequential statements is slightly more complex than the previous case. Let us consider the statement \(S_{1}; \; S_{2}\) and let the initial state be \(s_{1}\). We will name the state which is the result of executing \(S_{1}\) from \(s_{1}\) as \(s_{2}\). Similarly, let \(s_{3}\) be the state which is the result of executing \(S_{2}\) from \(s_{2}\). Then, we write the rule as follows :-

In Coq, we can write it like this :-

  | E_Seq : forall (st1 st2 st3 : state) (s1 s2 : stmt), 
      seval st1 s1 st2 ->
      seval st2 s2 st3 ->
      seval st1 (Seq s1 s2) st3

Assign

To deal with assignment, we need to introduce another piece of notation :-

This indicates a substitution. It represents the state \(s\) with \(x\) mapped (or remapped) to the expression \(a\). Using substitution, we can state the rule for assignment as an axiom :-

In Coq :-

  | E_Assign : forall (st : state) (a : aexp) (n : nat) (x : string), 
      aeval st a = n -> seval st (Assign x a) (t_update x n st)

If

Two rules are required for the evaluation of if statements - one where the condition is true and another where the condition is false. Based on the value of the condition, the statement to be executed and subsequently the effects on the state are determined. Let \(b\) be the condition. Let \(S_{1}\) be the statement executed when \(b\) is true and \(S_{2}\) otherwise. Let \(s_{2}\) be the state when \(S_{1}\) is executed from \(s_{1}\) and \(s_{3}\) be the state when \(S_{2}\) is executed instead. We can write the inference rules as follows :-

In Coq :-

  | E_IfTrue : forall (st1 st2 : state) (b : bexp) (s1 s2 : stmt), 
      beval st1 b = true ->
      seval st1 s1 st2 ->
      seval st1 (If b s1 s2) st2
  | E_IfFalse : forall (st1 st2 : state) (b : bexp) (s1 s2 : stmt), 
      beval st1 b = false ->
      seval st1 s2 st2 ->
      seval st1 (If b s1 s2) st2

While

Similar to the approach used for if statements, we will require two rules, one for each value of the condition \(b\). When the condition is false, evaluation is quite straightforward because the statement is not executed at and all and hence, there is no state change. The rule is simply the following :-

In Coq :-

  | E_WhileFalse : forall (st : state) (b : bexp) (s : stmt),
      beval st b = false -> 
      seval st (While b s) st

The case for when the condition is true is more complex. We do not know how long the loop runs for, it can even be an infinite loop. What we do know is that the statement will be executed atleast once. Knowing this, we will write the rule somewhat recursively.

After \(S\) is executed, the new state is \(s_{2}\). The final result/state is the result of executing the while loop from this new state \(s_{2}\).

In Coq :-

  | E_WhileTrue : forall (st1 st2 st3: state) (b : bexp) (s : stmt),
      beval st1 b = true ->
      seval st1 s st2 ->
      seval st2 (While b s) st3 ->
      seval st1 (While b s) st3.

Proving facts about programs

Now that we have defined the evaluation of statements, we can use the defined relation in proofs about While programs. Let us consider the program we saw in the beginning. Here it is again in While :-

x := 3; 
y := 1;
while ¬(x = 1) do (y := y * x; x := x - 1) 

In Coq, we can write the AST for this program using the types we defined earlier.

Definition factorial : stmt :=
  Seq (Assign "x" (Num 3))
  (Seq (Assign "y" (Num 1))
  (While (Not(Eq(Id "x")(Num 1)))
  (Seq(Assign "y" (Mult (Id "y") (Id "x")))
  (Assign "x" (Minus (Id "x") (Num 1)))))).

Let us prove that that when the program execution ends, the value of y is 6.

Derivation tree

The proof is a derivation tree built using the rules we defined earlier. Below is the full derivation tree.

Here, \(s_{xy}\) is the initial state where x and y are undefined. As their values change, the state is represented by \(s_{(x - value)(y - value)}\). For example, the final state is \(s_{16}\), where x is 1 and y is 6.

There is quite a bit of to unravel here, so let us construct the derivation tree part by part from the bottom up. The root of the derivation tree will be what we are trying to prove, that is :-

This is of the form \(S_{1}; \; S_{2}\) and hence there is only one rule that could have been used to construct this, namely the rule for sequences. Thus, the root of the derivation tree is constructed as follows :-

Here, \(T1\) is a derivation tree with root.

The assignment statement uses the axiom for assignment.

Once again, \(T1\) is a sequence and hence the rule for sequences is used to construct it.

\(T2\) is a derivation tree with root

Since this is a while loop, there are two possible rules that can be applied. In the state \(s_{31}\), the value of x is 3. Hence, the condition \(\neg (x \; = \; 1)\) is true. Thus, we will use the rule for when the condition is true. The derivation looks like this :-

Based on the rule, the root of \(T3\) is

The root of \(T4\) is again the while loop but with a different state.

The full derivation tree for \(T3\) can be constructed by first using the rule for sequences and then the axiom for assignment.

\(T4\) again has a while loop as its root. Analyzing the state, we can determine that the condition is true and the appropriate rule is used.

\(T5\) is constructed similar to \(T3\).

Once again, \(T6\) has a while loop as its root. But this time, the condition is false and the relevant axiom is used. Thus. \(T6\) is simply

Putting it all together gives us the full derivation tree we saw at the beginning of this section.

We can construct a proof for the same in Coq as well. In the statement of the theorem, we have to explicitly mention the state we expect the program to terminate in. A little bit of automation has also been used to avoid having to manually specify the state at each step.

Theorem factorial_3 : forall st : state, 
  seval (st) factorial ("x" !-> 1; "y" !-> 6; "x" !-> 2; "y" !-> 3; "y" !-> 1; "x" !-> 3; st).
Proof.
  intros st. eapply E_Seq.
  - apply E_Assign. reflexivity.
  - eapply E_Seq.
    + apply E_Assign. reflexivity.
    + eapply E_WhileTrue.
      * reflexivity.
      * eapply E_Seq.
        -- apply E_Assign. reflexivity.
        -- apply E_Assign. reflexivity.
      * eapply E_WhileTrue.
        -- reflexivity.
        -- eapply E_Seq.
          ++ apply E_Assign. reflexivity.
          ++ apply E_Assign. reflexivity.
        -- eapply E_WhileFalse. reflexivity. 
Qed.

Proving program equivalences

Another thing operational semantics can be used for is proving that two programs are equivalent. For example, consider the following two programs.

x := 1

skip; x := 1

Are these two programs equivalent? Intuitively, it seems like they are. Both assign the value 1 to x and that’s it. Formally, we can use the transition system we defined to prove that the two programs are semantically equivalent. Two programs are semantically equivalent if, for any given state, the first one terminating in a certain state implies that the second terminates in the same state as well and vice-versa.

Definition sequiv (s1 s2 : stmt) : Prop :=
  forall (st1 st2 : state), seval st1 s1 st2 <-> seval st1 s2 st2.

The proof of this theorem has two directions.

Let us proceed with the first direction. Let us construct the only possible derivation tree of the second program.

We can see that the execution of the skip statement leads to an intermediate state which is then used to execute the second statement which yields the final state. However, from the axiom for evaluating the skip statement, we know that it does not cause any state change. Thus, \(s_{intermediate} = s\). From this, we can conclude

But from our hypothesis, we know that \(\langle \; S, \; s \; \rangle \; \rightarrow \; s'\) and thus, \(s_{final} = s'\). We can rewrite the root of the tree which is the conclusion we are trying to show as follows :-

This completes our proof of the first direction.

For the second direction, let us start with our hypothesis as the root and then construct the only possible derivation tree.

As you can see, this tree clearly derives the conclusion we are trying to show. Thus, we have proved the second direction as well.

The proof in Coq :-

Theorem skip_stmt : forall (s : stmt), sequiv s (Seq Skip s).
Proof. 
  intros s st st'. split; intros H.
  - eapply E_Seq.
    + apply E_Skip.
    + assumption.
  - inversion H. subst. inversion H3. subst. assumption.
Qed.

Next steps

Semantics is a very deep topic and we have only scratched the surface. There are many more kinds of semantics that we haven’t even touched upon. As previously mentioned, there is another style of operational semantics call structural operational semantics which can be used to do a few things you can’t with natural semantics. There are also the other categories, namely denotional and axiomatic semantics. There are many books which cover these topics. My recommendation would be Semantics with Applications: An Appetizer by Nielson and Nielson. A free alternative is Concrete Semantics by Nipkow and Klein which covers these topics using Isabelle/HOL, which is another proof assistant. For readers who wish to learn Coq, the first volume of Software Foundations is the best resource out there. The second volume also covers most of the content of this post.

That brings us to end of this post. I hope it was both informative and enjoyable. If you have any questions or suggestions, feel free to reach out to me!