3 Semantics
CS 381 • Semantics
1
en.wikipedia.org/wiki/Blissymbols
Semantics
3 Semantics
CS 381 • Semantics
Syntax
2
CS 381 • Semantics
3
3 Semantics
Why semantics?
What is semantics?
Semantics of simple expression languages Elements of semantic definitions
Examples: Shape & Move languages
Advanced semantic domains
Translating Haskell into denotational semantics Haskell as a metalanguage
Modus Ponens
S⟶G S G
Why Semantics ?
If this statement is true, then God exists
If this statement is true, then God does not exist
If this statement is true, then Facebook protects your privacy
Curry’s Paradox
Prior, A. N., 1955.“Curry’s Paradox and 3-Valued Logic”, Australasian Journal of Philosophy 33:177-82
See also: John Allen Paulos: Irreligion, Hill and Wang 2008 CS 381 • Semantics
Haskell B. Curry, 1900-1982
4
Why Semantics ?
Recursion without a base case
S = If S is true, then God exists
S = If S is true, then God does not exist
S = If S is true, then Facebook protects your privacy
CS 381 • Semantics
5
Why Semantics ?
Access to non-local variables
{
int x=2;
int f(int y) {return y+x;};
{
int x=4;
printf(“%d”, f(3));
}
CS 381 • Semantics
6
}
Output? 5
Why Semantics ?
Swap the values of two variables ✓ {
What?!
{
int x=1;
int y=8;
y = x + 0*(x = y);
}
Effect?
{
int x=1;
int y=8;
y = x;
x = y; }
Effect? CS 381 • Semantics
int x=1;
int y=8;
int z;
z = y;
y = x;
x = z;
}
Effect?
y: 1 x: 1
y: 1 x: 8
y: 1 x: 8
7
Why Semantics ? •Understand what program constructs do
•Judge the correctness of a program (compare expected with observed behavior)
•Prove properties about languages
• Compare languages Syntax: Form of programs
CS 381 • Semantics
8
• Design languages Semantics: Meaning of programs •Specification for language implementations
The Meaning of Programs
What is the meaning of a program?
It depends on the language!
Language
Meaning
Boolean expressions
Boolean value
Arithmetic expressions
Integer
Imperative Language
State transformation
Logo
Picture
CS 381 • Semantics
Denotational Semantics of a language: Transformation of representation (abstract syntax → semantic domain)
9
CS 381 • Semantics
10
Simple Examples
BoolSyn.hs BoolSem.hs
ExprSyn.hs ExprSem.hs
CS 381 • Semantics
11
Exercises
(1) Extend the boolean expression language by an and operation (abstract syntax and semantics)
(2) Extend the arithmetic expressions by multiplication and division (abstract syntax and semantics)
(3) Define a Haskell function to apply DeMorgan’s laws to boolean expression, i.e., a function to transform any expression not (x and y) into (not x) or (not y) (and accordingly for not (x or y))
Defining Semantics in 3 Steps Example Language
(1) Define the abstract syntax S, i.e. set of syntax trees
(2) Define the semantic domain D,
i.e. the representation of semantic values
“Arithmetic expressions”
S: Expr
D: Int
⟦⋅⟧: sem :: Expr → Int
(3) Define the semantic function / valuation ⟦⋅⟧ : S → D that maps trees to semantic values
CS 381 • Semantics
12
Language Definitions
Language
Definition Profile
Language
Aspect
Metalanguage
Definiittioionn
CS 381 • Semantics
13
Aspect
Metalanguage
Example Expression Language
Expr
Semantics
Haskell
Expr
Syntax
Haskell
data Expr = N Int
| Plus Expr Expr
| Neg Expr
Semantic Domain
sem :: Expr → Int
sem (N i) = i
sem (Plus e e’) = sem e + sem e’
sem (Neg e)
= -(sem e)
Expr
Semantics
Math
Semantic Function
Expr
Syntax
Grammar
::= | | CS 381 • Semantics
Syntactic Symbol
· :
=
= + =
Semantic Operation
14
Related: Expressions vs.Values
tail [1 .. 4]
✗ or [2 .. 4]
8
2:3:4:[]
semantics
[2,3,4]
3+5
semantics ✗ 2+6
Gottlob Frege:
Sense vs. Reference
3*5 and 5+5+5 have different
sense (meaning) but the same referent
CS 381 • Semantics
15
Example: Shape Language
A language for constructing bitmap images: an image is either a pixel or a vertical or horizontal composition of images
CS 381 • Semantics
Operation TD s1 s2 puts s1 on top of s2 =
=
Operation LR s1 s2 puts s1 left next to s2
16
Abstract Syntax
data Shape = X
| TD Shape Shape
| LR Shape Shape
Example:
LR (TD X X) X
TD X (LR X X)
TD (LR X X) X
LR aligns at bottom TD aligns at left
… part of semantics
CS 381 • Semantics
17
Semantic Domain
data Shape = X
| TD Shape Shape
| LR Shape Shape
LR (TD X X) X
How to represent a bitmap image?
type Image = Array (Int,Int) Bool Drawback: size is fixed, operations
require complicated bit shifting
[(1,1),(1,2),(2,1)]
CS 381 • Semantics
18
semantics
type Pixel = (Int,Int)
type Image = [Pixel]
Semantic Function (1) Approach:Translate individual shapes separately
into pixel lists and then compose pixel lists
semantics
Base case: Individual pixel
data Shape = X
| TD Shape Shape
| LR Shape Shape
type Pixel = (Int,Int)
type Image = [Pixel]
CS 381 • Semantics
19
sem :: Shape -> Image
sem X = [(1,1)]
Semantic Function (2)
How can we compose (horizontally and vertically) two pixel lists images without overlapping?
Take bounding boxes and adjust y-coordinates of top shape by height of bottom shape
sem (TD s1 s2) = adjustY ht p1 ++ p2 where p1 = sem s1
p2 = sem s2
ht = maxY p2
CS 381 • Semantics
20
Semantic Function (3)
sem (TD s1 s2) = adjustY ht p1 ++ p2 where p1 = sem s1
p2 = sem s2
ht = maxY p2
adjustY :: Int -> [(Int,Int)] -> [(Int,Int)]
adjustY ht p = [(x,y+ht) | (x,y) <- p]
CS 381 • Semantics
21
maxY :: [(Int,Int)] -> Int
maxY p = maximum (map snd p)
sem (TD s1 s2) = adjustY ht p1 ++ p2 where p1 = sem s1
p2 = sem s2
ht = maxY p2
Exercise
Define the functions:
sem (LR s1 s2) maxX adjustX
maxY :: [(Int,Int)] -> Int
maxY p = maximum (map snd p)
adjustY :: Int -> [(Int,Int)] -> [(Int,Int)]
adjustY ht p = [(x,y+ht) | (x,y) <- p]
sem (LR s1 s2) = p1 ++ adjustX wd p2 where p1 = sem s1
p2 = sem s2
wd = maxX p1
maxX :: [(Int,Int)] -> Int
maxX p = maximum (map fst p)
adjustX :: Int -> [(Int,Int)] -> [(Int,Int)]
adjustX wd p = [(x+wd,y) | (x,y) <- p]
CS 381 • Semantics
22
CS 381 • Semantics
23
Example
Shape.hs ShapePP.hs
Example: Move Language
A language describing vector-based movements in the 2D plane. A step is an n-unit horizontal or vertical move,
a move is a sequence of steps.
Go Up 3; Go Right 4; Go Down 1
CS 381 • Semantics
24
Abstract Syntax
dataDir =Lft|Rgt|Up|Dwn data Step = Go Dir Int
type Move = [Step]
Example:
[Go Up 3, Go Rgt 4, Go Dwn 1]
CS 381 • Semantics
25
(1) Give a type definition for the data type Step
data Step = Go Dir Int
(2) Define the data type Move
without using built-in lists
type Step = (Dir,Int)
Exercises
data Move = One Step
| Seq Step Move
type Move = [Step]
(3) Write the move [Go Up 3, Go Rgt 4, Go Dwn 1]
using the representation from (1) and(2)
(Up,3) `Seq` (Rgt,4) `Seq` One (Dwn,1)
CS 381 • Semantics
Seq (Up,3) (Seq (Rgt,4) (One (Dwn,1)))
26
Semantic Domain
dataDir =Lft|Rgt|Up|Dwn data Step = Go Dir Int
type Move = [Step]
[Go Up 3, Go Rgt 4, Go Dwn 1]
What is the meaning of a move? The distance traveled, the
final position, or both.
type Pos = (Int,Int)
semantics (4,2)
CS 381 • Semantics
27
Semantic Function
sem :: Move -> Pos
sem [] = (0,0)
sem (Go d i:ss) = (dx*i+x,dy*i+y)
where (dx,dy) = vector d (x,y) = sem ss
pattern matching in definitions
vector :: Dir -> (Int,Int)
vector Lft = (-1,0)
vector Rgt = (1,0)
vector Up = (0,1)
vector Dwn = (0,-1)
CS 381 • Semantics
28
CS 381 • Semantics
29
Example Move.hs
Exercises Define the semantic function for the
sem :: Move -> Pos
sem [] = (0,0)
sem (Go d i:ss) = (dx*i+x,dy*i+y)
where (dx,dy) = vector d (x,y) = sem ss
move language for the semantic domain Define the semantic function for the
type Dist = Int
move language for the semantic domain type Trip = (Dist,Pos) CS 381 • Semantics
30
CS 381 • Semantics
31
Advanced Semantic Domains The story so far: Semantic domains were mostly simple types
(such as Int or [(Int,Int)])
How can we deal with language features, such as
errors, union types, or state?
(1) Errors: Use the Maybe data type
(2) Union types: Use corresponding data types (3) State: Use function types
Error Domains
If T is the type representing “regular” values, define the semantic domain as Maybe T
regular value error value
data Maybe a = Just a | Nothing type of regular values
CS 381 • Semantics
32
CS 381 • Semantics
33
Example ExprErr.hs
Union Domains
If T1 … Tk are types representing different semantic values for different
nonterminals, define the semantic domain as a data type with k constructors.
semantic domain
different types of result values
data T = C1 T1
| …
| Ck Tk
CS 381 • Semantics
34
Special Case: Binary Union Domains
If T1 and T2 are types representing different semantic values for different nonterminals, define the semantic domain as a data type with 2 constructors.
Or: Use the Either data type.
data Either a b = Left a | Right b
type T = Either T1 T2
type Val = Either Int Bool
CS 381 • Semantics
35
data T = C1 T1 | C2 T2
data Val = I Int
| B Bool
CS 381 • Semantics
36
Example Expr2.hs
(1) Extend the semantic domain for the two-type expression language to include errors
type ValE = Maybe Val Or:
Exercises
data Val = I Int
| B Bool
| Error
CS 381 • Semantics
37
data Val = I Int
| B Bool
(2) Extend the semantic function for the two-type expression language to handle errors
Function Domains
If a language operates on a state that can be represented by a type T,
define the semantic domain as a function type T -> T type D = T -> T
sem :: S -> D
= sem :: S -> (T -> T)
= sem :: S -> T -> T
Semantic function takes state as an additional argument
CS 381 • Semantics
38
CS 381 • Semantics
39
Example RegMachine.hs
Exercises
data Op = LD Reg Int | INC Reg
| DUP Reg data Reg = A | B
(1) Extend the machine language to work on two registers A and B
(2) Define a new semantic domain for the extended language
(3) Define the semantics functions for the extended language
type RegCont = Int
type D = RegCont -> RegCont
CS 381 • Semantics
40
data Op = LD Int
| INC
| DUP
type RegCont = (Int,Int)
RegMachine2.hs
CS 381 • Semantics
41
Zoom Poll
Semantic Domain
Translating Haskell into Mathematical Denotational Semantics
(1) Replace type definitions by sets (should actually be CPOs)
(2) Replace patterns by grammar productions (and replace nonterminals by variables) (3) Replace function names by semantic brackets that enclose only syntactic objects
Expr
Semantics
Math
Expr
Semantics
Haskell
sem :: Expr → Int sem (N i) = i
sem (Neg e)
CS 381 • Semantics
➌
= ➌
::= | |
42
➊
· : ➊
➋ =
➋ = +
sem (Plus e e’) = sem e + sem e’
= -(sem e)
Haskell as a Mathematical Metalanguage
Grammars
(Languages)
2 Syntax
Data Types
Math World
(Semantic domains)
Functions
(Semantics)
3 Semantics
Functions
Sets
CS 381 • Semantics
= Executable Math World
Data Types
Haskell World
43