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