Denotational semantics: Difference between revisions

Revision as of 17:42, 24 November 2005

Latest revision as of 00:41, 12 July 2025

(462 intermediate revisions by more than 100 users not shown)

Line 1:

{{short description|Study of programming languages via mathematical objects}}

{{ActiveDiscuss}}

{{Semantics}}

In [[computer science]], '''denotational semantics''' is(initially oneknown ofas the'''mathematical approachessemantics''' toor formalize'''Scott–Strachey semantics''') is an approach of formalizing the [[semantics]]meanings of [[computer system|computerprogramming systemslanguage]]s by constructing [[mathematical objectsobject]]s (called ''denotations'' or ''meanings'') whichthat expressdescribe the semanticsmeanings of these systems. Originally the field was developed more narrowly to deal only with a system that is defined by a [[Expression (computer programscience)|expressions]]. Laterfrom the fieldlanguages. broadenedOther toapproaches include systems not defined by a single program as found inproviding [[networking]]formal andsemantics [[concurrentof systemsprogramming languages]]. The field originated in work byinclude [[Christopheraxiomatic Stracheysemantics]] and [[Danaoperational Scott]] in the [[1960ssemantics]].

Other approaches include [[axiomatic semantics]] and [[operational semantics]]. (See [[formal semantics of programming languages]].)

Broadly speaking, denotational semantics is concerned with finding mathematical objects called [[___domain theory|domains]] that represent what programs do. For example, programs (or program phrases) might be represented by [[partial function]]s<ref name="ropas.snu.ac.kr">Dana S. Scott. [https://ropas.snu.ac.kr/~kwang/520/readings/sco70.pdf Outline of a mathematical theory of computation]. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.</ref><ref name="Research Group Technical Monograph 1971">[[Dana Scott]] and [[Christopher Strachey]]. ''Toward a mathematical semantics for computer languages'' Oxford Programming Research Group Technical Monograph. PRG-6. 1971.</ref> or by [[Game theory|games]]<ref>Jan Jürjens. J. Games In The Semantics Of Programming Languages – An Elementary Introduction. Synthese 133, 131–158 (2002). [https://doi.org/10.1023/A:1020883810034 https://doi.org/10.1023/A:1020883810034]</ref> between the environment and the system.

Denotational semantics as originally developed by Strachey and Scott interpreted the denotation (meaning) of a computer program as a [[function_(mathematics)|function]] that mapped input into output. Functions later this proved to be too limiting for the denotations (meanings) of networked and concurrent systems.

An important tenet of denotational semantics is that ''semantics should be [[compositional]]'': the denotation of a program phrase should be built out of the denotations of its [[phrase|subphrases]].

==Fixed point semantics==

The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. The theory makes use of a computational mathematical [[Domain theory|___domain]] <'''Denotations''', ≤>. Examples of such objects are partial functions, sets of states, and [[Actor model|Actor]] event scenarios. The relationship <tt>x≤y</tt> means that <tt>x</tt> can computationally evolve to <tt>y</tt>. If the denotations are partial functions, for example, <tt>f≤g</tt> may mean that <tt>f</tt> agrees with <tt>g</tt> on all values for which <tt>f</tt> is defined. If the denotations are [[Actor model|Actor]] event diagram scenarios, <tt>x≤y</tt> means that a system which satisfies <tt>x</tt> can evolve into a system which satisfies <tt>y</tt>.

==Historical development==

As computation continues, the denotations should become better and have a limit so if we have <tt>∀i∈ω x<sub>i<sub>≤x<sub>i+1<sub> then the [[least upper bound]] <tt>∨_i∈ω x_i</tt> should exist. The property just stated is called ω-completeness.

Denotational semantics originated in the work of [[Christopher Strachey]] and [[Dana Scott]] published in the early 1970s.<ref name="ropas.snu.ac.kr"/><ref name="Research Group Technical Monograph 1971"/> As originally developed by Strachey and Scott, denotational semantics provided the meaning of a computer program as a [[function (mathematics)|function]] that mapped input into output.<ref name="Research Group Technical Monograph 1971"/> To give meanings to [[Recursion|recursively defined]] programs, Scott proposed working with [[Scott continuity|continuous functions]] between [[___domain theory|domains]], specifically [[complete partial order]]s. As described below, work has continued in investigating appropriate denotational semantics for aspects of programming languages such as sequentiality, [[Denotational semantics#Denotational semantics of concurrency|concurrency]], [[Nondeterministic algorithm|non-determinism]] and [[local state]].

Denotational semantics has been developed for modern programming languages that use capabilities like [[Concurrent computing|concurrency]] and [[Exception handling|exceptions]], e.g., [[Concurrent ML]],<ref>John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, ''[[Lecture Notes in Computer Science]]'', Vol. 693. 1993</ref> [[Communicating sequential processes|CSP]],<ref name=Roscoe>[[A. W. Roscoe]]. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.</ref> and [[Haskell (programming language)|Haskell]].<ref>[[Simon Peyton Jones]], Alastair Reid, Fergus Henderson, [[Tony Hoare]], and Simon Marlow. "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.1525&rep=rep1&type=pdf A semantics for imprecise exceptions]" Conference on Programming Language Design and Implementation. 1999.</ref> The semantics of these languages is compositional in that the meaning of a phrase depends on the meanings of its subphrases. For example, the meaning of the [[Applicative programming language|applicative expression]] <code>f(E1,E2)</code> is defined in terms of semantics of its subphrases f, E1 and E2. In a modern programming language, E1 and E2 can be evaluated concurrently and the execution of one of them might affect the other by interacting through [[Object (computer science)|shared objects]] causing their meanings to be defined in terms of each other. Also, E1 or E2 might throw an exception which could [[Abort (computing)|terminate]] the execution of the other one. The sections below describe special cases of the semantics of these modern programming languages.

The mathematical denotation denoted by a system <tt>S</tt> is found by solving by constructing increasingly better approximations from an initial empty denotation called <tt>⊥_S</tt> using some denotation approximating function <tt>'''progression'''_S</tt> to constuct a denotation (meaning ) for <tt>S</tt> as follows:

::<tt>'''Denote'''_S ≡ ∨_i∈ω '''progression'''_Sⁱ(⊥<sub>S<sub>)</tt>..

===Meanings of recursive programs===

It would be expected that <tt>'''progression'''_S</tt> would be ''monotone'', ''i.e.'', if <tt>x≤y</tt> then <tt>'''progression'''_S(x)≤'''progression'''_S(y)</tt>. More generally, we would expect that

Denotational semantics is ascribed to a program phrase as a function from an environment (holding current values of its free variables) to its denotation. For example, the phrase {{code|n*m}} produces a denotation when provided with an environment that has binding for its two free variables: {{code|n}} and {{code|m}}. If in the environment {{code|n}} has the value 3 and {{code|m}} has the value 5, then the denotation is 15.<ref name="Research Group Technical Monograph 1971"/>

::If <tt>∀i∈ω x<sub>i<sub>≤x<sub>i+1<sub></tt>, then <tt>'''progression'''_S(∨_i∈ω x_i) = ∨_i∈ω '''progression'''_S(x_i)</tt>

This last stated property of <tt>'''progression'''_S</tt> is called ω-continuity.

A function can be represented as a set of [[ordered pair]]s of argument and corresponding result values. For example, the set {(0,1), (4,3)} denotes a function with result 1 for argument 0, result 3 for the argument 4, and undefined otherwise.

A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) in according to the equation for <tt>'''Denote'''_S</tt>. If the the denotations (meanings) that we are using are ω-complete and <tt>'''progression'''_S<tt> is ω-continuous then <tt>'''Denote'''_S</tt> will exist.

Consider for example the [[factorial]] function, which might be defined recursively as:

It follows from the ω-continuity of <tt>'''progression'''_S</tt> that

<syntaxhighlight lang="c">

:::<tt>'''progression'''_S('''Denote'''_S) = '''Denote'''_S</tt>

int factorial(int n)

{

if (n == 0)

return 1;

else

return n * factorial(n - 1);

}

</syntaxhighlight>

To provide a meaning for this recursive definition, the denotation is built up as the limit of approximations, where each approximation limits the number of calls to factorial. At the beginning, we start with no calls - hence nothing is defined. In the next approximation, we can add the ordered pair (0,1), because this doesn't require calling factorial again. Similarly we can add (1,1), (2,2), etc., adding one pair each successive approximation because computing ''factorial(n)'' requires ''n+1'' calls. In the limit we get a [[total function]] from <math>\mathbb{N}</math> to <math>\mathbb{N}</math> defined everywhere in its ___domain.

The above equation motivates the terminology that <tt>'''Denote'''_S</tt> is a ''fixed point'' of <tt>'''progression'''_S</tt>.

Formally we model each approximation as a [[partial function]] <math>\N \rightharpoonup \N</math>. Our approximation is then repeatedly applying a function implementing "make a more defined partial factorial function", i.e. <math>F : (\N \rightharpoonup \N) \to (\N \rightharpoonup \N) </math>, starting with the [[empty function]] (empty set). ''F'' could be defined in code as follows (using <code>Map<int,int></code> for <math>\N \rightharpoonup \N</math>):

Furthermore this fixed point is least among all fixed points of <tt>'''progression'''_S</tt>.

<syntaxhighlight lang="cpp">

int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n)

{

if (n == 0) then return 1;

else if (fprev = lookup(factorial_less_defined, n-1)) then

return n * fprev;

else

return NOT_DEFINED;

}

Map<int,int> F(Map<int,int> factorial_less_defined)

The denotational semantics of functional programs provides an example of fixed point semantics as shown in the next section.

{

Map<int,int> new_factorial = Map.empty();

for (int n in all<int>()) {

if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED)

new_factorial.put(n, f);

}

return new_factorial;

}

</syntaxhighlight>

Then we can introduce the notation ''Fⁿ'' to indicate [[iterated function|''F'' applied ''n'' times]].

===Example of factorial function===

* ''F''⁰({}) is the totally undefined partial function, represented as the set {};

Consider the <tt>factorial</tt> function which is defined on all non-negative numbers as follows:

* ''F''¹({}) is the partial function represented as the set {(0,1)}: it is defined at 0, to be 1, and undefined elsewhere;

:<tt>factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)</tt>

* ''F''⁵({}) is the partial function represented as the set {(0,1), (1,1), (2,2), (3,6), (4,24)}: it is defined for arguments 0,1,2,3,4.

The '''<tt>graph</tt>''' of <tt>factorial</tt> is the set of all ordered pairs for which factorial is defined with the first element of an ordered pair being the argument and the second element being the value, ''e.g.'',

:<tt>'''graph'''(factorial) = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}</tt>

The denotation (meaning) <tt>'''Denote'''_factorial</tt> for the <tt>factorial</tt> progam is constructed as follows:

:<tt>'''Denote'''_factorial = '''graph'''(factorial) = ∪_i∈ω '''progression'''_factorialⁱ({})</tt>

This iterative process builds a sequence of partial functions from <math>\mathbb{N}</math> to <math>\mathbb{N}</math>. Partial functions form a [[chain-complete partial order]] using ⊆ as the ordering. Furthermore, this iterative process of better approximations of the factorial function forms an expansive (also called progressive) mapping because each <math>F^i\le F^{i+1}</math> using ⊆ as the ordering. So by a [[fixed-point theorem]] (specifically [[Bourbaki–Witt theorem]]), there exists a fixed point for this iterative process.

where

In this case, the fixed point is the least upper bound of this chain, which is the full {{code|factorial}} function, which can be expressed as the [[Union (set theory)|union]]

:<tt>'''progression'''_factorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)</tt>

:<math>\bigcup_{i \in \mathbb N} F^i(\{\}). </math>

The fixed point we found is the [[least fixed point]] of ''F'', because our iteration started with the smallest element in the ___domain (the empty set). To prove this we need a more complex fixed point theorem such as the [[Knaster–Tarski theorem]].

Note: <tt>'''progression'''_factorial</tt> is a fix point operator (see definition in section above) whose least fixed point is <tt>'''Denote'''_factorial</tt>, i.e.,

:<tt>'''Denote'''_factorial = '''progression'''_factorial('''Denote'''_factorial)</tt>

Also <tt>'''progression'''_factorial</tt> is ω-continuous (see definition in section above).

===Denotational semantics of non-deterministic programs===

===Derivation of Scott Continuity from Actor Semantics===

The concept of [[power domains]] has been developed to give a denotational semantics to non-deterministic sequential programs. Writing ''P'' for a power-___domain constructor, the ___domain ''P''(''D'') is the ___domain of non-deterministic computations of type denoted by ''D''.

