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.
_⟶_ : Expr × Env × State → Expr × Env × State_⟶_ : Stmt × Env × State → Stmt × Env × State_⇓_ : Expr × Env × State → Value
Value is the set of values of the appropriate types_⇓_ : Stmt × Env × State → Env × StateThe two semantics we present, big-step and small-step operational semantics, each serve a different purpose.
Neither approach is “correct” or “incorrect”; they are complementary!
We assume in these slides that every program we consider is correct, meaning it is
That is, we assume these syntactic/static semantic rules have been enforced
To define our two semantic relations, we use inference rules.
An inference rule consists of
Inference rules are written
premise₁ premise₂ … premiseₙ
–––––––––––––––––––––––––––––––––––– name
conclusion
and such an inference rule can be read
premise₁, premise₂, …, and premiseₙ are true (satisfied),
then conclusion is true (satisfied).
You are familiar with the relation ≤ : ℕ → ℕ.
–––––––––– Zero is least
0 ≤ n
m ≤ n
––––––––––––––––– Less than successor
suc m ≤ suc n
which can be read as
nand
m is less than or equal to n,
then suc m is less than or equal to suc m.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.
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.
Let ⊕ be any of the binary, infix operators of the Expr₀ language.
⊕ is a meta-operator standing in for ==, \=, +, *, etc.We make the (arbitrary) choice to always reduce the left subexpression first.
Then the small-step semantics of Expr₀ can be given by just four inference rules.
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 , Σ , σ)
Let us examine each small-step semantic rule.
First, note there are no rules given for the expressions
true, false and number.
The first rule we give
n = σ(Σ(x))
–––––––––––––––––––––––––––––– variable
(x , Σ , σ) ⟶ (n , Σ , σ)
says that a variable reduces to the value stored at the variable in the current environment and state.
The three remaining rules
(E₁ , Σ , σ) ⟶ (E₁′ , Σ , σ)
–––––––––––––––––––––––––––––––––––––––––– operator-left
(E₁ ⊕ E₂ , Σ , σ) ⟶ (E₁′ ⊕ E₂ , Σ , σ)
(E₂ , Σ , σ) ⟶ (E₂′ , Σ , σ)
––––––––––––––––––––––––––––––––––––––––– operator-right
(c ⊕ E₂ , Σ , σ) ⟶ (c ⊕ E₂′ , Σ , σ)
c = c₁ ⊕ c₂
–––––––––––––––––––––––––––––––––––– operator-apply
(c₁ ⊕ c₂ , Σ , σ) ⟶ (c , Σ , σ)
tell us respectively:
c)
and the right subexpression can be reduced,
then reduce the right expression.c₁ ⊕ c₂ refers to the application of the operator ⊕ to the constants,
not an expression.Consider the expression
5 + 3 == 2 * x
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.
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
For each reduction step, we state the inference rule used.
⟶,
we must further state the inference rule which justifies the premise.
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.
–––––––––––––––––– constant
(n , Σ , σ) ⇓ n
n = σ(Σ(x))
–––––––––––––––––– variable
(x , Σ , σ) ⇓ n
(E₁ , Σ , σ) ⇓ n₁ (E₂ , Σ , σ) ⇓ n₂ n = n₁ ⊕ n₂
–––––––––––––––––––––––––––––––––––––––––––––––––––– operator
(E₁ ⊕ E₂ , Σ , σ) ⇓ n
The evaluation relation is between
we do not “return” the environment and state because they never change.
Let us consider once more the expression
5 + 3 == 2 * x
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.
(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.
This proof could also be presented as a “derivation tree”, but this presentation is unwieldly.
(Pardon the poor rendering in LaTeX)
For completion's sake, here is the evaluation of expression
5 + 3 == 2 * x
presented as a derivation tree. We omit the names of the rules used for space.
–––––––––––––––
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
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⟩
skip. (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₂ , Σ , σ)
(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 , Σ , σ)
(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])
skip, assignment, composition
––––––––––––––––––––– skip
(skip , Σ , σ) ⇓ σ
(E , Σ , σ) ⇓ n
––––––––––––––––––––––––––––––––– assign
(x ≔ E , Σ , σ) ⇓ σ[Σ(x) ≔ n]
(S₁ , Σ , σ) ⇓ σ′ (S₂ , Σ , σ′) ⇓ σ″
––––––––––––––––––––––––––––––––––––––– composition
(S₁ S₂ , Σ , σ) ⇓ σ″
(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 , Σ , σ) ⇓ σ
(S , Σ[x ≔ nextref(x,Σ)] , σ) ⇓ σ′
–––––––––––––––––––––––––––––––––––––––––––––––––––––––––– local
(local x in S , Σ , σ) ⇓ σ′[nextref(x,Σ) ≔ undefined]