In theoretical computer science, Actor model theory concerns theoretical issues for the Actor model. Actors are the primitives that form the basis of the Actor model of concurrent digital computation. In response to a message that it receives, an Actor can make local decisions, create more Actors, send more messages, and designate how to respond to the next message received. Actor model theory incorporates theories of the events and structures of Actor computations, their proof theory, and denotational models.
Events and their orderings
From the definition of an Actor, it can be seen that numerous events take place: local decisions, creating Actors, sending messages, receiving messages, and designating how to respond to the next message received. However, this article focuses on just those events that are the arrival of a message sent to an Actor. This article reports on the results published in Hewitt .
Activation ordering
The activation ordering is a fundamental ordering that models one event activating another.
Because of the transmission of energy, the activation ordering is relativistically invariant; that is, for all events e1.e2, if e1 -≈→ e2, then the time of e1 precedes the time of e2 in the relativistic frames of reference of all observers.
Law of Strict Causality for the Activation Ordering: For no event does e -≈→ e.
Law of Finite Predecession in the Activation Ordering: For all events e1 the set is finite.
Arrival orderings
The arrival ordering of an Actor x models the ordering of events in which a message arrives at x. Arrival ordering is determined by arbitration in processing messages. The arrival events of an Actor are on its world line. The arrival ordering means that the Actor model inherently has indeterminacy.
Because all of the events of the arrival ordering of an actor x happen on the world line of x, the arrival ordering of an actor is relativisticallyinvariant. I.e., for all actors x and events e1.e2, if e1 -x→ e2, then the time of e1 precedes the time of e2 in the relativistic frames of reference of all observers.
Law of Finite Predecession in Arrival Orderings: For all events e1 and Actors x the set is finite.
Combined ordering
The combined ordering is defined to be the transitive closure of the activation ordering and the arrival orderings of all Actors.
The combined ordering is relativistically invariant because it is the transitive closure of relativistically invariant orderings. I.e., for all events e1.e2, if e1→e2. then the time of e1 precedes the time of e2 in the relativistic frames of reference of all observers.
Law of Strict Causality for the Combined Ordering: For no event does e→e.
The combined ordering is obviously transitive by definition. In , it was conjectured that the above laws might entail the following law:
Independence of the Law of Finite Chains Between Events in the Combined Ordering
However, surprisingly proved that the Law of Finite Chains Between Events in the Combined Ordering is independent of the previous laws, i.e., Theorem. The Law of Finite Chains Between Events in the Combined Ordering does not follow from the previously stated laws. Proof. It is sufficient to show that there is an Actor computation that satisfies the previously stated laws but violates the Law of Finite Chains Between Events in the Combined Ordering. However, we know from physics that infinite energy cannot be expended along a finite trajectory. Therefore, since the Actor model is based on physics, the Law of Finite Chains Between Events in the Combined Ordering was taken as an axiom of the Actor model.
Law of Discreteness
The Law of Finite Chains Between Events in the Combined Ordering is closely related to the following law: In fact the previous two laws have been shown to be equivalent: The law of discreteness rules out Zeno machines and is related to results on Petri nets . The Law of Discreteness implies the property ofunbounded nondeterminism. The combined ordering is used by in the construction of a denotational model of Actors.
