Talk:Denotational semantics/Compositionality in Programming Language

Functional approach

A functional approach to denotational semantics in 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, 〚⊢8:nat〛:1→ℕ_⊥ is the constantly "8" function, while 〚x:nat,y:nat⊢x/y:nat〛:ℕ_⊥×ℕ_⊥→ℕ_⊥ is the function that divides two numbers.

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

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 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.

Problems with the functional approach to compostionality in programming languages

Unfortunately, the above is not a general scheme for compositional denotational semantics that is adequate for modern software engineering. An initial difficulty comes with expressions like 8/0. An inital approach was to define a special element of the domain to be an "error element" and have 8/0 denote the error element. However, the error element approach is unsatisfactory for software engineering. One problem is that it becomes necessary for programs to continually test for the error element. Another problem is that the error element approach does not automatically propagate exceptions higher if they are not caught.

An even more serious problem with the above functional approach is that it does not encompass communication and change. Consider the following program in ActorScript:

What is the denotation of the expression "return also become(contents=newContents)" in the above program?

Scott and Strachey [1971] proposed that the semantics of programming languages be reduced to the semantics of the lambda calculus and thus inherit the denotational semantics of the lambda calculus. However, it turned out that general computation could not be implemented in the lambda calculus (see Indeterminacy in concurrent computation). Thus there arose the problem of how to provide modular denotational semantics for general programming languages. One solution to this problem is to use the Eval messages with an environment so that programs obtain their denotational semantics from the methods explained earlier in this article.

General compositionality in programming languages

The general approach to compositonality in programming languages solves the above problems using environments and customers as explained below.

 λ(leftSubTree, rightSubTree)
   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree