Denotational semantics of the Actor model
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 .
Actor fixed point semantics
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 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 for a system S is found by constructing increasingly better approximations from an initial empty denotation called ⊥S using some denotation approximating function progressionS to construct a denotation for S as follows:
It would be expected that progressionS would be monotone, i.e., if x≤y then progressionS≤progressionS. More generally, we would expect that
This last stated property of progressionS is called ω-continuity.
A central question of denotational semantics is to characterize when it is possible to create denotations according to the equation for DenoteS. A fundamental theorem of computational domain theory is that if progressionS is ω-continuous then DenoteS will exist.
It follows from the ω-continuity of progressionS that
The above equation motivates the terminology that DenoteS is a fixed point of progressionS.
Furthermore, this fixed point is least among all fixed points of progressionS.
Compositionality in programming languages
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 "The Actor model provides a modern and very general way the compositionality of programs can be analyzed. Scott and Strachey 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. 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 so that programs inherit their denotational semantics from the denotational semantics of the Actor model.
Environments
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 binding of x.As an example of how this works consider the lambda expression
λ
λ
if then leftSubTree
else if then rightSubTree
Consider what happens when an expression of the form "" is sent an Eval message with environment E. One semantics for application expressions such as this one is the following:
However,
When C receives the message ', it creates a new environment Actor F which behaves as follows:
- When it receives a Lookup message for the identifier leftSubTree, it responds with 1
- When it receives a Lookup message for the identifier rightSubTree, it responds with 2
- When it receives a Lookup message for any other identifier, it forwards the Lookup message to E
λ
if then leftSubTree
else if then rightSubTree
Arithmetic expressions
For another example consider the Actor for the expression "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.Clinger's Model
In his doctoral dissertation, Will Clinger developed the first denotation semantics for the Actor model.The domain of Actor computations
Clinger explained the domain of Actor computations as follows:Denotations
In his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:From the article on Power domains: P 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 is given by the subset relation, least upper bounds do not in general coincide with unions.
Sequential computations form an ω-complete subdomain of the domain of Actor computations
In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:The Timed Diagrams Model
Hewitt published a new denotational semantics for Actors based on Timed Diagrams. The Timed Diagrams model stands in contrast to Clingerwhich 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 which provides guarantee of service.
Domain of Timed Actor Computations
Timed Diagrams denotational semantics constructs an ω-complete computationaldomain 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 delivery time is a positive rational number that is not the same as the delivery time of any other message.
- The delivery time is more than a fixed δ greater than the time of its activating event. It will later turn out that the value of δ doesn't matter. In fact the value of δ can even be allowed to decrease linearly with time to accommodate Moore's Law.
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.,
- If D⊆TimedDiagrams is directed, the least upper bound ⊔D exists; furthermore ⊔D obeys all the laws of Actor model theory.
- The finite elements of TimedDiagrams are countable where an element xεTimedDiagrams is finite if and only if D⊆TimedDiagrams is directed and x≤VD, there exists dεD with x≤d. In other words, x is finite if one must go through x in order to get up to or above x via the limit process.
- Every element of TimedDiagrams is the least upper bound of a countable increasing sequence of finite elements.
Power domains
- Definition: The domain
, ⊆> is the set of possible initial histories M of a computation such that - # M is downward-closed, i.e., if dεM, then ∀d’εTimedDiagrams d’≤d ⇒ d’εM
- # M is closed under least upper bounds of directed sets, i.e. if D⊆M is directed, then VDεM
- Note: Although Power is ordered by ⊆, limits are not given by U. I.e.,
- : ⇒ Ui∈ω Mi ⊆ ⊔i∈ω Mi
- : E.g., If ∀i diεTimedDiagrams' and di≤di+1 and Mi= then
- ::⊔i∈ω Mi = Ui∈ωMi U
- Theorem:'' Power is an ω-complete domain.
Concurrency Representation Theorem
Let d be a diagram with next scheduled event e and
X ≡ ,
Flow is defined to be the set of all timed diagrams with d and extensions of d by X
such that
- the arrival all of the events of X has been scheduled where
- the events of X are scheduled in all possible orderings among the scheduled future events of d
- subject to the constraint that each event in X is scheduled at least δ after e and every event in X is scheduled at least once in every δ interval after that.
Let S be an Actor system, ProgressionS is a mapping
Theorem: ProgressionS is ω-continuous.
Furthermore, the least fixed point of ProgressionS is given by the Concurrency Representation Theorem as follows:
where ⊥S is the initial configuration of S.
The denotation DenoteS 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 DenoteS 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.