Overview Operational Semantics Equivalence Proof
1
Semantics
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
Overview
Operational Semantics
Equivalence Proof
SSccooppeess
Semantics
σημαντιχως
Static Dynamic
Types SemanticsBehaviour
Cost
Scopes
2
Overview Operational Semantics Equivalence Proof
Static Semantics
Definition
3
The static semantics of a program is those significant aspects of the meaning of P that can be determined by the compiler (or an external lint tool) without running the program.
Recall our arithmetic expression language. What properties might we derive statically about those terms?
The only thing we can check is that the program is well-scoped (assuming FOAS).
Overview Operational Semantics Equivalence Proof
Scope-Checking
Γ⊢e1 ok Γ⊢e2 ok Γ⊢e1 ok Γ⊢e2 ok Γ⊢(Numn)ok Γ⊢(Timese1 e2)ok Γ⊢(Pluse1 e2)ok
(x bound)∈Γ Γ⊢e1 ok x bound,Γ⊢e2 ok Γ⊢(Varx)ok Γ⊢(Letx e1 e2)ok
Key Idea
We keep a context Γ, a set of assumptions, on the left hand of our judgement e ok, indicating what is required in order for e to be well-scoped.
This could be read as hypothetical derivations for the judgement e ok or as a binary judgement Γ ⊢ e ok; whichever you prefer.
4
Overview Operational Semantics Equivalence Proof
Scope-Checking Example
Γ⊢e1 ok Γ⊢e2 ok Γ⊢e1 ok Γ⊢e2 ok Γ⊢(Numn)ok Γ⊢(Timese1 e2)ok Γ⊢(Pluse1 e2)ok
(x bound)∈Γ Γ⊢(Varx)ok
Γ⊢e1 ok x bound,Γ⊢e2 ok Γ⊢(Letx e1 e2)ok
“y” ,”x” ⊢ (V “x”) “y” ,”x” ⊢ (V “y”) “y” ,”x” ⊢ (Plus (V “x”) (V “y”))
“x” ⊢ (N 4)
⊢ (N 3) “x” ⊢ (Let “y” (N 4) (Plus (V “x”) (V “y”)))
5
⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
Overview Operational Semantics Equivalence Proof
Dynamic Semantics
Dynamic Semantics can be specified in many ways:
1 Denotational Semantics is the compositional construction of a mathematical
object for each form of syntax. COMP6752 (briefly)
2 Axiomatic Semantics is the construction of a proof calculus to allow correctness of
a program to be verified. COMP2111, COMP6721
3 Operational Semantics is the construction of a program-evaluating state machine
or transition system.
In this course
We focus mostly on operational semantics. We will use axiomatic semantics (Hoare Logic) on Thursday in the imperative programming topic. Denotational semantics are mostly an extension topic, except for the very next slide.
6
Overview Operational Semantics Equivalence Proof
7
Denotational Semantics
· : AST → (Var Z) → Z
Our denotation for arithmetic expressions is functions from environments (mapping from variables to their values) to values.
Num n
Var x Plus e1 e2 Times e1 e2 Let x e1 e2
= λE.n
= λE. E(x)
= λE.e1E+e2E
= λE.e1E×e2E
= λE. e2 (E[x := e1E])
Where E[x := n] is a new environment just like E except the variable x now maps to n.
Overview Operational Semantics Equivalence Proof
Operational Semantics
There are two main kinds of operational semantics.
Small Step Big Step
Also called structural operational semantics (SOS).
A judgement that specifies transitions between states:
e → e′
Also called natural or evaluation semantics.
One big judgement relating expressions to their values:
e⇓v
8
Overview Operational Semantics Equivalence Proof
Big-Step Semantics
We need:
A set of evaluable expressions E A set of values V
A relation ⇓ ⊆ E × V
Example (Arithmetic Expressions)
E is the set of all closed expressions {e | e ok}. V is the set of integers Z.
e1 ⇓ v1 e2[x := (Num v1)] ⇓ v2 (Numn)⇓n (Lete1 (x.e2))⇓v2
e1 ⇓v1 e2 ⇓v2 e1 ⇓v1 e2 ⇓v2 (Pluse1 e2)⇓(v1+v2) (Timese1 e2)⇓(v1×v2)
9
To Code Let’s do it in Haskell!
Overview Operational Semantics Equivalence Proof
Evaluation Strategies
e1 ⇓ v1 e2[x := (Num v1)] ⇓ v2 (Let e1 (x. e2)) ⇓ v2
Any other ways to evaluate Let?
The above is called call-by-value or strict evaluation. Below we have call-by-name:
e2[x := e1] ⇓ v2 (Let e1 (x. e2)) ⇓ v2
This can be computationally very expensive, for example:
let x = ⟨very expensive computation⟩ in x + x + x + x
In confluent languages like this or λ-calculus, this only matters for performance. In
other languages, this is not so. Why?
Haskell uses call-by-need or lazy evaluation, which optimises cases like this.
10
Overview Operational Semantics Equivalence Proof
11
Small Step Semantics
For small step semantics, we need: A set of states Σ
A set of initial states I ⊆ Σ
AsetoffinalstatesF ⊆Σ
A relation → ⊆ Σ × Σ, which specifies only “one step” of the execution.
An execution or trace σ1 → σ2 → σ3 → · · · → σn is called maximal if there exists no σn+1 such that σn → σn+1; and is called complete if it is maximal and σn ∈ F.
Overview Operational Semantics Equivalence Proof
Example
Σ and I are the set of all closed expressions {e | e ok}, F is the set of evaluated expressions {(Num n) | n ∈ Z}.
e1 → e1′ e2 → e2′
(Plus e1 e2) → (Plus e1′ e2) (Plus (Num n) e2) → (Plus (Num n) e2′ )
(Plus (Num n) (Num m)) → (Num (n + m)) (Similarly for Times)
e 1 → e 1′
(Let e1 (x. e2)) → (Let e1′ (x. e2))
(Let (Num n) (x. e2)) → e2[x := Num n]
Example (Arithmetic Expressions)
12
To Code Let’s do it in Haskell!
Overview Operational Semantics Equivalence Proof
Equivalence Comparing small step and big step
Small step semantics are lower-level, they clearly specify the order of evaluation. Big step semantics give us a result without telling us explicitly how it was computed.
Having specified the dynamic semantics in these two ways, it becomes desirable to show they are equivalent, that is:
If there exists a trace e → ··· → (Num n), then e ⇓ n, and vice versa. We will need to define some notation to remove those blasted magic dots.
13
Overview
Operational Semantics
Equivalence Proof
⋆
Let → be the reflexive, transitive closure of →. e1 →e2
⋆
Notation
e2 →en e → e e1 → en
14
We can now state our property formally as:
⋆
e→(Numn) ⇐⇒ e⇓n
⋆⋆
Overview Operational Semantics Equivalence Proof
Doing the Proof
The proof will be done on the iPad, with typeset versions being uploaded as usual. The big-step to small-step direction can be proven by reasonably straightforward rule induction:
e⇓n ⋆
e → n The other direction requires the lemma:
e → e′ e′ ⇓ n e⇓n
The abridged proof is presented in this lecture, with all cases left for the course website.
15