#+Title: 5 – Semantics of the While language
#+Author: Mark Armstrong, PhD Candidate, McMaster University
#+Date: Fall, 2019
#+Description: Formal semantics for our While language
#+Options: toc:nil
#+Reveal_root: https://cdn.jsdelivr.net/reveal.js/3.0.0/
#+Reveal_init_options: width:1600, height:900, controlsLayout:'edges',
#+Reveal_init_options: margin: 0.1, minScale:0.125, maxScale:5
#+Reveal_extra_css: local.css
#+html:
* LaTeX Header :ignore:
#+LaTeX_header: \usepackage{amsthm}
#+LaTeX_header: \theoremstyle{definition}
#+LaTeX_header: \newtheorem{definition}{Definition}[section]
#+LaTeX_header: \newenvironment{NOTES}{
#+LaTeX_header: \begin{center}
#+LaTeX_header: \begin{tabular}
#+LaTeX_header: {|p{0.9\textwidth}|}
#+LaTeX_header: \hline\\
#+LaTeX_header: \begin{scriptsize}
#+LaTeX_header: }{
#+LaTeX_header: \end{scriptsize}
#+LaTeX_header: \\\\\hline
#+LaTeX_header: \end{tabular}
#+LaTeX_header: \end{center}
#+LaTeX_header: }
#+LaTeX_header: \usepackage{unicode-math}
#+LaTeX_header: \usepackage{unicode}
* Preamble
** Notable references
- Programming Languages and Operational Semantics: A Concise Overview,
Fernández
- Chapter 4 – Operational Semantics of Imperative Languages
** Update history
- Nov. 12 ::
- A correction to the PDF version: missing prime symbols were added.
- Slight cleanup; added references and table of contents.
- Nov. 4 ::
- Original version posted
** Table of contents
# The table of contents are added using org-reveal-manual-toc,
# and so must be updated upon changes or added last.
#+HTML:
#+begin_scriptsize
- [[Preamble][Preamble]]
- [[Notable references][Notable references]]
- [[Update history][Update history]]
- [[Table of contents][Table of contents]]
- [[Introduction to operational semantics][Introduction to operational semantics]]
- [[Why two different semantics?][Why two different semantics?]]
- [[Syntactic correctness][Syntactic correctness]]
- [[Defining a relation via inference rules][Defining a relation via inference rules]]
- [[Example inference rules – defining the “less than” relation][Example inference rules – defining the “less than” relation]]
- [[Semantics of /Expr₀/][Semantics of /Expr₀/]]
- [[Meta-variables][Meta-variables]]
- [[Small-step semantics of /Expr₀/][Small-step semantics of /Expr₀/]]
- [[Explaining the small-step semantic rules of /Expr₀/ – constants][Explaining the small-step semantic rules of /Expr₀/ – constants]]
- [[Explaining the small-step semantic rules of /Expr₀/ – variables][Explaining the small-step semantic rules of /Expr₀/ – variables]]
- [[Explaining the small-step semantic rules of /Expr₀/ – operators][Explaining the small-step semantic rules of /Expr₀/ – operators]]
- [[An example reduction sequence][An example reduction sequence]]
- [[Big-step semantics of /Expr₀/][Big-step semantics of /Expr₀/]]
- [[Notes][Notes]]
- [[An example evaluation][An example evaluation]]
- [[Derivation tree][Derivation tree]]
- [[Semantics of /While/][Semantics of /While/]]
- [[Small-step semantics of /While/][Small-step semantics of /While/]]
- [[Assignment, composition][Assignment, composition]]
- [[Branch, loop][Branch, loop]]
- [[Local variables][Local variables]]
- [[Big-step semantics of /While/][Big-step semantics of /While/]]
- [[~skip~, assignment, composition][~skip~, assignment, composition]]
- [[Branch, loop][Branch, loop]]
- [[Local variables][Local variables]]
#+end_scriptsize
#+HTML:
* Introduction to operational semantics
** Intro slide :ignore:
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.
** 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!
** 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).
** Defining a relation via inference rules
To define our two semantic relations, we use /inference rules/.
An inference rule consists of
- a set of /premises/ and
- a /conclusion/;
- we also give each inference rule a /name/.
Inference rules are written
#+begin_src text
premise₁ premise₂ … premiseₙ
–––––––––––––––––––––––––––––––––––– name
conclusion
#+end_src
and such an inference rule can be read
- If ~premise₁~, ~premise₂~, …, and ~premiseₙ~ are true (satisfied),
then ~conclusion~ is true (satisfied).
** Example inference rules – defining the “less than” relation
You are familiar with the relation ~≤ : ℕ → ℕ~.
- It can be defined via two inference rules.
- One “base case” rule with no premises, and
- one “induction step” with one premise.
#+begin_src text
–––––––––– Zero is least
0 ≤ n
m ≤ n
––––––––––––––––– Less than successor
suc m ≤ suc n
#+end_src
which can be read as
- Zero is less than or equal to any natural number ~n~
and
- If ~m~ is less than or equal to ~n~,
then ~suc m~ is less than or equal to ~suc m~.
* Semantics of /Expr₀/
Recall our language of expressions, /Expr₀/.
#+begin_src text
⟨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⟩
#+end_src
We'll define both the small-step and big-step semantics of expressions
before moving on to statements.
** Meta-variables
Throughout this section, the meta-variables
- ~E~, ~E₁~, ~E₂~, ~E′~, etc. vary over /expressions/,
- ~c~, ~c₁~, ~c₂~, ~c′~, etc. vary over /constant/ expressions
of either integer or boolean type,
- ~x~ is any variable,
- ~Σ~ is any environment, and
- ~σ~ is any state.
** Small-step semantics of /Expr₀/
Let ~⊕~ be any of the binary, infix operators of the /Expr₀/ language.
- That is, ~⊕~ is a meta-operator standing in for ~==~, ~\=~, ~+~, ~*~, etc.
We make the (arbitrary) choice to always reduce the left subexpression first.
- An alternate small-step semantics could reduce the right subexpression,
or give different orders for different operators.
Then the small-step semantics of /Expr₀/ can be given
by just four inference rules.
#+begin_src text
n = σ(Σ(x))
–––––––––––––––––––––––––––––– variable
(x , Σ , σ) ⟶ (n , Σ , σ)
(E₁ , Σ , σ) ⟶ (E₁′ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––– operator-left
(E₁ ⊕ E₂ , Σ , σ) ⟶ (E₁′ ⊕ E₂ , Σ , σ)
(E₂ , Σ , σ) ⟶ (E₂′ , Σ , σ)
––––––––––––––––––––––––––––––––––––––––– operator-right
(c ⊕ E₂ , Σ , σ) ⟶ (c ⊕ E₂′ , Σ , σ)
c = c₁ ⊕ c₂
–––––––––––––––––––––––––––––––––––– operator-apply
(c₁ ⊕ c₂ , Σ , σ) ⟶ (c , Σ , σ)
#+end_src
*** Explaining the small-step semantic rules of /Expr₀/ – constants
Let us examine each small-step semantic rule.
First, note there are no rules given for the expressions
~true~, ~false~ and ~number~.
- That is, there are no rules for constant expressions.
- This is because constants are /irreducible/;
they cannot be simplified any further!
- The presence of such rules would mean we could
/infinitely/ “reduce” expressions, which is undesirable.
*** Explaining the small-step semantic rules of /Expr₀/ – variables
The first rule we give
#+begin_src text
n = σ(Σ(x))
–––––––––––––––––––––––––––––– variable
(x , Σ , σ) ⟶ (n , Σ , σ)
#+end_src
says that a variable reduces to the value stored at the variable
in the current environment and state.
- Recall that we only have integer variables in /Expr₀/.
*** Explaining the small-step semantic rules of /Expr₀/ – operators
The three remaining rules
#+begin_src text
(E₁ , Σ , σ) ⟶ (E₁′ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––– operator-left
(E₁ ⊕ E₂ , Σ , σ) ⟶ (E₁′ ⊕ E₂ , Σ , σ)
(E₂ , Σ , σ) ⟶ (E₂′ , Σ , σ)
––––––––––––––––––––––––––––––––––––––––– operator-right
(c ⊕ E₂ , Σ , σ) ⟶ (c ⊕ E₂′ , Σ , σ)
c = c₁ ⊕ c₂
–––––––––––––––––––––––––––––––––––– operator-apply
(c₁ ⊕ c₂ , Σ , σ) ⟶ (c , Σ , σ)
#+end_src
tell us respectively:
- If the left subexpression can be reduced (it is non-constant),
then reduce it.
- If the left subexpression is a constant,
(expressed by the fact we use the variable ~c~)
and the right subexpression can be reduced,
then reduce the right expression.
- If both subexpressions are constants,
then perform the operation.
- We abuse notation a small amount here; in the premise,
~c₁ ⊕ c₂~ refers to the application of the operator ~⊕~ to the constants,
not an expression.
*** An example reduction sequence
Consider the expression
#+begin_src text
5 + 3 == 2 * x
#+end_src
and suppose in the current environment and state,
- ~Σ(x) = R~ and
- ~σ(R) = 4~.
We can test out our reduction rules by trying to reduce this expression
to its value, which should be ~true~.
#+begin_src text
5 + 3 == 2 * x
⟶⟨ “operator-left” with “operator-apply” ⟩
8 == 2 * x
⟶⟨ “operator-right” with “operator-right” with “variable” with fact 4 = σ(Σ(x)) ⟩
8 == 2 * 4
⟶⟨ “operator-right” with “operator-apply” ⟩
8 == 8
⟶⟨ “operator-apply” ⟩
true
#+end_src
For each reduction step, we state the inference rule used.
- If the inference rule has a premise involving ~⟶~,
we must further state the inference rule which justifies the premise.
** Big-step semantics of /Expr₀/
Once again, let ~⊕~ be any of the binary, infix operators
of the /Expr₀/ language.
The big-step semantics of /Expr₀/ can be given
by just three inference rules.
#+begin_src text
–––––––––––––––––– constant
(n , Σ , σ) ⇓ n
n = σ(Σ(x))
–––––––––––––––––– variable
(x , Σ , σ) ⇓ n
(E₁ , Σ , σ) ⇓ n₁ (E₂ , Σ , σ) ⇓ n₂ n = n₁ ⊕ n₂
–––––––––––––––––––––––––––––––––––––––––––––––––––– operator
(E₁ ⊕ E₂ , Σ , σ) ⇓ n
#+end_src
*** Notes
- Recall that we did not give a reduction rule for constants;
in contrast, we do give an evaluation rule for them.
- Any expression can be evaluated; not all expressions can be reduced.
- The evaluation relation is between
- expression, environment, state triples and
- values;
we do not “return” the environment and state because they never change.
- Expressions are evaluated only for their value, not for a side effect.
- These evaluation rules “look similar” to the behaviour of the
interpreter provided for assignment 1.
- It is possible to write an interpreter following the small-step semantics.
*** An example evaluation
Let us consider once more the expression
#+begin_src text
5 + 3 == 2 * x
#+end_src
and an environment and state such that
- ~Σ(x) = R~ and
- ~σ(R) = 4~.
Evaluation semantics do not define steps; to evaluate this expression,
we will have to evaluate each subexpression in turn.
#+begin_src text
(1) (5 , Σ , σ) ⇓ 5, by “constant”.
(2) (3 , Σ , σ) ⇓ 3, by “constant”.
(3) (2 , Σ , σ) ⇓ 2, by “constant”.
(4) (x , Σ , σ) ⇓ 4, by “variable” with fact 4 = σ(Σ(x)).
(5) (5 + 3 , Σ , σ) ⇓ 8, by “expression” with (1) and (2)
and fact 8 = 5 + 3.
(6) (2 + x , Σ , σ) ⇓ 8, by “expression” with (3) and (4)
and fact 8 = 2 * 4.
(7) (5 + 3 == 2 + x , Σ , σ) ⇓ true, by “expression” with (5) and (6)
and fact 8 == 8.
#+end_src
This proof could also be presented as a “derivation tree”,
but this presentation is unwieldly.
*** Derivation tree
(Pardon the poor rendering in LaTeX)
For completion's sake, here is the evaluation of expression
#+begin_src text
5 + 3 == 2 * x
#+end_src
presented as a derivation tree.
We omit the names of the rules used for space.
#+begin_src text
–––––––––––––––
4 = σ(Σ(x))
––––––––––––––––– –––––––––––––––– ––––––––––––– ––––––––––––––––– ––––––––––––––– –––––––––––––
(5 , Σ , σ) ⇓ 5 (3 , Σ , σ) ⇓ 3 8 == 5 + 3 (2 , Σ , σ) ⇓ 2 (x , Σ , σ) ⇓ 4 8 == 2 * x
––––––––––––––––––––––––––––––––––––––––––––––––– ––––––––––––––––––––––––––––––––––––––––––––––––––
(5 + 3 , Σ , σ) ⇓ 8 (2 * x , Σ , σ) ⇓ 8
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
(5 + 3 == 2 + x , Σ , σ) ⇓ true
#+end_src
* 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/.
#+begin_src text
⟨stmt⟩ ∷=
skip
| local var in ⟨stmt⟩
| var ≔ ⟨expr⟩
| ⟨stmt⟩ ⟨stmt⟩
| if ⟨bexpr⟩ then ⟨stmt⟩ else ⟨stmt⟩
| while ⟨bexpr⟩ do ⟨stmt⟩
#+end_src
- 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/.
** Small-step semantics of /While/
*** Assignment, composition
#+begin_src text
(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₂ , Σ , σ)
#+end_src
*** Branch, loop
#+begin_src text
(E , Σ , σ) ⟶ (E′ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––– branch-reduce
(if E then S₁ else S₂ , Σ , σ) ⟶ (if E′ then S₁ else S₂ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––––––––––––– branch-left
(if true then S₁ else S₂ , Σ , σ) ⟶ (S₁ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––––––––––––– branch-right
(if false then S₁ else S₂ , Σ , σ) ⟶ (S₂ , Σ , σ)
––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––– loop-unfold
(while E do S , Σ , σ) ⟶ (if E then (S (while E do S)) else skip , Σ , σ)
#+end_src
*** Local variables
#+begin_src text
(S , Σ[x ≔ nextref(x,Σ)] , σ) ⟶ (S , Σ[x ≔ nextref(x,Σ)] , σ′)
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––– local-reduce
(local x in S , Σ , σ) ⟶ (local x in S′ , Σ , σ′)
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––– local-skip
(local x in skip , Σ , σ) ⟶ (skip , Σ , σ[nextref(x,Σ) ≔ undefined])
#+end_src
** Big-step semantics of /While/
*** ~skip~, assignment, composition
#+begin_src text
––––––––––––––––––––– skip
(skip , Σ , σ) ⇓ σ
(E , Σ , σ) ⇓ n
––––––––––––––––––––––––––––––––– assign
(x ≔ E , Σ , σ) ⇓ σ[Σ(x) ≔ n]
(S₁ , Σ , σ) ⇓ σ′ (S₂ , Σ , σ′) ⇓ σ″
––––––––––––––––––––––––––––––––––––––– composition
(S₁ S₂ , Σ , σ) ⇓ σ″
#+end_src
*** Branch, loop
#+begin_src text
(E , Σ , σ) ⇓ true (S₁ , Σ , σ) ⇓ σ′
–––––––––––––––––––––––––––––––––––––––––– branch-left
(if E then S₁ else S₂ , Σ , σ) ⇓ σ′
(E , Σ , σ) ⇓ false (S₂ , Σ , σ) ⇓ σ′
–––––––––––––––––––––––––––––––––––––––––– branch-right
(if E then S₁ else S₂ , Σ , σ) ⇓ σ′
(E , Σ , σ) ⇓ true (S (while E do S) , Σ , σ) ⇓ σ′
––––––––––––––––––––––––––––––––––––––––––––––––––––––– loop-do
(while E do S , Σ , σ) ⇓ σ′
(E , Σ , σ) ⇓ false
––––––––––––––––––––––––––––––– loop-skip
(while E do S , Σ , σ) ⇓ σ
#+end_src
*** Local variables
#+begin_src text
(S , Σ[x ≔ nextref(x,Σ)] , σ) ⇓ σ′
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––– local
(local x in S , Σ , σ) ⇓ σ′[nextref(x,Σ) ≔ undefined]
#+end_src