Talk:Denotational semantics/Compositionality in Programming Language

(The following article extract was moved here from the parent discussion. —Piet Delport (talk) 2009-10-22 23:13)

Material in "Compositionality in Programming Language" removed by Sam Staton

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 "8 / 4". Compositionality in this case is to provide a meaning for "8 / 4" in terms of the meanings of "8", "4" and "/".

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:

SimpleCell ≡

serializer

contents

implements Cell

Read< > → return contents

Write<newContents> → return also become(contents=newContents)

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.

Environments

Environments hold the bindings of identifiers. When an environment is sent a Lookup message for an identifier x, it returns the latest (lexical) binding of x.

As an example of how this works consider the lambda expression <L> below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree. When such a tree is given a parameter message "getLeft", it return leftSubTree and likewise when given the message "getRight" it returns rightSubTree.

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

Consider what happens when an expression of the form "(<L> 1 2)" is sent an Eval message with environment E. One semantics for application expressions such as this one is the following: <L>, 1 and 2 are each sent Eval messages with environment E. The integers 1 and 2 immediately reply to the Eval message with themselves.

However, <L> responds to the Eval message by creating a closure C that has a body <L> and environment E. "(<L> 1 2)" then sends C the message [1 2].

When C receives the message [1 2], it creates a new environment F which behaves as follows:

1. When it receives a Lookup message for the identifier leftSubTree, it responds with 1
2. When it receives a Lookup message for the identifier rightSubTree, it responds with 2
3. When it receives a Lookup message for any other identifier, it forwards the Lookup message to E

C then sends an Eval message with environment F to the following:

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

Arithmetic expressions

For another example consider the expression "<expression₁> / <expression₂>" which has the subexpressions <expression₁> and <expression₂>. When the composite expression receives an Eval message with an environment E and a customer C, it sends Eval messages to <expression₁> and <expression₂> with environment E and sends C a newly created C₀. When C₀ has received back two values N₁ and N₂, it sends "/" the message [N₁ N₂] with customer C to perform the division.

Other programming language constructs

The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs. For example it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as delays and futures.

76.254.235.105 (talk) 02:59, 16 September 2009 (UTC)