留学生代考 CS 314: Principles of Programming Languages

CS 314: Principles of Programming Languages
Operational Semantics
CS 314 Spring 2022 1

Formal Semantics of a Prog. Lang.
Mathematical description of the meaning of programs written in that language
• What a program computes, and what it does
Operational semantics: define how programs execute
• Often on an abstract machine (mathematical model of computer)
• Analogous to interpretation
CS 314 Spring 2022 2

This Course: Operational Semantics
We will show how an operational semantics may be defined for Micro-Ocaml
• And develop an interpreter for it, along the way
Approach: use rules to define a judgment e⇒v
• Says“eevaluatestov”
•e: expression in Micro-OCaml
•v: valuethatresultsfromevaluatinge
CS 314 Spring 2022 4

Definitional Interpreter
It turns out that the rules for judgment e ⇒ v can be easily turned into idiomatic OCaml code
• Thelanguage’sexpressionseandvaluesvhave corresponding OCaml datatype representations exp and value
• The semantics is represented as a function
eval: exp -> value
This way of presenting the semantics is referred to as a definitional interpreter
• The interpreter defines the language’s meaning
CS 314 Spring 2022 5

Micro-OCaml Expression Grammar e::=x|n|e+e|let x = e in e
e, x, n are meta-variables that stand for categories of syntax
• x is any identifier (like z, y, foo)
• n is any numeral (like 1, 0, 10, -25)
• e is any expression (here defined, recursively!)
Concrete syntax of actual expressions in black • Such aslet,+,z,foo,in, …
•::= and | are meta-syntax used to define the syntax of a language (part of “Backus-Naur form,” or BNF)
CS 314 Spring 2022 6

Micro-OCaml Expression Grammar e::=x|n|e+e|let x = e in e
• 1 is a numeral n which is an expression e
• 1+z is an expression e because
Ø 1 is an expression e,
Ø z is an identifier x, which is an expression e, and Ø e+e is an expression e
• let z = 1 in 1+z is an expression e because Ø z is an identifier x,
Ø 1 is an expression e ,
Ø 1+z is an expression e, and
Ølet x = e in eis an expressione
CS 314 Spring 2022 7

Abstract Syntax = Structure
Here, the grammar for e is describing its abstract syntax tree (AST), i.e., e’s structure
e::=x|n|e+e|let x = e in e corresponds to (in definitional interpreter)
type id = string
type num = int
type exp =
| Ident of id (* x *) | Num of num (* n *) |Plusofexp*exp (*e+e*) | Let of id * exp * exp
(* let x=e in e *)
CS 314 Spring 2022 8

Aside: Real Interpreters
Abstract Syntax Tree (AST),
intermediate representation (IR)
Static Analyzer
(e.g., Type Checker)
the part we write in the definitional interpreter
CS 314 Spring 2022

An expression’s final result is a value. What can values be?
v::=n Just numerals for now
• In terms of an interpreter’s representation:
type value = int
• In a full language, values v will also include booleans (true, false), strings, functions, …
CS 314 Spring 2022 11

Interpreter
The semantics is represented as a function
eval: exp -> value
type id = string
type num = int
type exp =
| Ident of id (* x *) | Num of num (* n *) |Plusofexp*exp (*e+e*) | Let of id * exp * exp
(* let x=e in e *)
CS 314 Spring 2022 12
type value = int

Defining the Semantics
Use rules to define judgment e ⇒ v
Judgments are just statements. We use rules to prove that the statement is true.
Ø 1+3 is an expression e, and 4 is a value v
Ø This judgment claims that 1+3 evaluates to 4
Ø We use rules to prove it to be true • let foo=1+2 in foo+5 ⇒ 8
•let f=1+2 in let z=1 in f+z ⇒4
CS 314 Spring 2022 13

