Denotational Semantics - Compositionality

Compositionality

An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example consider the expression "7 + 4". Compositionality in this case is to provide a meaning for "7 + 4" in terms of the meanings of "7", "4" and "+".

A basic denotational semantics in domain theory is compositional because it is given as follows. We start by considering program fragments, i.e. programs with free variables. A typing context assigns a type to each free variable. For instance, in the expression (x + y) might be considered in a typing context (x:nat,y:nat). We now give a denotational semantics to program fragments, using the following scheme.

1. We begin by describing the meaning of the types of our language: the meaning of each type must be a domain. We write 〚τ〛 for the domain denoting the type τ. For instance, the meaning of type nat should be the domain of natural numbers: 〚nat〛=ℕ_⊥.
2. From the meaning of types we derive a meaning for typing contexts. We set 〚 x₁:τ₁,..., x_n:τ_n〛 = 〚 τ₁〛× ... ×〚τ_n〛. For instance, 〚x:nat,y:nat〛= ℕ_⊥×ℕ_⊥. As a special case, the meaning of the empty typing context, with no variables, is the domain with one element, denoted 1.
3. Finally, we must give a meaning to each program-fragment-in-typing-context. Suppose that P is a program fragment of type σ, in typing context Γ, often written Γ⊢P:σ. Then the meaning of this program-in-typing-context must be a continuous function 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛. For instance, 〚⊢7:nat〛:1→ℕ_⊥ is the constantly "7" function, while 〚x:nat,y:nat⊢x+y:nat〛:ℕ_⊥×ℕ_⊥→ℕ_⊥ is the function that adds two numbers.

Now, the meaning of the compound expression (7+4) is determined by composing the three functions 〚⊢7:nat〛:1→ℕ_⊥, 〚⊢4:nat〛:1→ℕ_⊥, and 〚x:nat,y:nat⊢x+y:nat〛:ℕ_⊥×ℕ_⊥→ℕ_⊥.

In fact, this is a general scheme for compositional denotational semantics. There is nothing specific about domains and continuous functions here. One can work with a different category instead. For example, in game semantics, the category of games has games as objects and strategies as morphisms: we can interpret types as games, and programs as strategies. For a simple language without general recursion, we can make do with the category of sets and functions. For a language with side-effects, we can work in the Kleisli category for a monad. For a language with state, we can work in a functor category. Milner has advocated modelling location and interaction by working in a category with interfaces as objects and bigraphs as morphisms.