Denotational Semantics

1. Expression Contexts

The set of expression contexts, is defined as:

The symbol () denotes the context hole of the expression context. We write to emphasize the hole of . Some example contexts are:

Given an expression and context , we can fill the hole with to obtain a new expression . This is called context application, and is defined inductively on the structure of as:

(?) What are the uses of expression contexts?

Previously, we had the following four rules for while loops:

Now, with contexts, we can combine W-EXP.LEFT and W-EXP.RIGHT into W-EXP.EITHER:

What does it mean for two expressions to be the same? This is contextual equivalence:

2. Denotational Semantics

Contextual equivalence allows us a succinct way to compare the outcome of two expressions, but it does not describe what the expression does.

Denotational semantics describe the meaning of a program with a mathematical object. The denotational semantics of are defined as , where is the interpretation, and is the semantic domain of simple expressions. We define the interpretation of simple expressions as:

The semantic is compositional - the meaning of a compound expression is given in terms the meanings of its subexpressions.

(!) Why is compositional semantics important?

It follows that each context determines a function between meanings, or . Consequently, , and hence .

(!) Proof is associative

Using compositional semantics, we can prove that is associative, i.e. :

Take arbitrary :

As such, denotational semantics of give rise to the following theorems:

2.1 While Denotational Semantics

Let be the set of all states, and . The semantic domain of commands is given by the set of state transformers defined as - a set of total functions that take an initial state, and either return a final state or , indicating the program is stuck or looped forever. Similarly:

Hence:

Definition of

is defined compositionally on the structure of as:

Where:

  • Lookup
  • Addition

Definition of

is defined compositionally on the structure of as:

Where:

  • Assignment
  • Skip
  • Sequencing
  • Conditional
  • Iteration

Denotational semantics are compositional. For example, the sequential operator ; has its meaning as function , and hence it is reasonable to say that .

State Transformer for while

We know that . But this is an equation, not a definition. Instead, for a given and , we define . This means that , or is a fixpoint of . To do this, we use domain theory.

Aside: Fixpoint Theorem

Assume a set and function . We are looking for fixpoints of .

  1. Define a sequence of functions where and .
  2. Define a function where
  3. Assume that .

The fixpoint theorem states that is a well defined fixpoint of . Moreover, for any which is a further fixpoint of , we have .

Now, we can:

  1. Define where and .
  2. Define where .
  3. Assume .
  4. By fixpoint theorem, is the well defined smallest fixpoint of . Therefore, .
Back to Home