Rules as English Text
Suppose e is a numeral n
• Theneevaluatestoitself,i.e.,n⇒n
Suppose e is an addition expression e1 + e2
• Ife1evaluateston1,i.e.,e1⇒n1
• Ife2evaluateston2,i.e.,e2⇒n2
• Theneevaluateston3,wheren3isthesumofn1andn2 • I.e.,e1+e2⇒n3
Suppose e is a let expression let x = e1 in e2
• Ife1evaluatestov,i.e.,e1⇒v1
• Ife2{v1/x}evaluatestov2,i.e.,e2{v1/x}⇒v2
Ø Here, e2{v1/x} means “the expression after substituting occurrences of x in
e2 with v1”
• Theneevaluates tov2, i.e.,let x = e1 in e2⇒v2
CS 314 Spring 2022 14
No rule when e is x

Rules of Inference
We can use a more compact notation for the rules we just presented: rules of inference
• Has the following format
• Says: if the conditions H1 … Hn (“hypotheses”) are
true, then the condition C (“conclusion”) is true
• If n=0 (no hypotheses) then the conclusion
automatically holds; this is called an axiom
We are using inference rules where C is our judgment about evaluation, i.e., that e ⇒ v
CS 314 Spring 2022 15

Rules of Inference: Num and Sum
Suppose e is a numeral n
• Theneevaluatestoitself,i.e.,n⇒n
Suppose e is an addition expression e1 + e2 • Ife1evaluateston1,i.e.,e1⇒n1
• Ife2evaluateston2,i.e.,e2⇒n2
• Theneevaluateston3,wheren3isthesumofn1andn2 • I.e.,e1+e2⇒n3
e1⇒n1 e2⇒n2 n3isn1+n2
CS 314 Spring 2022 16

Rules of Inference: Let
Suppose e is a let expression let x = e1 in e2 • Ife1evaluatestov,i.e.,e1⇒v1
• Ife2{v1/x}evaluatestov2,i.e.,e2{v1/x}⇒v2
• Theneevaluates tov2, i.e.,let x = e1 in e2⇒v2
e1 ⇒ v1 e2{v1/x} ⇒ v2
letx=e1ine2 ⇒v2
CS 314 Spring 2022 17

Derivations
When we apply rules to an expression in succession, we produce a derivation
• It’s a kind of tree, rooted at the conclusion
Produce a derivation by goal-directed search
• Pick a rule that could prove the goal
• Then repeatedly apply rules on the corresponding hypotheses
Ø Goal: Show that let x = 4 in x+3 ⇒ 7
CS 314 Spring 2022 18

Derivations
e1⇒n1 e2⇒n2 n3isn1+n2
e1 ⇒ v1 e2{v1/x} ⇒ v2
letx=e1ine2 ⇒v2
Goal: show that letx=4inx+3 ⇒ 7
4⇒4 3⇒3 7is4+3 x+3{44/+x3} ⇒ 7
let x = 4 in x+3 ⇒ 7
CS 314 Spring 2022

What is derivation of the following judgment?
2 + (3 + 8) ⇒ 13
2⇒2 3+8⇒11 ——————— 2+(3+8) ⇒ 13
11 is 3+8 ———-
2⇒2 3 + 8 ⇒ 11 —————————- 2+(3+8) ⇒ 13
————
3 + 8 ⇒ 11 2 ⇒ 2 ————————- 2+(3+8) ⇒ 13
CS 314 Spring 2022

Trace of evaluation of eval function corresponds to a derivation by the rules
Definitional Interpreter
The style of rules lends itself directly to the implementation of an interpreter as a recursive function
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
e1⇒n1 e2⇒n2 n3isn1+n2
e1 ⇒ v1 e2{v1/x} ⇒ v2
letx=e1ine2 ⇒v2
CS 314 Spring 2022 22

Trace of evaluation of eval function corresponds to a derivation by the rules
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
Definitional Interpreter
let x = 4 in x + 3
eval Let(“x”,Num 4, Plus(Ident(“x”),Num 3))
CS 314 Spring 2022 23

