CS 314: Principles of Programming Languages
Operational Semantics
CS 314 Spring 2022 1
Copyright By Assignmentchef assignmentchef
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 ev
Sayseevaluatestov
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
Thelanguagesexpressionseandvaluesvhave 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 languages 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., es 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 expressions final result is a value. What can values be?
v::=n Just numerals for now
In terms of an interpreters 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.,nn
Suppose e is an addition expression e1 + e2
Ife1evaluateston1,i.e.,e1n1
Ife2evaluateston2,i.e.,e2n2
Theneevaluateston3,wheren3isthesumofn1andn2 I.e.,e1+e2n3
Suppose e is a let expression let x = e1 in e2
Ife1evaluatestov,i.e.,e1v1
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 e2v2
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.,nn
Suppose e is an addition expression e1 + e2 Ife1evaluateston1,i.e.,e1n1
Ife2evaluateston2,i.e.,e2n2
Theneevaluateston3,wheren3isthesumofn1andn2 I.e.,e1+e2n3
e1n1 e2n2 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.,e1v1
Ife2{v1/x}evaluatestov2,i.e.,e2{v1/x}v2
Theneevaluates tov2, i.e.,let x = e1 in e2v2
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
Its 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
e1n1 e2n2 n3isn1+n2
e1 v1 e2{v1/x} v2
letx=e1ine2 v2
Goal: show that letx=4inx+3 7
44 33 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
22 3+811 2+(3+8) 13
11 is 3+8 –
22 3 + 8 11 – 2+(3+8) 13
3 + 8 11 2 2 – 2+(3+8) 13
CS 314 Spring 2022
What is derivation of the following judgment?
2 + (3 + 8) 13
22 3+811 2+(3+8) 13
11 is 3+8 –
22 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
e1n1 e2n2 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
let x = 4 in x + 3
eval Let(x,Num 4, Plus(Ident(x),Num 3))
eval Num 4 4 eval (subst 4 x
Plus(Ident(x),Num 3))
CS 314 Spring 2022 26
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))
eval Num 4 4 eval(Plus(Num 4,Num 3))
CS 314 Spring 2022 27
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
44 33 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
evholds 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|ev}
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;e1v1 A,x:v1;e2v2
A;letx=e1ine2 v2
A;e1n1 A;e2n2 n3isn1+n2
A;e1+e2n3
CS 314 Spring 2022
Derivation of the following judgment?
;letx=3inx+2 5
(,x:3);x3 (,x:3);22 5is3+2
;33 (,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., es 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
Adding Conditionals to Micro-OCaml
e::=x| |e+e|letx=eine v::=n|true|false
In terms of interpreter definitions:
|eq0e |ifetheneelsee
type exp =
| Ident of string
| Plus of exp * exp
| Let of id * exp * exp | Val of value
| Eq0 of exp
| If of exp * exp * exp
type value =
| Int of int
| Bool of bool
CS 314 Spring 2022 43
Rules for Eq0 and Booleans
A; true true
A;eq0etrue
A;ev v=0
A;eq0efalse
A; false false
Booleans evaluate to themselves
A;falsefalse
eq0 tests for 0
A;eq00true
A;eq03+4false
CS 314 Spring 2022 44
Rules for Conditionals
A;e1true A;e2v
A;ife1thene2elsee3 v
A;e1false A;e3v
A;ife1thene2elsee3 v
Notice that only one branch is evaluated
A;ifeq00then3else43 A;ifeq01then3else44
CS 314 Spring 2022 45
What is the derivation of the following judgment? ; if eq0 3-2 then 5 else 1010
; 33 ; 22 3-2is1
; eq0 3-2 false ; 1010 – ;ifeq03-2then5else10 10
–
;3-21 1=0
; eq0 3-2 false ;ifeq03-2then5else10 10
eq0 3-2 false 10 10 if eq0 3-2 then 5 else 1010
CS 314 Spring 2022 46
What is the derivation of the following judgment? ; if eq0 3-2 then 5 else 1010
; 33 ; 22 3-2is1
; eq0 3-2 false ; 1010 – ;ifeq03-2then5else10 10
–
;3-21 1=0
; eq0 3-2 false ;ifeq03-2then5else10 10
eq0 3-2 false 10 10 if eq0 3-2 then 5 else 1010
CS 314 Spring 2022 47
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;ev
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;ev
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 programs 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: assignmentchef QQ: 1823890830 Email: [email protected]
Reviews
There are no reviews yet.