Denotational Semantics

Slonneger & Kurtz 9.1 - 9.3, 9.4

Map syntactic objects into domains of mathematical objects.

meaning: Syntax -> Semantics 

Semantics

• semantic domain - some notation for talking about meaning
• semantic meaning - maps syntatic elements to the semantic domain

In denotational semantics the syntactic domain is the elements of the abstract syntax of a language. The semantic domain consists of abstract mathematical objects (integers, booleans, lists, functions, etc). Semantic functions map elements of syntatic domain to semantic domain.

There is also

• Translational semantics- mapping programs in a source language to programs in a target language (think compilers)
• Axiomatic semantics- mapping programs to sets of Hoare triples (or the related notion of weakest preconditions)

A fundamental principle of denotational semantics is that the definition be compositional. The denotation of a language construct is defined in terms of the denotations of its subphrases.

Denotational definitions use special brackets, [[ ]], to separate the syntactic world from the semantic world.

Example:

meaning[[2 * 4]] = meaning[[(5 + 3)]] = meaning[[ 008 ]] = meaning [[8]] = 8

Example with binary digits. Let semantic domain be the natural numbers, and the abstract syntax be

BinLit ::= Digit | BinLit Digit
Digit ::= 0 | 1

for semantic functions

val: BinLit -> N
dval: Digit -> N

We can say

dval [[ 0 ]] = 0
dval [[ 1 ]] = 1
val [[ B ]] = dval [[ D ]]
val [[ B D ]] = 2 * val [[ B ]] + dval [[ D ]]

Then val [[ 101 ]] = 2 * val [[ 10 ]] + dval [[ 1 ]] = 2 * (2 * val [[ 1 ]] + dval [[ 0 ]]) + 1 = 2 * (2 * dval [[ 1 ]]) + 1 = 5.