Trace of evaluation of eval function corresponds to a derivation by the rules
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
Definitional Interpreter
let x = 4 in x + 3 eval Let(“x”,Num 4,
Plus(Ident(“x”),Num 3))
CS 314 Spring 2022 24

Trace of evaluation of eval function corresponds to a derivation by the rules
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
Definitional Interpreter
CS 314 Spring 2022
let x = 4 in x + 3
eval Let(“x”,Num 4, Plus(Ident(“x”),Num 3))
eval Num 4⇒ 4

Trace of evaluation of eval function corresponds to a derivation by the rules
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
Definitional Interpreter
CS 314 Spring 2022
let x = 4 in x + 3
eval Let(“x”,Num 4, Plus(Ident(“x”),Num 3))
eval Num 4⇒ 4 eval(Plus(Num 4,Num 3))
eval Num 4⇒ 4 eval Num 3⇒ 3

Trace of evaluation of eval function corresponds to a derivation by the rules
let rec eval (e:exp):value = match e with
Ident x -> (* no rule *) failwith “no value”
| Num n -> n
| Plus (e1,e2) ->
let n1 = eval e1 in let n2 = eval e2 in let n3 = n1+n2 in n3
| Let (x,e1,e2) ->
let v1 = eval e1 in
let e2’ = subst v1 x e2 in let v2 = eval e2’ in v2
Definitional Interpreter
CS 314 Spring 2022
let x = 4 in x + 3
eval Let(“x”,Num 4, Plus(Ident(“x”),Num 3))
eval Num 4⇒ 4 eval(Plus(Num 4,Num 3)) ⇒7

Derivations = Interpreter Call Trees
4⇒4 3⇒3 7is4+3 x+3{44/+x3} ⇒ 7
let x = 4 in x+3 ⇒ 7
Has the same shape as the recursive call tree of the interpreter:
eval Num 4⇒ 4 eval Num 3⇒ 3 7is4+3
eval (subst 4 “x” Plus(Ident(“x”),Num 3)) ⇒ 7
eval Num 4⇒ 4
eval Let(“x”,Num 4,Plus(Ident(“x”),Num 3)) ⇒ 7
CS 314 Spring 2022 30

Semantics Defines Program Meaning
e⇒vholds if and only if a proof can be built
• Proofs are derivations: axioms at the top, then rules
whose hypotheses have been proved to the bottom • N o p r o o f m e a n s e ⇒/ v
Proofs can be constructed bottom-up
• In a goal-directed fashion
Thus, function evale= {v|e⇒v}
• Determinism of semantics implies at most one
element for any e
So: Expression e means v
CS 314 Spring 2022 31

Environment-style Semantics
The previous semantics uses substitution to handle variables
• As we evaluate, we replace all occurrences of a variable x with values it is bound to
An alternative semantics, closer to a real implementation, is to use an environment
• As we evaluate, we maintain an explicit map from variables to values, and look up variables as we see them
CS 314 Spring 2022 32

Environment-style Semantics
Program Environment
let a = 1;;
let a = 0;;
let b = a + 10;; let f = a + b;; let b = 5;;
let x = f;; (* End *)
10; a = 0; a = 1}
A = {x = 10; b = 5; f = 10; b = 10; a = 0; a = 1}
= 0; a = 1}
= 10;a = 0; a = 1} = 10; b = 10;a = 0;
= 5; f = 10; b =
CS 314 Spring 2022

Environments
Mathematically, an environment is a partial function from identifiers to values
• IfAisanenvironment,andxisanidentifier,thenA(x)can either be …
• … a value (intuition: the variable has been declared)
• … or undefined (intuition: variable has not been declared)
An environment can also be thought of as a table
• thenA(x)is0,A(y)is2,andA(z)isundefined
CS 314 Spring 2022 34

