Programming Languages

G22.2110 Summer 1998

 

Class #11

Denotational Semantics

 

 

Contents

 

C11.0. Current Assignments, PL Project #3

C11.1. Formal Semantics

C11.2. Denotational Semantics

C11.3. Language of Decimal Numerals

C11.4. Language of Regular Expressions

C11.5. Language of Propositional Logic

C11.6. Language of Simple Expressions

C11.7. Other Languages

 

C11.0. Current Assignments, PL Project #3

 

PL Project Part III due 8/3/98.

 

C11.1. Formal Semantics

 

Meaning of languages should be:

Complete

Consistent

Precise

Unambiguous

Concise

Understandable

Useful

 

Possible uses of formal semantics:

Standardization of Programming Languages

References for users

Proof of program correctness

Reference for implementors

Automatic implementation

Better understanding of language design

 

Approaches to formal semantics to programming languages:

Operational semantics

Define an abstract machine with primitive instructions

The semantic description of the PL specifies a translation into this code

Denotational semantics

Give functions that map computer programs to the abstract mathematical values

they denote (numbers, truth values, functions, etc.)

Axiomatic semantics

Define the action of a program construct by the logical properties that hold of the

state of the computer before and after the execution of the construct.

Algebraic semantics

Consider objects of computation to be terms in multi-sorted algebras.

Programs implement functions that can be expressed by equations between

terms.

Structured operational semantics or natural semantics

Programs are given meaning by derivation rules that describe the evaluation of

the constructs in the language.

 

C11.2. Denotational Semantics

 

Denotational approach associates mathematical denotations to syntactical parts of the languages.

 

Proceed in four steps:

Give the syntactic categories

Define the (abstract) syntax of the language

Give the value domains

Define functions that map each syntactic object to some semantic value

 

C11.3. Language of Decimal Numerals

 

Syntactic categories:

 

D Î Digits the decimal digits

N Î Num decimal numerals

 

Syntax of decimal numerals (BNF):

 

D ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

N ::= D | ND

 

Mathematical denotations of decimal numerals come from the set of natural numbers:

 

Nat = {0, 1, 2 , } natural numbers (only value domain required)

 

Semantic functions:

 

D : Digits -> Nat

M : Num -> Nat

 

Following equations define the two semantic functions inductively:

 

D[0] = 0

D[1] = 1

D[9] = 9

M[D] = D[D]

M[ND] = 10 x M[N] + M[D]

C11.4. Language of Regular Expressions

 

Syntactic categories:

 

A Î Alpha the alphabet

R Î RE regular expressions

 

Abstract syntax of regular expressions:

 

R ::= A | Æ | (R + R) | (R . R) | R*

 

Value domains:

Lang formal languages (set of strings over Alpha)

 

Semantic functions:

 

A : Alpha -> Lang

D : RE -> Lang

 

Definition of semantic functions:

 

A[A] = {A}

D[A] = A[A]

D[Æ ] = { }

D[(R1 + R2)] = D[R1] È D[R2]

D[(R1 . R2)] = {x . y | x Î D[R1] & y Î D[R2]}

D[R*] = È ( i ) (D[R])i

 

e.g., alphabet containing symbols a and b, D[(Æ + a)] = D[Æ ] È D[a] = {a}, and D[a . Æ ] = { }.

 

C11.5. Language of Propositional Logic

 

Syntactic categories:

 

P Î Prop propositions

F Î Form formulas

 

Formulas syntax:

 

F ::= P | Ø F | F Þ F

 

Value domains:

Bool = { True, False } boolean values

r Î Assign = P -> Bool assignments (reveals if a proposition is true or not)

 

Semantic functions:

 

M : Form -> Assign -> Bool

 

Definition of M:

 

M[P]r = r (P)

M[Ø F]r = Ø M[F]r

M[F1 => F2]r = Ø M[F1]r Ú M[F2]r

 

C11.6. Language of Simple Expressions

 

Syntactic categories:

I Î Ident identifiers

E Î Exp expressions

 

Language syntax:

 

E ::= 0 | 1 | I | (E1 + E2) | (E1 - E2) | let I = E1 in E2 end

 

Value domains:

 

Int = { , -2, -1, 0, 1, 2, } integers

r Î Env = Ident -> Int environments

 

Semantic functions:

e : Exp -> Env -> Int

 

Function definitions:

e [0]r = 0

e [1]r = 1

e [I]r = r (I)

e [E1 + E2]r = e [E1]r + e [E2]r

e [E1 - E2]r = e [E1]r - e [E2]r

 

e [let I = E1 in E2 end]r = e [E2](r [I -> e [E1]r ])

 

f[x -> y] means that the function f is modified so that f(x) = y.

 

e.g., in ML

fun Update (f, x, y) (x0) = if x0 =x then y else f(x0)

 

C11.7. Other Languages

 

Language with Error Values

Language with State

Language with Commands

Language Combining Expressions and Commands

Language with Function Calls

Language with goto