1000/1000
Hot
Most Recent
The denotational semantics of the Actor model is the subject of denotational domain theory for Actors. The historical development of this subject is recounted in [Hewitt 2008b].
The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. Collections of such objects are called domains. The Actor uses the domain of event diagram scenarios. It is usual to assume some properties of the domain, such as the existence of limits of chains (see cpo) and a bottom element. Various additional properties are often reasonable and helpful: the article on domain theory has more details.
A domain is typically a partial order, which can be understood as an order of definedness. For instance, given event diagram scenarios x and y, one might let "x≤y" mean that "y extends the computations x".
The mathematical denotation denoted by a system S is found by constructing increasingly better approximations from an initial empty denotation called ⊥_{S} using some denotation approximating function progression_{S} to construct a denotation (meaning ) for S as follows:
It would be expected that progression_{S} would be monotone, i.e., if x≤y then progression_{S}(x)≤progression_{S}(y). More generally, we would expect that
This last stated property of progression_{S} is called ω-continuity.
A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for Denote_{S}. A fundamental theorem of computational domain theory is that if progression_{S} is ω-continuous then Denote_{S} will exist.
It follows from the ω-continuity of progression_{S} that
The above equation motivates the terminology that Denote_{S} is a fixed point of progression_{S}.
Furthermore this fixed point is least among all fixed points of progression_{S}.
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 "<expression_{1}> + <expression_{2}>". Compositionality in this case is to provide a meaning for "<expression_{1}> + <expression_{2}>" in terms of the meanings of <expression_{1}> and <expression_{2}>.
The Actor model provides a modern and very general way the compositionality of programs can be analyzed. 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 concurrent 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 concurrent programming languages. One solution to this problem is to use the Actor model of computation. In Actor model, programs are Actors that are sent Eval messages with the address of an environment (explained below) so that programs inherit their denotational semantics from the denotational semantics of the Actor model (an idea published in Hewitt [2006]).
Environments hold the bindings of identifiers. When an environment is sent a Lookup message with the address of 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 Actor (process) C that has an address (called body) for <L> and an address (called environment) for E. The Actor "(<L> 1 2)" then sends C the message [1 2].
When C receives the message [1 2], it creates a new environment Actor F which behaves as follows:
The Actor (process) C then sends an Eval message with environment F to the following actor (process):
λ(message) if (message == "getLeft") then leftSubTree else if (message == "getRight") then rightSubTree
For another example consider the Actor for the expression "<expression_{1}> + <expression_{2}>" which has addresses for two other actors (processes) <expression_{1}> and <expression_{2}>. When the composite expression Actor (process) receives an Eval message with addresses for an environment Actor E and a customer C, it sends Eval messages to <expression_{1}> and <expression_{2}> with environment E and sends C a new Actor (process) C_{0}. When C_{0} has received back two values N_{1} and N_{2}, it sends C the value N_{1} + N_{2}. In this way, the denotational semantics for process calculi and the Actor model provide a denotational semantics for "<expression_{1}> + <expression_{2}>" in terms of the semantics for <expression_{1}> and <expression_{2}>.
The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs (see [Hewitt 2008a]). For example it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as delays and futures.
In his doctoral dissertation, Will Clinger developed the first denotation semantics for the Actor model.
Clinger [1981] explained the domain of Actor computations as follows:
In his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:
From the article on Power domains: P[D] is the collection of downward-closed subsets of domain D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.
In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:
Hewitt [2006b] published a new denotational semantics for Actors based on Timed Diagrams. The Timed Diagrams model stands in contrast to Clinger [1981] which constructed an ω-complete power domain from an underlying incomplete diagrammatic domain, which did not include time. The advantage of the domain Timed Diagrams model is that it is physically motivated and the resulting computations have the desired property of ω-completeness (therefore unbounded nondeterminism) which provides guarantee of service.
Timed Diagrams denotational semantics constructs an ω-complete computational domain for Actor computations. In the domain, for each event in an Actor computation, there is a delivery time which represents the time at which the message is delivered such that each delivery time satisfies the following conditions:
The Actor event timed diagrams form a partially ordered set <TimedDiagrams, ≤>. The diagrams are partial computation histories representing "snapshots" (relative to some frame of reference) of a computation on its way to being completed. For d1,d2εTimedDiagrams, d1≤d2 means d1 is a stage the computation could go through on its way to d2 The completed elements of TimedDiagrams represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of TimedDiagrams. Concretely, the completed elements are those having no pending events.
Theorem: TimedDiagrams is an ω-complete domain of Actor computations i.e.,
An Actor computation can progress in many ways. Let d be a diagram with next scheduled event e and X ≡ {e’ | e ─≈→_{1-message} e’} (see Actor model theory), Flow(d) is defined to be the set of all timed diagrams with d and extensions of d by X such that
(Recall that δ is the minimum amount of time to deliver a message.)
Flow(d) ≡ {d} if d is complete.
Let S be an Actor system, Progression_{S} is a mapping
Theorem: Progression_{S} is ω-continuous.
Furthermore the least fixed point of Progression_{S} is given by the Concurrency Representation Theorem as follows:
where ⊥_{S} is the initial configuration of S.
The denotation Denote_{S} of an Actor system S is the set of all computations of S.
Define the time abstraction of a timed diagram to be the diagram with the time annotations removed.
Representation Theorem: The denotation Denote_{S of an Actor system S is the time abstraction of}
Using the domain TimedDiagrams, which is ω-complete, is important because it provides for the direct expression of the above representation theorem for the denotations of Actor systems by directly constructing a minimal fixed point.
The criterion of continuity for the graphs of functions that Scott used to initially develop the denotational semantics of functions can be derived as a consequence of the Actor laws for computation as shown in the next section.