Notation, Operations on Environments
• is the empty environment (undefined for all ids)
If A is an environment then A,x:v is one that extends A with a mapping from x to v
• Sometimes just write x:v instead of •,x:v for brevity • NB. if A maps x to some v’, then that mapping is
shadowed by the mapping x:v
Lookup A(x) is defined as follows •(x) = undefined
(A, y:v)(x) = A(x) if x <> y and A(x) defined
CS 314 Spring 2022
undefined otherwise

Environment-style Semantics
Environment
let m = 2;;
let a = 1;;
let a = 0;;
let b = a + 10;;
A2 = (A1,m:2) A3 = (A2,a:1) A4 = (A3,a:0)
A4(a)=0, A4(m)=2
Lookup A(x) is defined as follows •(x) = undefined
(A, y:v)(x) = A(x) undefined
CS 314 Spring 2022
if x <> y and A(x) defined otherwise

Definitional Interpreter: Environments
type env = (id * value) list
let extend env x v = (x,v)::env
let rec lookup env x = match env with
[] -> failwith “undefined” | (y,v)::env’ ->
if x = y then v else lookup env’ x
let m = 2;;
let a = 1;;
let a = 0;;
let b = a + 10;;
Environment
A2 = (m,2):: A1 A3 = (a,1):: A2 A4 = (a,0):: A3
An environment is just a list of mappings, which are just pairs of variable to value
– called an association list
CS 314 Spring 2022
A4(a)=0, A4(m)=2

Semantics with Environments
The environment semantics changes the judgment
where A is an environment
• Idea: A is used to give values to the identifiers in e
• Acanbethoughtofascontainingdeclarationsmadeuptoe
Previous rules can be modified by
• Inserting A everywhere in the judgments • AddingaruletolookupvariablesxinA • ModifyingtheruleforlettoaddxtoA
CS 314 Spring 2022 38

Environment-style Rules
Look up variable x in environment A
Extend environment A
with mapping fromxtov1
A;e1⇒v1 A,x:v1;e2⇒v2
A;letx=e1ine2 ⇒v2
A;e1⇒n1 A;e2⇒n2 n3isn1+n2
A;e1+e2⇒n3
CS 314 Spring 2022

Derivation of the following judgment?
•;letx=3inx+2 ⇒ 5
(•,x:3);x⇒3 (•,x:3);2⇒2 5is3+2
———————————— •;3⇒3 (•,x:3); x+2 ⇒ 5
———————————— •;letx=3inx+2 ⇒ 5
CS 314 Spring 2022

Recall: Abstract Syntax = Structure
Here, the grammar for e is describing its abstract syntax tree (AST), i.e., e’s structure
e::=x|n|e+e|let x = e in e corresponds to (in definitional interpreter)
type id = string
type num = int
type exp =
| Ident of id (* x *) | Num of num (* n *) |Plusofexp*exp (*e+e*) | Let of id * exp * exp
(* let x=e in e *)
CS 314 Spring 2022 41

Definitional Interpreter: Evaluation
let rec eval env e = match e with
Ident x -> lookup env x | Num n -> n
| Plus (e1,e2) ->
let n1 = eval env e1 in let n2 = eval env e2 in let n3 = n1+n2 in
| Let (x,e1,e2) ->
let v1 = eval env e1 in
let env’ = extend env x v1 in let v2 = eval env’ e2 in v2
CS 314 Spring 2022 42

Rules for Eq0 and Booleans
A; true ⇒ true
A;eq0e⇒true
A;e⇒v v≠0
A;eq0e⇒false
A; false ⇒ false
Booleans evaluate to themselves
• A;false⇒false
eq0 tests for 0
• A;eq00⇒true
• A;eq03+4⇒false
CS 314 Spring 2022 44

