程序代写代做代考 Haskell flex compiler Overview Operational Semantics Equivalence Proof

Overview Operational Semantics Equivalence Proof
Semantics
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
1

Overview
Operational Semantics
Equivalence Proof
Semantics
σημαντιχως
Scopes
Scopes
Semantics
2

Overview
Operational Semantics
Equivalence Proof
Semantics
σημαντιχως
Static Dynamic
Scopes
Scopes
3

Overview
Operational Semantics
Equivalence Proof
Semantics
σημαντιχως
Static Dynamic
Types
SSccooppeess
Scopes
4

Overview
Operational Semantics
Equivalence Proof
Semantics
σημαντιχως
Static
Types
Dynamic
Behaviour
Cost
SSccooppeess
Scopes
5

Overview Operational Semantics Equivalence Proof
Definition
Static Semantics
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?
6

Overview Operational Semantics Equivalence Proof
Scope-Checking
e1 ok e2 ok e1 ok e2 ok (Num n) ok (Times e1 e2) ok (Plus e1 e2) ok
Γ ⊢ (Var x) 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.

Overview Operational Semantics Equivalence Proof
Scope-Checking
Γ⊢e1 ok Γ⊢e2 ok Γ⊢e1 ok Γ⊢e2 ok Γ⊢(Numn)ok Γ⊢(Timese1 e2)ok Γ⊢(Pluse1 e2)ok
Γ ⊢ (Var x) 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.
9

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) ∈ Γ Γ ⊢ (Var x) 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.
10

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) ∈ Γ
Γ⊢(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.
11

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
Γ⊢(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.
12

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.
13

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)∈Γ Γ⊢e1 ok x bound,Γ⊢e2 ok Γ⊢(Varx)ok Γ⊢(Letx e1 e2)ok
⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
14

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)∈Γ Γ⊢e1 ok x bound,Γ⊢e2 ok Γ⊢(Varx)ok Γ⊢(Letx e1 e2)ok
⊢ (N 3)
⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
15

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)∈Γ Γ⊢e1 ok x bound,Γ⊢e2 ok Γ⊢(Varx)ok Γ⊢(Letx e1 e2)ok
⊢ (N 3) “x” ⊢ (Let “y” (N 4) (Plus (V “x”) (V “y”))) ⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
16

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” ⊢ (Plus (V “x”) (V “y”)) ⊢ (N 3) “x” ⊢ (Let “y” (N 4) (Plus (V “x”) (V “y”)))
“x” ⊢ (N 4)
⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
17

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”)))
⊢ (Let “x” (N 3) (Let “y” (N 4) (Plus (V “x”) (V “y”))))
18

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.
22

Overview
Operational Semantics
Equivalence Proof
Denotational Semantics
􏰍·􏰎 : AST →
􏰍Num n􏰎 = 􏰍Var x􏰎 = 􏰍Plus e1 e2􏰎 = 􏰍Times e1 e2􏰎 = 􏰍Letxe1e2􏰎 =
23

Overview
Operational Semantics
Equivalence Proof
Denotational Semantics
􏰍·􏰎 : AST → Z
􏰍Numn􏰎 =n 􏰍Var x􏰎 = 􏰍Plus e1 e2􏰎 = 􏰍Times e1 e2􏰎 = 􏰍Letxe1e2􏰎 =
24

Overview Operational Semantics Equivalence Proof
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􏰎 􏰍Letxe1e2􏰎
= λE.n
= λE. E(x)
= λE. 􏰍e1􏰎 􏰍e2􏰎
= λE. 􏰍e1􏰎 􏰍e2􏰎
= λE.
26

Overview Operational Semantics Equivalence Proof
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􏰎 􏰍Letxe1e2􏰎
= λE.n
= λE. E(x)
= λE.􏰍e1􏰎E+􏰍e2􏰎E
= λE.􏰍e1􏰎E×􏰍e2􏰎E
= λE.
27

Overview Operational Semantics Equivalence Proof
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.􏰍e1􏰎E+􏰍e2􏰎E
= λE.􏰍e1􏰎E×􏰍e2􏰎E
= λE. 􏰍e2􏰎 (E[x := 􏰍e1􏰎E])
Where E[x := n] is a new environment just like E except the variable x now maps to n.
28

Overview Operational Semantics Equivalence Proof
Operational Semantics
There are two main kinds of operational semantics.
Small Step Big Step
29

Overview Operational Semantics Equivalence Proof
Operational Semantics
There are two main kinds of operational semantics.
Small Step Big Step
Also called natural or evaluation semantics.
One big judgement relating expressions to their values:
e⇓v
30

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
31

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.
(Num n) ⇓ n
e1 ⇓v1 e2 ⇓v2 e1 ⇓v1 e2 ⇓v2
(Pluse1 e2)⇓(v1+v2) (Timese1 e2)⇓(v1×v2) To Code Let’s do it in Haskell!

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.
(Numn)⇓n (Lete1 (x.e2))⇓
e1 ⇓v1 e2 ⇓v2 e1 ⇓v1 e2 ⇓v2
(Pluse1 e2)⇓(v1+v2) (Timese1 e2)⇓(v1×v2) To Code Let’s do it in Haskell!
34

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
(Numn)⇓n (Lete1 (x.e2))⇓
e1 ⇓v1 e2 ⇓v2 e1 ⇓v1 e2 ⇓v2 (Pluse1 e2)⇓(v1+v2) (Timese1 e2)⇓(v1×v2)
To Code Let’s do it in Haskell!
35

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)
To Code Let’s do it in Haskell!
36

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?
37

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?
39

Overview Operational Semantics Equivalence Proof
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.
41

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}.
e 1 􏰀 → e 1′ (Plus e1 e2) 􏰀→
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
42

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}.
e 1 􏰀 → e 1′
(Plus e1 e2) 􏰀→ (Plus e1′ e2)
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
43

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}.
e 1 􏰀 → e 1′
(Plus e1 e2) 􏰀→ (Plus e1′ e2) (Plus (Num n) e2) 􏰀→
(Plus (Num n) (Num m)) 􏰀→
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
44

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)) 􏰀→
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
45

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))
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
46

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)
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
47

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)
(Let e1 (x. e2)) 􏰀→
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
48

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))
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
49

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)) 􏰀→
Example (Arithmetic Expressions)
To Code Let’s do it in Haskell!
50

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)
To Code Let’s do it in Haskell!
51

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.
52

Overview
Operational Semantics
Equivalence Proof
⋆
Let 􏰀→ be the reflexive, transitive closure of 􏰀→. e1 􏰀→e2
⋆
Notation
e2 􏰀→en e 􏰀→ e e1 􏰀→ en
We can now state our property formally as:
⋆
e􏰀→(Numn) ⇐⇒ e⇓n
⋆⋆
53

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.
54

Related Posts