5 – Semantics of the While language

Mark Armstrong, PhD Candidate, McMaster University

Fall, 2019

2 Introduction to operational semantics

An operational semantics describes the meaning of programs in terms of computation steps on some abstract machine.

In particular, our “abstract machine” for the While language will be a relation.

We consider two different semantics, each consisting of two relations.

Small-step, or reduction, semantics,
- which defines two reduction relations
  - _⟶_ : Expr × Env × State → Expr × Env × State
  - _⟶_ : Stmt × Env × State → Stmt × Env × State
- These relations describe individual computation steps.
Big-step, or evaluation, semantics,
- which defines two evaluation relations
  - _⇓_ : Expr × Env × State → Value
    - where Value is the set of values of the appropriate types
  - _⇓_ : Stmt × Env × State → Env × State
- These relations describe the final results of computation.

2.1 Why two different semantics?

The two semantics we present, big-step and small-step operational semantics, each serve a different purpose.

The small-step semantics precisely describe the order in which expressions/statements are computed.
- For instance, in the case of a binary operator, small-step semantics describe which operand is computed first.
The big-step semantics provide a simpler view of computation, in that there are fewer rules.
- Sometimes big-step semantics are called “natural” semantics.

Neither approach is “correct” or “incorrect”; they are complementary!

2.2 Syntactic correctness

We assume in these slides that every program we consider is correct, meaning it is

syntactically correct, and in particular that they are
- well typed,
- well scoped, and
- every variable is declared before it is used.

That is, we assume these syntactic/static semantic rules have been enforced

by a context-free grammar
- (given in notes 3; we repeat the relevant portions below)
and an attribute grammars
- (to be given as part of assignment 2).

3 Semantics of Expr₀

Recall our language of expressions, Expr₀.

⟨expr⟩ ∷= ⟨bexpr⟩ | ⟨iexpr⟩
⟨bexpr⟩ ∷= true | false
        | ⟨expr⟩ == ⟨expr⟩ | ⟨expr⟩ \= ⟨expr⟩
        | ⟨expr⟩ =< ⟨expr⟩ | ⟨expr⟩ < ⟨expr⟩
        | ⟨expr⟩ >= ⟨expr⟩ | ⟨expr⟩ > ⟨expr⟩
⟨iexpr⟩ ∷= number | var
        | ⟨iexpr⟩ + ⟨iexpr⟩ | ⟨iexpr⟩ - ⟨iexpr⟩
        | ⟨iexpr⟩ * ⟨iexpr⟩ | ⟨iexpr⟩ div ⟨iexpr⟩ | ⟨iexpr⟩ mod ⟨iexpr⟩

We'll define both the small-step and big-step semantics of expressions before moving on to statements.

4 Semantics of While

With the semantics of expressions defined, we are now prepared to give the semantics of While statements (programs).

Recall the grammar for While.

⟨stmt⟩ ∷=
  skip
| local var in ⟨stmt⟩
| var ≔ ⟨expr⟩
| ⟨stmt⟩ ⟨stmt⟩
| if ⟨bexpr⟩ then ⟨stmt⟩ else ⟨stmt⟩
| while ⟨bexpr⟩ do ⟨stmt⟩

With expressions, we wanted to reduce/evaluate to a constant.
- For statements, we will want to reduce to the simplest program: skip.
- And we will evaluate statements for their side effects, meaning we return a (potentially updated) state.

4.1.1 Assignment, composition

      (E , Σ , σ) ⟶ (E′ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––– assign-reduce
 (x ≔ E , Σ , σ) ⟶ (x ≔ E′ , Σ , σ)


–––––––––––––––––––––––––––––––––––––––––––––––– assign-number
 (x ≔ n , Σ , σ) ⟶ (skip , Σ , σ[Σ(x) ≔ n])


    (S₁ , Σ , σ) ⟶ (S₁′ , Σ , σ′)
––––––––––––––––––––––––––––––––––––––– compose-reduce
 (S₁ S₂ , Σ , σ) ⟶ (S₁′ S₂ , Σ , σ′)


––––––––––––––––––––––––––––––––––––––– compose-skip
    (skip S₂ , Σ , σ) ⟶ (S₂ , Σ , σ)

5 – Semantics of the While language Mark Armstrong, PhD Candidate, McMaster University Fall, 2019