Semantics
1 / 21
Outline
What is semantics?
Denotational semantics
Semantics of naming
What is semantics? 2 / 21
What is the meaning of a program?
Recall: aspects of a language
• syntax: the structure of its programs
• semantics: the meaning of its programs
What is semantics? 3 / 21
How to define the meaning of a program? Formal specifications
• denotational semantics: relates terms directly to values
• operational semantics: describes how to evaluate a term
• axiomatic semantics: defines the effects of evaluating a term • …
Informal/non-specifications
• reference implementation: execute/compile program in some implementation • community/designer intuition: how people think a program should behave
What is semantics?
4 / 21
Advantages of a formal semantics
What is semantics?
5 / 21
A formal semantics . . .
• is simpler than an implementation, more precise than intuition
• can answer: is this implementation correct?
• supports the definition of analyses and transformations • prove properties about the language
• prove properties about programs
• promotes better language design
• better understand impact of design decisions
• apply semantic insights to improve the language design (e.g. compositionality)
Outline
What is semantics?
Denotational semantics
Semantics of naming
Denotational semantics 6 / 21
Denotational semantics
A denotational semantics relates each term to a denotation
an abstract syntax tree
a value in some
semantic domain
Semantic function
· : abstract syntax → Semantic function in Haskell
eval :: Term -> Value
semantic domain
Denotational semantics
7 / 21
Semantic domains
Semantic domain: captures the set of possible meanings of a program/term what is a meaning? — it depends on the language!
Example semantic domains
Language
Boolean expressions
Arithmetic expressions Imperative language SQL query
MiniLogo program MIDI
Meaning Boolean value
Integer
State transformation Set of relations Drawing
Music performance
Denotational semantics
8 / 21
Defining a language with denotational semantics
Denotational semantics
9 / 21
1. Define the abstract syntax, T the set of abstract syntax trees
2. Identify or define the semantic domain, V the representation of semantic values
3. Define the semantic function, · : T → V the mapping from ASTs to semantic values
Example encoding in Haskell:
data Term = …
type Value = …
eval :: Term -> Value
Example: simple arithmetic expressions
1. Define abstract syntax 3. Define the semantic function
data Exp = Add Exp Exp
| Mul Exp Exp
| Neg Exp
| Lit Int
2. Identify semantic domain
Use the set of all integers, Int
eval :: Exp ->
eval (Add l r)
eval (Mul l r)
eval (Neg e)
eval (Lit n)
Int
= eval l + eval r
= eval l * eval r
= negate (eval e)
= n
Denotational semantics
10 / 21
Desirable properties of a denotational semantics
Compositionality: a program’s denotation is built from the denotations of its parts • supports modular reasoning, extensibility
• supports proof by structural induction
Completeness: every value in the semantic domain is denoted by some program • if not, language has expressiveness gaps, or semantic domain is too general • ensures that semantic domain and language align
Soundness: two programs are “equivalent” iff they have the same denotation • equivalence: same w.r.t. to some other definition
• ensures that the denotational semantics is correct
Denotational semantics
11 / 21
More on compositionality
Compositionality: a program’s denotation is built from the denotations of its parts an AST sub-ASTs
Example: What is the meaning of op e1 e2 e3?
1. Determine the meaning of e1, e2, e3
2. Combine these submeanings in some way specific to op
Implications:
• The semantic function is probably recursive
• Often need different semantic functions for each syntactic category (type of AST)
Denotational semantics
12 / 21
Example: simple arithmetic expressions (again)
1. Define abstract syntax 3. Define the semantic function
data Exp = Add Exp Exp
| Mul Exp Exp
| Neg Exp
| Lit Int
2. Identify semantic domain
Use the set of all integers, Int
eval :: Exp ->
eval (Add l r)
eval (Mul l r)
eval (Neg e)
eval (Lit n)
Int
= eval l + eval r
= eval l * eval r
= negate (eval e)
= n
Denotational semantics
13 / 21
Example: move language
A language describing movements on a 2D plane
• a step is an n-unit horizontal or vertical movement • a move is described by a sequence of steps
Abstract syntax
dataDir =N|S|E|W data Step = Go Dir Int type Move = [Step]
[Go N 3, Go E 4, Go S 1]
Denotational semantics
14 / 21
Semantics of move language
1. Abstract syntax 3. Semantic function (Step)
dataDir =N|S|E|W data Step = Go Dir Int type Move = [Step]
2. Semantic domain
type Pos = (Int,Int) Domain: Pos -> Pos
step::Step->Pos->Pos
step (Go N k) = \(x,y) -> (x,y+k) step (Go S k) = \(x,y) -> (x,y-k) step (Go E k) = \(x,y) -> (x+k,y) step (Go W k) = \(x,y) -> (x-k,y)
3. Semantic function (Move)
move :: Move -> Pos -> Pos
move [] = \p -> p
move (s:m) = move m . step s
Denotational semantics
15 / 21
Alternative semantics
Often multiple interpretations (semantics) of the same language
Example: Database schema Distance traveled
Onedeclarativespec,usedto: • initialize the database
• generate APIs
• validate queries
• normalize layout • …
type Dist = Int
dstep :: Step -> Int
dstep (Go _ k) = k
dmove :: Move -> Int
dmove [] = 0
dmove (s:m) = dstep s + dmove m
Combined trip information
trip :: Move -> Pos -> (Dist, Pos)
trip m = \p -> (dmove m, move m p)
Denotational semantics
16 / 21
Picking the right semantic domain (1/2)
Simple semantic domains can be combined in two ways:
• sum: contains a value from one domain or the other • e.g. IntBool language can evaluate to Int or Bool • use Haskell Either a b or define a new data type
• product: contains a value from both domains
• e.g. combined trip information for move language • use Haskell (a,b) or define a new data type
Denotational semantics
17 / 21
Picking the right semantic domain (2/2)
Can errors occur?
• use Haskell Maybe or define a new data type
Does the language manipulate state or use names? • use a function type
Example stateful domains
Denotational semantics
18 / 21
Read-onlystate: Modify as only effect: Modify as side effect:
State -> Value
State ->
State ->
State
(State,Value)
Outline
What is semantics?
Denotational semantics
Semantics of naming
Semantics of naming 19 / 21
What is naming?
Most languages provide a way to name and reuse stuff
Naming concepts C/Java variables
declaration binding reference
In Haskell:
introduce a new name associateanamewithathing usethenametostandfortheboundthing
int x; int y;
x = slow(42);
y = x + x + x;
Local variables Type names
Function parameters
area r = pi * r * r
let x = slow 42
in x + x + x
type Radius = Float
data Shape = Circle Radius
Semantics of naming
20 / 21
Semantics of naming
Environment: a mapping from names to things type Env = Name -> Thing Naming concepts
declaration binding reference
add a new name to the environment set the thing associated with a name get the thing associated with a name
Example semantic domains for expressions with . . .
We’ll come back to mutablevariablesin unit on scope
Semantics of naming
21 / 21
immutablevars(Haskell) mutable vars (C/Java/Python)
Env -> Val
Env -> (Env,Val)