程序代写代做 go Haskell 3 Semantics

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