VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 489

3.3 Denotations

Let us first recall how Scott and Strachey defined denotations in their joint paper
in 1971 [3], before reviewing the more commonly-used continuation passing style.

Direct Semantics. Scott and Strachey's choice of denotations is called direct
semantics. The basic idea is that denotations of commands are functions from
environments to store transformers. The semantic function

C maps commands

to their denotations:

C : Cmd → Env → S → S (2)

Similarly, the denotations of expressions (whose evaluations might have side-
effects) should be functions from environments to value-returning store trans-
formers. The semantic function

E maps expressions to their denotations:

E : Exp → Env → S → V × S (3)

Thanks to the use of combinators, the denotations of various commands and
expressions can be defined without explicit reference to the store σ :

C [[ γ 0 ; γ 1 ]] = λρ. C [[ γ 1 ]] ( ρ ) ◦C [[ γ 0 ]] ( ρ ) (4)

C

[[ ε -> γ 0 , γ 1 ]] = λρ. ( λβ.Cond (

C

[[ γ 0 ]] ( ρ ) ,

C

[[ γ 1 ]] ( ρ )( β

| T )) ∗E

[[ ε ]] ( ρ ) (5)

However, Scott and Strachey were apparently not satisfied with the relatively
complicated notation required for expressing the denotations of assignment com-
mands, and resorted to an informal explanation of the steps involved. Here is
how they could have written the formal definition: 3

C [[ ε 0 := ε 1 ]] = λρ. ( λβ 0 . ( λβ 1 .Assign ( β 0 | L, β 1 )) ∗E [[ ε 1 ]] ( ρ )) ∗E [[ ε 0 ]] ( ρ ) (6)

Reading the above equation operationally involves associating the values com-
puted by the expressions ε 0 and ε 1 with the λ -abstractions on β 0 and β 1 ,which
is not immediately obvious without close inspection of the grouping of the term.
Suppose, however, that we were to use variants ˆ

◦ and ˆ ∗ of the combinators ◦

and ∗ , taking their operands in the reverse order:

- reverse composition f ˆ ◦ g = λa.g ( f ( a )):

f ˆ ◦ g : A → C when f : A → B and g : B → C ;

- reverse composition f ˆ ∗ g = λa. ( λb.g ( M 0 b )( M 1 b ))( f ( a )):

f ˆ ∗ g : A → C when f : A → B 0 × B 1 and g : B 0 → B 1 → C .

The above definitions of denotations can now be written thus:

C [[ γ 0 ; γ 1 ]] = λρ. C [[ γ 0 ]] ( ρ ) ˆ ◦C [[ γ 1 ]] ( ρ ) (7)

C [[ ε -> γ 0 , γ 1 ]] = λρ. E [[ ε ]] ( ρ ) ˆ ∗ λβ.Cond ( C [[ γ 0 ]] ( ρ ) , C [[ γ 1 ]] ( ρ ))( β | T ) (8)

3 Let us assume here that any implicit dereferencing of variables is made explicit in
the abstract syntax of expressions, in order to simplify the examples a bit.