Editing Denotational semantics (section)

==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'':{{code|nat}},''y'':{{code|nat}}). We now give a denotational semantics to program fragments, using the following scheme.
#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 {{code|nat}} should be the domain of natural numbers: 〚{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>.
#From the meaning of types we derive a meaning for typing contexts. We set 〚 ''x''<sub>1</sub>:τ<sub>1</sub>,..., ''x''<sub>n</sub>:τ<sub>n</sub>〛 = 〚 τ<sub>1</sub>〛× ... ×〚τ<sub>n</sub>〛. For instance, 〚''x'':{{code|nat}},''y'':{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>. As a special case, the meaning of the empty typing context, with no variables, is the domain with one element, denoted 1.
#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:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub> is the constantly "7" function, while 〚''x'':{{code|nat}},''y'':{{code|nat}}⊢''x''+''y'':{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub> is the function that adds two numbers.

Now, the meaning of the compound expression (7+4) is determined by composing the three functions 〚⊢7:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, 〚⊢4:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, and 〚''x'':{{code|nat}},''y'':{{code|nat}}⊢''x''+''y'':{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub>.

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 (mathematics)|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|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]]. [[Robin Milner|Milner]] has advocated modelling location and interaction by working in a category with interfaces as objects and ''[[bigraphs]]'' as morphisms.<ref>{{cite book |first=Robin |last=Milner |title=The Space and Motion of Communicating Agents |publisher=Cambridge University Press |year=2009 |isbn=978-0-521-73833-0 }} [https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf 2009 draft] {{webarchive|url=https://web.archive.org/web/20120402095417/https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf |date=2012-04-02 }}.</ref>