Next: Recursive Definition Up: Mathematics Libraries Previous: Real Analysis

# Denotational Semantics

This section presents a constructive   denotational semantics theory for a simple program language where meaning is given as a stream  of states. The following definitions and theorems illustrate this library.

The data type Program is built from a dozen type definitions like those which follow.

```Atomic_stmt  == Abort | Skip | Assignment
```
```Program      == (depth:N # Statement(depth))
```
```Statement(<d>) ==
ind(<d>; x,y.void; void; x,T. Atomic_stmt |
(T#T) *concat* | (expr#T) *do loop* |
expr#T#T *if then else*)
```

The type for stream of states, S, is defined below. Note that the ind form in the definition of Statement approximates a type of trees, while N->State approximates a stream of states. The intended meaning for S is that given an initial state, its value on n is the program state after executing n steps.

```State*   == Identifier -> Value
```
```Done     == {x:atom | x="done" in atom}
```
```State    == State* | Done
<st:State> terminated ==
decide(<st>; u.void; u.int)
```
```S        ==
{f: State -> N -> State |
All a:State, n:N.
f(a)(n) terminated => f(a)(n+1) terminated}
```

Figure presents the various meaning functions as extracted objects. Using these definitions, one can define a meaning function, M, for programs. This is done in figure in the definition of M, the meaning function for programs. With M one can reason about programs as well as executing them directly using the evaluation mechanism.

Figure: A Constructive Theory of Denotational Semantics

Figure: A Constructive Meaning Function for Programs

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995