The [[Actor model]] provides a foundation for deriving [[Dana Scott|Dana Scott's]] denotational semantics of functions (as illustrated in the previous section above for <tt>factorial</tt>) as demonstrated first by a theorem of [[Carl Hewitt]] and [[Henry Baker (computer scientist)|Henry Baker]] [1977]:

There are difficulties with fairness and [[Unbounded nondeterminism|unboundedness]] in ___domain-theoretic models of non-determinism.<ref>{{cite journal |first=Paul Blain |last=Levy |title=Amb Breaks Well-Pointedness, Ground Amb Doesn't |journal=Electron. Notes Theor. Comput. Sci. |volume=173 |pages=221–239 |year=2007 |doi=10.1016/j.entcs.2007.02.036 |doi-access=free }}</ref>

If an Actor <tt>f</tt> behaves like a mathematical function, then <tt>'''progression'''_f</tt> is a [[Scott continuity|Scott continuous functional]] whose least fixed point is

:<tt>'''graph'''(f) = ∪_i∈ω '''progression'''_fⁱ({})</tt></tt>

where

:<tt>'''progression'''_f(G)≡{<x,y>|<x,y>&isin;'''graph'''(f) ''and'' '''immediate-descendants'''_f(<x,y>)&sube;G}</tt>

The paper by Hewitt and Baker contained a small bug in the definition of <tt>'''immediate-descendants'''_f</tt> that was corrected in Will Clinger [1981].

===Denotational semantics of concurrency===

==Compositionality==

Many researchers have argued that the ___domain-theoretic models given above do not suffice for the more general case of [[Concurrency (computer science)|concurrent computation]]. For this reason various [[Concurrency (computer science)#Models|new models]] have been introduced. In the early 1980s, people began using the style of denotational semantics to give semantics for concurrent languages. Examples include [[Denotational semantics of the Actor model#Clinger.27s Model|Will Clinger's work with the actor model]]; Glynn Winskel's work with event structures and [[Petri nets]];<ref>''[https://www.cl.cam.ac.uk/~gw104/eventStructures82.pdf Event Structure Semantics for CCS and Related Languages]''. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.</ref> and the work by Francez, Hoare, Lehmann, and de Roever (1979) on trace semantics for CSP.<ref>[[Nissim Francez]], [[C. A. R. Hoare]], Daniel Lehmann, and [[Willem-Paul de Roever]]. "[https://dspace.library.uu.nl/bitstream/handle/1874/24888/francez_79_Semantics+of+nondeterminism.pdf?sequence=1 Semantics of nondeterminism, concurrency, and communication]", ''Journal of Computer and System Sciences''. December 1979.</ref> All these lines of inquiry remain under investigation (see e.g. the various denotational models for CSP<ref name=Roscoe/>).

An important aspect of denotational semantics is compositionality by which the denotation of a program is constructed from denotations of its parts. For example consider the expression "<tt><expression₁> + <expression₂></tt>". Compositionality in this case is to provide a meaning for "<tt><expression₁> + <expression₂></tt>" in terms of the meanings of <tt><expression₁></tt> and <tt><expression₂></tt>.

Recently, Winskel and others have proposed the category of [[profunctor]]s as a ___domain theory for concurrency.<ref>{{cite journal |first1=Gian Luca |last1=Cattani |first2=Glynn |last2=Winskel |title=Profunctors, open maps and bisimulation |journal=Mathematical Structures in Computer Science |volume=15 |issue=3 |pages=553–614 |year=2005 |doi= 10.1017/S0960129505004718|citeseerx=10.1.1.111.6243 |s2cid=16356708 }}</ref><ref>{{cite journal |first1=Mikkel |last1=Nygaard |first2=Glynn |last2=Winskel |title=Domain theory for concurrency |journal=Theor. Comput. Sci. |volume=316 |issue=1–3 |pages=153–190 |year=2004 |doi=10.1016/j.tcs.2004.01.029 |doi-access=free }}</ref>

===Environments===

The [[Actor model]] provides a modern and very general way the compositionality of programs can be analyzed. In this analysis, programs are Actors that are sent <tt>Eval</tt> messages with the address of an environment Actor. The environment holds the bindings of identifiers. When an environment is sent a <tt>Lookup</tt> message with the address of an identifier '''x''', it returns the latest (lexical) binding of '''x'''.

===Denotational semantics of state===

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

State (such as a heap) and simple [[imperative programming|imperative features]] can be straightforwardly modeled in the denotational semantics described above. The key idea is to consider a command as a partial function on some ___domain of states. The meaning of "{{code|1=x:=3}}" is then the function that takes a state to the state with {{code|3}} assigned to {{code|x}}. The sequencing operator "{{code|;}}" is denoted by composition of functions. Fixed-point constructions are then used to give a semantics to looping constructs, such as "{{code|while}}".

Things become more difficult in modelling programs with local variables. One approach is to no longer work with domains, but instead to interpret types as [[functor]]s from some category of worlds to a category of domains. Programs are then denoted by [[natural transformation|natural]] continuous functions between these functors.<ref>[[Peter W. O'Hearn]], John Power, [[Robert D. Tennent]], Makoto Takeyama. Syntactic control of interference revisited. ''Electron. Notes Theor. Comput. Sci.'' 1. 1995.</ref><ref>Frank J. Oles. ''A Category-Theoretic Approach to the Semantics of Programming''. PhD thesis, [[Syracuse University]], New York, USA. 1982.</ref>

λ(leftSubTree,rightSubTree)

λ(message)

''if'' (message == "getLeft") ''then'' leftSubTree

''else if'' (message == "getRight") ''then'' rightSubTree

===Denotations of data types===

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

Many programming languages allow users to define [[recursive data type]]s. For example, the type of lists of numbers can be specified by

<syntaxhighlight lang=sml>datatype list = Cons of nat * list | Empty</syntaxhighlight>

This section deals only with functional data structures that cannot change. Conventional imperative programming languages would typically allow the elements of such a recursive list to be changed.

For another example: the type of denotations of the [[untyped lambda calculus]] is

However <tt><L><tt> responds to the <tt>Eval</tt> message by creating a [[Closure (computer science)|closure]] Actor '''C''' that has an address (called ''body'') for <tt><L></tt> an address (called ''environment'') for '''E'''. The Actor <tt>"(<L> 1 2)"</tt> then sends '''C''' the message '''[1 2]'''.

<syntaxhighlight lang=sml>datatype D = D of (D → D)</syntaxhighlight>

The problem of ''solving ___domain equations'' is concerned with finding domains that model these kinds of datatypes. One approach, roughly speaking, is to consider the collection of all domains as a ___domain itself, and then solve the recursive definition there.

[[Polymorphism (computer science)|Polymorphic data types]] are data types that are defined with a parameter. For example, the type of α {{code|list}}s is defined by

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

<syntaxhighlight lang=sml>datatype α list = Cons of α * α list | Empty</syntaxhighlight>

#When it receives a <tt>Lookup</tt> message for the identifier <tt>leftSubTree</tt> it responds with <tt>1</tt>

Lists of natural numbers, then, are of type {{code|nat list}}, while lists of strings are of {{code|string list}}.

#When it receives a <tt>Lookup</tt> message for the identifier <tt>rightSubTree</tt> it responds with <tt>2</tt>

#When it receives a <tt>Lookup</tt> message for any other identifier, it forwards the <tt>Lookup</tt> message to '''E'''.

Some researchers have developed ___domain theoretic models of polymorphism. Other researchers have also modeled [[parametric polymorphism]] within constructive set theories.

The Actor '''C''' then sends an <tt>Eval</tt> message with enviornment '''F''' to the following actor:

A recent research area has involved denotational semantics for object and class based programming languages.<ref>{{cite journal |first1=Bernhard |last1=Reus |first2=Thomas |last2=Streicher |title=Semantics and logic of object calculi |journal=Theor. Comput. Sci. |volume=316|issue=1 |pages=191–213 |year=2004 |doi=10.1016/j.tcs.2004.01.030 |doi-access=free }}</ref>

λ(message)

''if'' (message == "getLeft") ''then'' leftSubTree

''else if'' (message == "getRight") ''then'' rightSubTree

===Denotational semantics for programs of restricted complexity===

===Arithmetic expressions===

Following the development of programming languages based on [[linear logic]], denotational semantics have been given to languages for linear usage (see e.g. [[proof net]]s, [[Coherent space|coherence spaces]]) and also polynomial time complexity.<ref>{{cite journal |first=P. |last=Baillot |title=Stratified coherence spaces: a denotational semantics for Light Linear Logic |journal=Theor. Comput. Sci. |volume=318 |issue=1–2 |pages=29–55 |year=2004 |doi=10.1016/j.tcs.2003.10.015 |doi-access=free }}</ref>

For another example consider the Actor for the expression "<tt><expression₁> + <expression₂></tt>" which has addresses for two other actors <tt><expression₁></tt> and <tt><expression₂></tt>). When the composite expression actor receives an <tt>Eval</tt> message with addresses for an environment Actor '''E''' and a customer Actor '''C''', it sends <tt>Eval</tt> messages to <tt>expression₁</tt> and <tt><expression₂</tt> with environment '''E''' and customer a new Actor '''C₀'''. When '''C₀''' has received back two values '''N₁''' and '''N₂''', it sends '''C''' the value '''N₁''' <tt>+</tt> '''N₂'''. In this way, the Actor model provides a semantics for "<tt><expression₁> + <expression₂></tt>" in terms of the semantics for <tt><expression₁></tt> and <tt><expression₂></tt>.

===Denotational semantics of sequentiality===

===Delayed evaluation===

The problem of full [[Denotational semantics#Abstraction|abstraction]] for the sequential programming language [[Programming language for Computable Functions|PCF]] was, for a long time, a big open question in denotational semantics. The difficulty with PCF is that it is a very sequential language. For example, there is no way to define the [[logical disjunction#parallel-or|parallel-or]] function in PCF. It is for this reason that the approach using domains, as introduced above, yields a denotational semantics that is not fully abstract.

Providing a compositional semantics for delayed evaluation provides a challenge for denotational semantics. The problem with classical approaches for compositional denotatonal sementics in dealing with expressions of form <tt>"''delay'' <Expression>"</tt> has been how to formaize the semantics of the evaluation of <tt><Expression></tt>.

This open question was mostly resolved in the 1990s with the development of [[game semantics]] and also with techniques involving [[logical relations]].<ref>{{cite journal |first1=P.W. |last1=O'Hearn |first2=J.G. |last2=Riecke |title=Kripke Logical Relations and PCF |journal=Information and Computation |volume=120 |issue=1 |pages=107–116 |date=July 1995 |doi=10.1006/inco.1995.1103 |s2cid=6886529 |url=https://surface.syr.edu/lcsmith_other/3 |doi-access=free }}</ref> For more details, see the page on PCF.

The Actor model provides a perfectly reasonable account:

===Denotational semantics as source-to-source translation===

:The ''delay'' expression responds to an <Eval> message with environment '''E''' by creating a [[Closure (computer science)|closure]] Actor '''C''' that has an address (called ''body'') for <tt><Expression></tt> an address (called ''environment'') for '''E'''.

It is often useful to translate one programming language into another. For example, a concurrent programming language might be translated into a [[process calculus]]; a high-level programming language might be translated into byte-code. (Indeed, conventional denotational semantics can be seen as the interpretation of programming languages into the [[internal language]] of the category of domains.)

In this context, notions from denotational semantics, such as full abstraction, help to satisfy security concerns.<ref>Martin Abadi. "Protection in programming-language translations". ''Proc. of ICALP'98''. LNCS 1443. 1998.</ref><ref>{{cite journal |first=Andrew |last=Kennedy |title=Securing the .NET programmingmodel |journal=Theor. Comput. Sci. |volume=364 |issue=3 |pages=311–7 |year=2006|doi=10.1016/j.tcs.2006.08.014 |doi-access=free }}</ref>

:When '''C''' receives a message '''M''' with '''Customer₀''', it creates a new Actor '''Customer₁''' and sends <tt><Expression></tt> an </tt>Eval</tt> message with environment '''E''' and the address of '''Customer₁'''.

:When '''Customer₁''' receives a value '''V''', it sends '''V''' the message '''M''' with '''Customer₀'''.

==Abstraction==

Other programming language constructs can be provided compositional semantics in similar ways.

It is often considered important to connect denotational semantics with [[operational semantics]]. This is especially important when the denotational semantics is rather mathematical and abstract, and the operational semantics is more concrete or closer to the computational intuitions. The following properties of a denotational semantics are often of interest.

#'''Syntax independence''': The denotations of programs should not involve the syntax of the source language.

#'''Adequacy (or soundness)''': All [[observational equivalence|observably distinct]] programs have distinct denotations;

#'''Full abstraction''': All observationally equivalent programs have equal denotations.

For semantics in the traditional style, adequacy and full abstraction may be understood roughly as the requirement that "operational equivalence coincides with denotational equality". For denotational semantics in more intensional models, such as the [[actor model]] and [[process calculi]], there are different notions of equivalence within each model, and so the concepts of adequacy and of full abstraction are a matter of debate, and harder to pin down. Also the mathematical structure of operational semantics and denotational semantics can become very close.

The Actor model compositional semantics is very general and can be used for [[Functional programming|functional]], [[Imperative programming|imperative]], [[Concurrent programming language|concurrent]], [[Logic programming|logic]], ''etc.'' programs

Additional desirable properties we may wish to hold between operational and denotational semantics are:

==Denotational semantics of concurrency==

#'''Constructivism''': [[Constructivism (mathematics)|Constructivism]] is concerned with whether ___domain elements can be shown to exist by constructive methods.

Extending denotational semantics to concurrency proved challenging. See [[unbounded nondeterminism]].

#'''Independence of denotational and operational semantics''': The denotational semantics should be formalized using mathematical structures that are independent of the operational semantics of a programming language; However, the underlying concepts can be closely related. See the section on [[Denotational semantics#Compositionality|Compositionality]] below.

#'''Full completeness''' or '''definability''': Every morphism of the semantic model should be the denotation of a program.<ref>{{cite journal

| last = Curien

| first = Pierre-Louis

| title = Definability and Full Abstraction

| journal = Electronic Notes in Theoretical Computer Science

| volume = 172

| pages = 301–310

| doi = 10.1016/j.entcs.2007.02.011

| year = 2007 | doi-access = free

}}</ref>

==Compositionality==

===The ___domain of Actor computations===

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

Clinger [1981] explained the ___domain of Actor computations as follows:

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.

:The augmented Actor event diagrams [see [[Actor model theory]]] form a partially ordered set < <tt>'''Diagrams'''</tt>, &nbsp;<tt>&le;</tt>&nbsp;> from which to construct the power ___domain <tt>''P''['''Diagrams''']</tt> (see the section on [[Denotational semantics#Denotations|Denotations]] below). The augmented diagrams are partial computation histories representing "snapshots" [relative to some frame of reference] of a computation on its way to being completed. For <tt>x</tt>,<tt>y</tt>&isin;<tt>'''Diagrams'''</tt>, <tt>x&le;y</tt> means <tt>x</tt> is a stage the computation could go through on its way to <tt>y</tt>. The completed elements of <tt>'''Diagrams'''</tt> represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of <tt>'''Diagrams'''</tt> [see William Wadge 1979]. Concretely, the completed elements are those having non pending events. Intuitively, <tt>'''Diagrams'''</tt> is not [[Completeness (order theory)|&omega;-complete]] because there exist increasing sequences of finite partial computations

#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>_⊥.

#From the meaning of types we derive a meaning for typing contexts. We set 〚 ''x''₁:τ₁,..., ''x''_n:τ_n〛 = 〚 τ₁〛× ... ×〚τ_n〛. For instance, 〚''x'':{{code|nat}},''y'':{{code|nat}}〛= <math>\mathbb{N}</math>_⊥×<math>\mathbb{N}</math>_⊥. 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>_⊥ is the constantly "7" function, while 〚''x'':{{code|nat}},''y'':{{code|nat}}⊢''x''+''y'':{{code|nat}}〛:<math>\mathbb{N}</math>_⊥×<math>\mathbb{N}</math>_⊥→<math>\mathbb{N}</math>_⊥ 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>_⊥, 〚⊢4:{{code|nat}}〛:1→<math>\mathbb{N}</math>_⊥, and 〚''x'':{{code|nat}},''y'':{{code|nat}}⊢''x''+''y'':{{code|nat}}〛:<math>\mathbb{N}</math>_⊥×<math>\mathbb{N}</math>_⊥→<math>\mathbb{N}</math>_⊥.

::<tt>x₀&nbsp;&le;&nbsp;x₁&nbsp;&le;&nbsp;x₂&nbsp;&le;&nbsp;x₃&nbsp;&le;&nbsp;...</tt>

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>

:in which some pending event remains pending forever while the number of realized events grows without bound, contrary to the requirement of finite [arrival] delay. Such a sequence cannot have a limit, because any limit would represent a completed nonterminating computation in which an event is still pending.

==Semantics versus implementation==

:To repeat, the actor event diagram ___domain <tt>'''Diagrams'''</tt> is incomplete because of the requirement of finite arrival delay, which allows any finite delay between an event and an event it activates but rules out infinite delay.

According to Dana Scott (1980):<ref>"What is Denotational Semantics?", MIT Laboratory for Computer Science Distinguished Lecture Series, 17 April 1980, cited in Clinger (1981).</ref>

:''It is not necessary for the semantics to determine an implementation, but it should provide criteria for showing that an implementation is correct.''

According to Clinger (1981):<ref name="clinger1981">{{cite thesis |degree=PhD |first=William D. |last=Clinger |title=Foundations of Actor Semantics |date=May 1981 |publisher=Massachusetts Institute of Technology |id=AITR-633 |hdl=1721.1/6935 |hdl-access=free}}</ref>{{rp|79}}

===Denotations===

:''Usually, however, the formal semantics of a conventional sequential programming language may itself be interpreted to provide an (inefficient) implementation of the language. A formal semantics need not always provide such an implementation, though, and to believe that semantics must provide an implementation leads to confusion about the formal semantics of concurrent languages. Such confusion is painfully evident when the presence of unbounded nondeterminism in a programming language's semantics is said to imply that the programming language cannot be implemented.''

In his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:

From the article on [[Power domains]]: <tt>''P''[D]</tt> is the collection of downward-closed subsets of ___domain <tt>D</tt> that are also closed under existing least upper bounds of directed sets in <tt>D</tt>. Note that while the ordering on <tt>''P''[D]</tt> is given by the subset relation, least upper bounds do not in general coincide with unions.

:For the actor event diagram ___domain <tt>'''Diagrams'''</tt>, an element of <tt>''P''['''Diagrams''']</tt> represents a list of possible initial histories of a computation. Since for elements <tt>x</tt> and <tt>y</tt> of </tt>'''Diagrams'''</tt>, <tt>x&le;y</tt> means that <tt>x</tt> is an initial segment of the initial history </tt>y</tt>, the requirement that elements of <tt>''P''['''Diagrams''']</tt> be downward-closed has a clear basis in intuition.

:...

:Usually the partial order from which the power ___domain is constructed is required to be [[Completeness (order theory)#Completion of domains|&omega;-complete]]. There are two reasons for this. The first reason is that most power domains are simply generalizations of domains that have been used as semantic domains for conventional sequential programs, and such domains are all complete because of the need to compute fixed points in the sequential case. The second reason is that &omega;-completeness permits the solution of recursive ___domain equations involving the power ___domain such as

::<tt>R &#8776; S&nbsp;&rarr;&nbsp;''P''[S + (S <math>\times</math> R)]</tt>

:which defines a ___domain of resumptions [Gordon Plotkin 1976]. However, [[power domains]] can be defined for any ___domain whatsoever. Furthermore the power ___domain of a ___domain is essentially the power ___domain of its &omega;-completion, so recursive equations involving the power ___domain of an incomplete ___domain can still be solved, provide the domains to which the usual constructors (<tt>+</tt>, <math>\times</math>, &nbsp;&rarr;&nbsp;, and <tt>*</tt>) are applied are &omega;-complete. It happens that defining Actor semantics as in Clinger [1981] does not require solving any recursive equations involving the power ___domain.

:In short, there is no technical impediment to building power domains from incomplete domains. But why should one want to do so?

:In ''behavioral semantics'', developed by Irene Greif, the meaning of program is a specification of the computations that may be performed by the program. The computations are represented formally by Actor event diagrams. Greif specified the event diagrams by means of causal axioms governing the behaviors of individual Actors [Greif 1975].

:Henry Baker has presented a nondeterministic interpreter generating instantaneous schedules which then map onto event diagrams. He suggested that a corresponding deterministic interpreter operating on sets of instantaneous schedules could be defined using power ___domain semantics [Baker 1978].

:The semantics presented in [Clinger 1981] is a version of behavioral semantics. A program denotes a set of Actor event diagrams. The set is defined extensionally using power ___domain semantics rather than intensionally using causal axioms. The behaviors of individual Actors is defined functionally. It is shown, however, that the resulting set of Actor event diagrams consists of exactly those diagrams that satisfy causal axioms expressing the functional behaviors of Actors. Thus Greif's behavioral semantics is compatible with a denotational power ___domain semantics.

:Baker's instantaneous schedules introduced the notion of ''pending events'', which represent messages on the way to their targets. Each pending event must become an actual (realized) arrival event sooner or later, a requirement referred to as ''finite delay''. Augmenting Actor event diagrams with sets of pending events helps to express the finite delay property, which is characteristic of true concurrency [Schwartz 1979].

===Sequential computations form an &omega;-complete subdomain of the ___domain of Actor computations===

In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:

:Instead of beginning with a semantics for sequential programs and then trying to extend it for concurrency, Actor semantics views concurrency as primary and obtains the semantics of sequential programs as a special case.

:...

:The fact that there exist increasing sequences without least upper bounds may seem strange to those accustomed to thinking about the semantics of sequential programs. It may help to point out that the increasing sequences produced by sequential programs all have least upper bounds. Indeed, the partial computations that can be produced by sequential computation form an &omega;-complete subdomain of the ___domain of Actor computations <tt>'''Diagrams'''</tt>. An informal proof follows.

::From the Actor point of view, sequential computations are a special case of concurrent computations, distinguishable by their event diagrams. The event diagram of a sequential computation has an initial event, and no event activates more than one event. In other words, the activation ordering of an sequential computation is linear; the event diagram is essentially a conventional execution sequence. This means that the finite elements of <tt>'''Diagrams'''</tt>

:::<tt>x₀&nbsp;&le;&nbsp;x₁&nbsp;&le;&nbsp;x₂&nbsp;&le;&nbsp;x₃&nbsp;&le;&nbsp;...</tt>

::corresponding to the finite initial segments of a sequential execution sequence all have exactly one pending event, excepting the largest, completed element if the computation terminates. One property of the augmented event diagrams ___domain < <tt>'''Diagrams'''</tt>, &nbsp;<tt>&le;</tt>&nbsp;> is that if <tt>x&le;y</tt> and <tt>x&ne;y</tt>, then some pending event of <tt>x</tt> is realized in <tt>y</tt>. Since in this case each <tt>x_i</tt> has at most one pending event, every pending event in the sequence becomes realized. Hence the sequence

:::<tt>x₀&nbsp;&le;&nbsp;x₁&nbsp;&le;&nbsp;x₂&nbsp;&le;&nbsp;x₃&nbsp;&le;&nbsp;...</tt>

::has a least upper bound in <tt>'''Diagrams'''</tt> in accord with intuition.

:The above proof applies to all sequential programs, even those with choice points such as [[guarded commands]]. Thus Actor semantics includes sequential programs as a special case, and agrees with conventional semantics of such programs.

==Early history of denotational semantics==

As mentioned earlier, the field was initially developed by [[Christopher Strachey]] and [[Dana Scott]] in the [[1960s]] and then [[Joe Stoy]] in the [[1970s]] at the [[Programming Research Group]], part of the [[Oxford University Computing Laboratory]].

[[Montague grammar]] is a form of denotational semantics for idealized fragments of [[English language|English]].

According to Clinger [1981],

:[[Gordon Plotkin|Plotkin]]'s original power ___domain construction was simplified in [Smyth 1978] which remains the standard introduction to the subject. A number of nondeterministic programming languages have now been given power ___domain semantics. Of these the semantics of [Francez, [[Hoare]], Lehmann, and de Roever 1979] had the most influence over the development of the denotational model in Clinger's dissertation.

:The denotational semantics in Clinger's dissertation is probably the first power ___domain semantics for languages with true concurrency, but it is not the first power ___domain semantics for a language with unbounded nondeterminism. [Back 1980] has given a power ___domain semantics for a language with unboundedly nondeterministic assignment as a primitive operation. Three differences between Back's work and the Actor denotation semantics in Clinger's dissertation stand out:

:#The source of nondeterminism in Back's paper is basic assignment statements whereas in the Actor model it is message latency.

:#Back's paper treats nondeterministic sequential programming languages whereas the Actor model is concerned with concurrent programming languages.

:#The power ___domain in Back's paper apparently is constructed from a complete underlying ___domain. This third difference is not entirely clear because Back's power ___domain construction appears to be nonstandard.

:A similarity between Back's work the Actor denotational semantics in Clinger's dissertation is that Back found it necessary to build the power ___domain out of execution sequences instead of single states: the Actor power ___domain is built out of Actor event diagrams, which are generalizations of execution sequences.

==Connections to other areas of computer science==

Some work in denotationdenotational semantics has interpreted types as domains in the sense of [[___domain theory]], which can be seen as a branch of [[model theory]]., andleading has manyto connections with [[type theory]] and [[category theory]]. Within computer science, there are connections with [[abstract interpretation]], [[program verification]], and [[functionalmodel programmingchecking]], see for instance [[monads in functional programming]]. In particular, denotational semantics has used the concept of [[continuation]]s to express control flow in sequential programming in terms of [[functional programming]] semantics.

==References==

{{reflist}}

*Irene Greif. ''Semantics of Communicating Parallel Professes'' MIT EECS Doctoral Dissertation. August 1975.

* [[Joe Stoy|Joseph E. Stoy]], ''Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics''. [[MIT Press]], Cambridge, Massachusetts, 1977. (A classic if dated textbook.)

==Further reading==

* Gordon Plotkin. ''A powerdomain construction'' SIAM Journal of Computing September 1976.

;Textbooks

* [[Edsger Dijkstra]]. ''A Discipline of Programming'' [[Prentice Hall]]. 1976.

{{refbegin}}

* Krzysztof R. Apt, J. W. de Bakker. ''Exercises in Denotational Semantics'' MFCS 1976: 1-11

*{{Cite book |last1=Milne |first1=R.E. |title=A theory of programming language semantics |last2=Strachey |first2=C. |year=1976 |isbn=978-1-5041-2833-9 |author-link2=Christopher Strachey}}

* J. W. de Bakker. ''Least Fixed Points Revisited'' Theor. Comput. Sci. 2(2): 155-181 (1976)

*{{Cite book |last=Gordon |first=M.J.C. |url=https://books.google.com/books?id=s4jTBwAAQBAJ |title=The Denotational Description of Programming Languages: An Introduction |date=2012 |publisher=Springer |isbn=978-1-4612-6228-2 |author-link=Michael J. C. Gordon |orig-date=1979}}

* [[Carl Hewitt]] and [[Henry Baker (computer scientist)|Henry Baker]] ''Actors and Continuous Functionals'' Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1&ndash;5, 1977.

*{{Cite book |last=Stoy |first=Joseph E. |title=Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics |publisher=MIT Press |year=1977 |isbn=978-0-262-19147-0 |author-link=Joe Stoy}} (A classic if dated textbook.)

* [[Henry Baker (computer scientist)|Henry Baker]]. ''Actor Systems for Real-Time Computation'' MIT EECS Doctoral Dissertation. January 1978.

*{{Cite book |last=Schmidt |first=David A. |title=Denotational semantics: a methodology for language development |publisher=Allyn & Bacon |year=1986 |isbn=978-0-205-10450-5}}

* Michael Smyth. ''Power domains'' [[Journal of Computer and System Sciences]]. 1978.

**out of print now; free electronic version available: {{Cite book |last=Schmidt |first=David A. |url=https://people.cs.ksu.edu/~schmidt/text/densem.html |title=Denotational Semantics: A Methodology for Language Development |publisher=Kansas State University |year=1997 |orig-date=1986}}

* [[C.A.R. Hoare]]. ''[[Communicating Sequential Processes]]'' [[CACM]]. August, 1978.

*{{Cite book |last=Gunter |first=Carl |title=Semantics of Programming Languages: Structures and Techniques |publisher=MIT Press |year=1992 |isbn=978-0-262-07143-7}}

* George Milne and [[Robin Milner]]. ''Concurrent processes and their syntax'' [[JACM]]. April, 1979.

*{{Cite book |last=Winskel |first=Glynn |title=Formal Semantics of Programming Languages |publisher=MIT Press |year=1993 |isbn=978-0-262-73103-4}}

* Nissim Francez, [[C.A.R. Hoare]], Daniel Lehmann, and Willem-Paul de Roever. ''Semantics of nondeterminism, concurrency, and communication'' Journal of Computer and System Sciences. December 1979.

*{{Cite book |last=Tennent |first=R.D. |title=Semantic Structures |publisher=Oxford University Press |year=1994 |isbn=978-0-19-853762-5 |editor-last=Abramsky |editor-first=S. |series=Handbook of logic in computer science |volume=3 |pages=169–322 |chapter=Denotational semantics |ref={{harvid|Abramsky|Gabbay|Maibaum|1994}} |editor-last2=Gabbay |editor-first2=Dov M. |editor-last3=Maibaum |editor-first3=T.S.E.}}

* Nancy Lynch and Michael Fischer. ''On describing the behavior of distributed systems'' in Semantics of Concurrent Computation. [[Springer-Verlag]]. 1979.

*{{Cite book |last1=Abramsky |first1=S. |title={{harvnb|Abramsky|Gabbay|Maibaum|1994}} |last2=Jung |first2=A. |year=1994 |chapter=Domain theory |author-link=Samson Abramsky |chapter-url=http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf}}

* Jerald Schwartz ''Denotational semantics of parallelism'' in Semantics of Concurrent Computation. Springer-Verlag. 1979.

*{{Cite book |last1=Stoltenberg-Hansen |first1=V. |url=https://archive.org/details/mathematicaltheo0000stol |title=Mathematical Theory of Domains |last2=Lindström |first2=I. |last3=Griffor |first3=E.R. |date=1994 |publisher=Cambridge University Press |isbn=978-0-521-38344-8 |url-access=registration}}

* William Wadge. ''An extensional treatment of dataflow deadlock'' Semantics of Concurrent Computation. Springer-Verlag. 1979.

{{refend}}

* Ralph-Johan Back. ''Semantics of Unbounded Nondeterminism'' [[ICALP]] 1980.

; Lecture notes

* David Park. ''On the semantics of fair parallelism'' Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.

{{refbegin}}

* Will Clinger, ''Foundations of Actor Semantics''. MIT Mathematics Doctoral Dissertation, June 1981. (Quoted by permission of author.)

*{{Cite Lloydweb Allison,|last=Winskel ''A Practical Introduction to|first=Glynn |title=Denotational Semantics'' Cambridge|url=http://www.cl.cam.ac.uk/~gw104/dens.pdf |publisher=University Press.of Cambridge}} 1987.

{{refend}}

* P. America, J. de Bakker, J. N. Kok and J. Rutten. ''Denotational semantics of a parallel object-oriented language'' Information and Computation, 83(2): 152 - 205 (1989)

;Other references

* David A. Schmidt, ''The Structure of Typed Programming Languages''. MIT Press, Cambridge, Massachusetts, 1994. ISBN 026269171X.

{{refbegin}}

*M. Korff ''True concurrency semantics for single pushout graph transformations with applications to actor systems'' Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.

*{{Cite thesis |last=Greif |first=Irene |title=Semantics of Communicating Parallel Processes |date=August 1975 |degree=PhD |publisher=Massachusetts Institute of Technology |url=https://dspace.mit.edu/bitstream/handle/1721.1/57710/02200859-MIT.pdf |series=Project MAC |id=ADA016302}}

*M. Korff and L. Ribeiro ''Concurrent derivations as single pushout graph grammar processes'' Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.

*{{Cite journal |last=Plotkin |first=G.D. |author-link=Gordon Plotkin |year=1976 |title=A powerdomain construction |journal=SIAM J. Comput. |volume=5 |issue=3 |pages=452–487 |citeseerx=10.1.1.158.4318 |doi=10.1137/0205035}}

*{{Cite book |last=Dijkstra |first=Edsger W. |title=A Discipline of Programming |date=1976 |isbn=0-13-215871-X |series=Prentice-Hall series in automatic computation |___location=Englewood Cliffs, N.J. |oclc=1958445 |author-link=Edsger Dijkstra}}

*{{Cite book

|last1=Apt |first1=Krzysztof R.|author-link1=Krzysztof R. Apt

|title=Exercises in denotational semantics

|last2=de Bakker |first2=J. W. |date=1976

|publisher=Mathematisch Centrum |series=Afdeling Informatica |___location=Amsterdam |language=English |oclc=63400684}}

*{{Cite journal |last=De Bakker |first=J.W. |date=1976 |title=Least Fixed Points Revisited |journal=Theoretical Computer Science |language=en |volume=2 |issue=2 |pages=155–181 |doi=10.1016/0304-3975(76)90031-1 |doi-access=free}}

*{{Cite journal |last=Smyth |first=Michael B. |year=1978 |title=Power domains |journal=J. Comput. Syst. Sci. |volume=16 |pages=23–36 |doi=10.1016/0022-0000(78)90048-X |doi-access=free}}

*{{Cite book |last1=Francez |first1=Nissim |title=Semantics of nondeterminism, concurrency, and communication |last2=Hoare |first2=C.A.R. |last3=Lehmann |first3=Daniel |last4=de Roever |first4=Willem-Paul |date=December 1979 |work=Journal of Computer and System Sciences |isbn=978-3-540-08921-6 |series=Lecture Notes in Computer Science |volume=64 |pages=191–200 |doi=10.1007/3-540-08921-7_67 |hdl=1874/15886}}

*{{Cite book |last1=Lynch |first1=Nancy |title=Semantics of concurrent computation: proceedings of the international symposium, Évian, France, July 2-4, 1979 |last2=Fischer |first2=Michael J. |publisher=Springer |year=1979 |isbn=978-3-540-09511-8 |editor-last=Kahn |editor-first=G. |chapter=On describing the behavior of distributed systems |ref={{harvid|Kahn|1979}} |author-link=Nancy Lynch |author-link2=Michael J. Fischer |chapter-url=https://books.google.com/books?id=lLgqAQAAIAAJ}}

*{{Cite book |last=Schwartz |first=Jerald |title={{harvnb|Kahn|1979}} |year=1979 |chapter=Denotational semantics of parallelism}}

*{{Cite book |last=Wadge |first=William |title={{harvnb|Kahn|1979}} |year=1979 |chapter=An extensional treatment of dataflow deadlock}}

*{{Cite book |last=Back |first=Ralph-Johan |title=Automata, Languages and Programming |chapter-url=https://link.springer.com/chapter/10.1007%2F3-540-10003-2_59 |chapter=Semantics of unbounded nondeterminism |date=1980 |publisher=Springer |isbn=978-3-540-39346-7 |editor-last=de Bakker |editor-first=Jaco |series=Lecture Notes in Computer Science |volume=85 |___location=Berlin, Heidelberg |pages=51–63 |language=en |doi=10.1007/3-540-10003-2_59 |oclc=476017025 |url=https://ir.cwi.nl/pub/27111 |author-link=Ralph-Johan Back |editor-last2=van Leeuwen |editor-first2=Jan}}

*{{Cite book |last=Park |first=David |title=Abstract Software Specifications |chapter-url=http://link.springer.com/10.1007/3-540-10007-5_47 |chapter=On the semantics of fair parallelism |series=Lecture Notes in Computer Science |date=1980 |publisher=Springer Berlin Heidelberg |isbn=978-3-540-10007-2 |editor-last=Bjøorner |editor-first=Dines |volume=86 |___location=Berlin, Heidelberg |pages=504–526 |doi=10.1007/3-540-10007-5_47|url=http://wrap.warwick.ac.uk/59429/1/WRAP_Park_cs-rr-031.pdf }}

*{{Cite book |last=Allison |first=L. |url=https://books.google.com/books?id=uIdF11msK58C |title=A Practical Introduction to Denotational Semantics |publisher=Cambridge University Press |year=1986 |isbn=978-0-521-31423-7}}

*{{Cite journal |last1=America |first1=P. |last2=de Bakker |first2=J. |last3=Kok |first3=J.N. |last4=Rutten |first4=J. |year=1989 |title=Denotational semantics of a parallel object-oriented language |url=https://ir.cwi.nl/pub/1602 |journal=Information and Computation |volume=83 |issue=2 |pages=152–205 |doi=10.1016/0890-5401(89)90057-6|s2cid=2405175 |doi-access=free }}

*{{Cite book |last=Schmidt |first=David A. |title=The Structure of Typed Programming Languages |publisher=MIT Press |year=1994 |isbn=978-0-262-69171-0}}

{{refend}}

==External links==

{{Wikibooks|Haskell|Denotational semantics}}

* [http://www.csse.monash.edu.au/~lloyd/tilde/Semantics/ ''Denotation Semantics''] by Lloyd Allison

* [http://www.risccsse.uni-linzmonash.acedu.atau/people~lloyd/schreinetilde/coursesSemantics/densem/densem.html ''Structure of Programming Languages I: Denotational Semantics'']. Overview of book by WolfgangLloyd SchreinerAllison

* {{cite web |first=Wolfgang |last=Schreiner |title=Structure of Programming Languages I: Denotational Semantics |date=1995 |work=Course notes |url=http://www.risc.uni-linz.ac.at/people/schreine/courses/densem/densem.html}}

* [http://www.cis.ksu.edu/~schmidt/text/densem.html ''Denotational Semantics: A Methodology for Language Development''] by David Schmidt

* [http://www.honors.montana.edu/~jjc/presentation/contents.xhtml Presentation] by Josh Cogliati

* [http://www.hhm.com.ar/hql.htm HQL] by H. Hernan Moraldo &ndash; complete denotational semantics of a small language

{{DEFAULTSORT:Denotational Semantics}}

[[Category:Formal methods]]

[[Category:Denotational semantics| ]]

[[Category:1970 in computing]]

[[Category:Logic in computer science]]

[[Category:ActorModels modelof computation]]

[[Category:ConcurrentFormal computingspecification languages]]

[[Category:SpecificationProgramming languageslanguage semantics]]

{{Compu-stub}}

[[es:Semántica denotacional]]

[[fr:Sémantique dénotationnelle]]

[[pt:Semântica denotacional]]