Denotational Semantics of The Actor Model - Actor Fixed Point Semantics

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 (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:

Denote_S ≡ ⊔_i∈ω progression_Si(⊥_S).

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

If ∀i∈ω x_i≤x_i+1, then progression_S(⊔_i∈ω x_i) = ⊔_i∈ω progression_S(x_i)

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

progression_S(Denote_S) = Denote_S

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.