Actor transition algebra

This is the canonical semantic map for Bombay Behavior.

Laws and project constructions

The actor-model laws preserved here are:

1. an actor processes one accepted communication at a time;
2. a transition may communicate with known recipients, create fresh actors, and designate the behavior used for the next communication; and
3. a newly allocated actor address is fresh with respect to the actor configuration.

Bombay derives a concrete typed construction from those laws:

Behavior::transition(ActiveTurn, Behavior::Event)
    -> Result<Actions<Addr, Phase, Sends, Birth>, Error>

Actions is the only effect boundary. Typed send products, closed creation products, initialization effects, phases, explicit termination, structural event paths, creator-local child routing, and interpretation order are Bombay constructions and policies, not claims about the surface syntax of Agha's formal calculus.

Four orthogonal roles

A protocol is not a behavior. It has no state, initialization, internal event lanes, effects, errors, phases, or birth capabilities. A behavior is not a protocol supertrait: senders need only the destination's public signature, not proof of its current implementation.

A nominal actor may implement both traits and use Behavior::Protocol = Self. Transparent wrappers preserve the inner protocol while changing the concrete behavior and event/effect algebra.

InitializationTurn and ActiveTurn cannot be constructed directly by an application. The public initialize(&mut B) and delegate_transition(&mut B, event) functions are trusted composition and runtime ports: they can be called repeatedly, and the latter can run before initialization. The consuming behavior_actors::Activate::initialize path enforces one initialization for its owned definition and returns Active<B> for mailbox ingress. A runtime or wrapper using the raw ports must enforce the same lifecycle order itself.

Destination evidence

P is always canonical protocol identity. O is structural occurrence evidence used to navigate duplicate child declarations. It is not a key, address, or second identity.

The runtime selects exact message endpoints through RecipientAddress::Established<P>. Actor-hosting namespaces additionally select EndpointAddress::Installed<B>, which projects the endpoint and keeps matching B::Event authority. Generic application types and protocol owners do not implement key traits or carry runtime types. The inert endpoint family requires Clone, not Send. InterpretSends and concrete request interpretation require Send when an effect actually crosses an asynchronous executor boundary.

Fresh creation

CreateChild<A, C> stages a concrete child behavior, creator-local nonce, and CreationKind. Staging allocates nothing. The nonce cannot be converted to an address and proves neither identity nor freshness.

The interpreter performs, in order:

1. reserve an address fresh with respect to the actor configuration, without publishing a live endpoint;
2. run the child's pure definition initialization fold;
3. install the endpoint and commit the creator-local nonce binding;
4. interpret and settle all initialization effects; and
5. permit ordinary mailbox ingress only if initialization continues and its effects settle successfully.

Only the committed path may produce ChildCreationOutcome<C, Occurrence>::Established(CommittedChild<C, Occurrence>). A later named report may return EstablishedCreation<C, Occurrence>::Installed with the same committed product. Allocation rejection returns the complete staged creation before the initialization fold. Pure initialization rejection returns the current child and exact error; host rejection after that fold returns the current child and uninterpreted initialization Actions. A caught pure initialization panic returns the extant current child through InitializationPanicked, without claiming an initialization error or accepted actions. None of these outcomes commits a binding. Once committed, an initialization-effect failure belongs to the installed child's drain and cannot be reported as a creation rejection. An initialization Stop still settles its final actions and never enables ordinary ingress. A nonce collision is rejection, never replacement or overwrite.

These commit and settlement steps are Bombay policy, not Agha's allocation law. Agha et al.'s newadr and initbeh are separate model operations; Bombay packages fresh allocation, the pure fold, and establishment into one staged creation request.

CreationKind::ReplacementIncarnation records Behavior-authored provenance. It is still fresh allocation. A runtime may report a restart only after the corresponding replacement creation commits successfully.

Creation facts are indexed by canonical child protocol and structural occurrence—not by an entire parent behavior. A fact can be strengthened to EstablishedActor<RoleChild<Parent, Occurrence>> only at the topology boundary where ChildRole<Parent> genuinely proves the concrete installed behavior. This avoids forcing arbitrary consumers or wrappers to pretend to be actors.

Event and effect composition

EventLayer<Owned, Inner> forms a closed event sum. Here identifies the current owner and Inside<Path> identifies an inner owner. InjectEvent constructs exactly the selected lane; it never searches by payload type.

SendLayer<Owned, Inner> is the corresponding named effect product. SendsFor<Event> proves that every interpreter request returning to its emitter has a valid structural ingress. InterpretSends visits inner effects before wrapper-owned effects, preserving initialization and delegated transition order. Independent named lanes retain their own order; no global order is invented between unrelated lanes.

Composition must preserve these invariants:

• every accepted event produces one result;
• mapping sends preserves creations and the exact next verdict;
• mapping the next verdict preserves sends and creation order;
• wrapping cannot drop, duplicate, reinterpret, or consume an inner lane;
• duplicate structural occurrences remain distinct;
• established, child, and external destinations are not reindexed merely because the emitting behavior is wrapped; and
• controlled failure emits no partial effects.

Static interpretation

ActionItem fixes the outcome vocabulary of each emitted value. SendSettlements fixes the complete product shape independently of any runtime. InterpretItem and InterpretSends are the monomorphized runtime capabilities. Closed child sums use DispatchBirth and one EstablishChild<Occurrence, Child> implementation per concrete occurrence. Missing support fails to compile.

ChildOccurrenceProduct is the structural product needed by runtimes that retain creator-local state per direct child occurrence. Behavior owns the closed Behavior leaf / ChildChoice / Never recursion and supplies the same ChildHead / ChildTail<_> navigation evidence used by child creation. A runtime-owned ChildOccurrenceShape supplies only the storage constructor. This is a type-level derived construction, not an actor operation: it performs no transition, allocation, binding, lookup, or effect interpretation. Transitive descendants remain owned by the concrete child actors that may create them.

ResolveChildOccurrence<O> supplies the inverse static connection needed when an effect names O: the running emitter and occurrence determine one exact direct child behavior and structural position. Generated nominal roles are resolved through BehaviorBase only while protocol and birth topology remain identical; raw ChildHead/ChildTail<_> positions inspect the emitter's own closed birth node. Consequently a supervision wrapper that replaces a direct child with a proxy cannot silently reinterpret the base role. This is navigation evidence derived from Behavior, not a new identity or effect.

No core path uses trait objects, runtime protocol registries, reflection, downcasting, type-name dispatch, serialization, or unsafe type escape hatches.

Code map

• crates/behavior/src/transition.rs: protocol and behavior contracts
• crates/behavior/src/effects/: actions and static send interpretation
• crates/behavior/src/actor/addressing.rs: logical and established recipients
• crates/behavior/src/actor/creation.rs: staged creation and structural dispatch
• crates/actors/src/protocol/established.rs: exact creation, observation, and shutdown protocols
• crates/actors/src/requirements.rs: occurrence-preserving installation requirements