Rules for Conditionals
A;e1⇒true A;e2⇒v
A;ife1thene2elsee3 ⇒v
A;e1⇒false A;e3⇒v
A;ife1thene2elsee3 ⇒v
Notice that only one branch is evaluated
• A;ifeq00then3else4⇒3 • A;ifeq01then3else4⇒4
CS 314 Spring 2022 45

What is the derivation of the following judgment? •; if eq0 3-2 then 5 else 10⇒10
•; 3⇒3 •; 2⇒2 3-2is1 ————————
•; eq0 3-2 ⇒ false •; 10⇒10 ———————————- •;ifeq03-2then5else10 ⇒ 10
———-
•;3-2⇒1 1≠0 ——————
•; eq0 3-2 ⇒ false ——————————— •;ifeq03-2then5else10 ⇒ 10
—————
eq0 3-2 ⇒ false 10 ⇒ 10 —————————– if eq0 3-2 then 5 else 10⇒10
CS 314 Spring 2022 46

Recall – let Specializes match More general form of let allows patterns:
let p = e1 in e2
• where p is a pattern. If e1 fails to match that pattern
then an exception is thrown
This pattern form of let is equivalent to match e1 with p -> e2
let [x] = [1] in 1::x (* evaluates to [1;1] *) let h::_ = [1;2;3] in h (* evaluates to 1 *) let _ = print_int 5 in 3 (* evaluates to 3 *)
CS 314 – Spring 2022 48

Updating the Interpreter
let rec eval env e =
match e with
Ident x -> lookup env x
| Val v -> v
| Plus (e1,e2) ->
let Int n1 = eval
let Int n2 = eval
let n3 = n1+n2 in
| Let (x,e1,e2) ->
let v1 = eval env e1 in
let env’ = extend env x v1 in let v2 = eval env’ e2 in v2
| Eq0 e1 ->
let Int n = eval env e1 in
CS 314 Spring 2022
if n=0 then Bool true
| If (e1,e2,e3) ->
let Bool b = eval env
if b then eval env e2
else eval env e3
else Bool false
Basically eq0 in th
both rules for is one snippet
Both if rules here

Scaling up – A;e⇒v
Operational semantics (and similarly styled typing rules) can handle full languages
• With records, recursive variant types, objects, first- class functions, and more
Provides a concise notation for explaining what a language does. Clearly shows:
• Evaluation order
• Call-by-value vs. call-by-name
• Static scoping vs. dynamic scoping
• … We may look at more of these later
CS 314 Spring 2022 50

Scaling up – A;e⇒v
CS 314 Spring 2022 51

Scaling up
let mult_sum (x, y) = let z = x + y in fun w -> w * z
let v = mult_sum (1, 2) let res = v 5
VClosure (env, None, “w”, Mul (Var “w”, Var “z”))
CS 314 Spring 2022 52
A = {z=3; y = 2; x = 1}

Quick Look: Type Checking
Inference rules can also be used to specify a program’s static semantics
• I.e., the rules for type checking
We may not cover this in depth in this course, but here is a flavor.
Types t ::= bool | int
Judgment ⊢e:t saysehas typet
• We define inference rules for this judgment, just as with the operational semantics
CS 314 Spring 2022 53

Some Type Checking Rules
Boolean constants have type bool Equality checking has type bool too
• Assuming its target expression has type int Conditionals
CS 314 Spring 2022 54
⊢ true : bool
⊢ false : bool
⊢eq0e:bool
⊢e1:bool ⊢e2:t ⊢e3:t
⊢ife1thene2elsee3 :t

Handling Binding
What about the types of variables?
• Taking inspiration from the environment-style operational semantics, what could you do?
Change judgment to be G ⊢ e : t which says e has type t under type environment G
• Gisamapfromvariablesxtotypest
Ø Analogous to map A, but maps vars to types, not values
What would be the rules for let, and variables? CS 314 Spring 2022 55

Type Checking with Binding
Variable lookup analogous to
Let binding
analogous to
G ⊢e1:t1 G

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts