BR Model

Bio Running (BR) Model

English | 中文 | Русский | Español | Português | 繁體中文 | Deutsch

Formal execution model of BioLang. This page defines, rigorously, what it means for a BioLang program to run. Notation is standard mathematical/type-theoretic; no prior knowledge beyond basic set theory is required.

1. Programs as stream networks

Definition 1.1 (Program). A program is a tuple

P = (Streams, Decls, Main)

where Streams is a finite set of stream names, Decls a finite set of declarations (signatures, forks, classes, constants, needs), and Main a distinguished stream with an entry method exec().

Definition 1.2 (Stream). A stream is a named container of methods and fields:

s ∈ Streams,   s = (M_s, F_s)

• M_s — set of methods, each m = (name, params, body, ann) where ann ⊆ {read, write, call, ucall, builtin} are annotations.
• F_s — set of fields (typed slots).

Intuition: a stream is a pipe; methods are the valves on it. Forking a stream (Greeter Friendly { ... }) creates a new stream that implements the signature's contract — like a new pipe connected to the same valve specification.

2. The request algebra

Definition 2.1 (Request). Every operation is a request q drawn from the set of all calls Q. A request carries a method name, a receiver stream, and arguments: q = (s, m, a⃗).

Definition 2.2 (Result). The result of a request is a result value:

Result = Res(Value) ⊎ Ref(Reason)

• Res(v) — the request succeeded, with value v.
• Ref(r) — the request was refused, with reason r (a string).

⊎ denotes a disjoint union: every request resolves to exactly one of the two, never both, never neither. This is the request totality axiom.

Axiom 2.3 (Totality). For every request q, the evaluation relation ⟦q⟧ yields exactly one result in Result.

Axiom 2.4 (Refusal transparency). A refusal is a value, not an exception: Ref(r) can be inspected (cause q), stored, passed, and forwarded. Refusals compose:

⟦q₁; q₂⟧ = Ref(r)   if ⟦q₁⟧ = Ref(r)      (short-circuit)
⟦f(q)⟧   = Ref(r)   if ⟦q⟧ = Ref(r)        (propagation)

Definition 2.5 (Unwrapping). The prefix operators extract the payload:

get q   = v            if ⟦q⟧ = Res(v)
cause q = r            if ⟦q⟧ = Ref(r)
ALL x   = q            captures the whole result;  x.res / x.cause project it.

Philosophical note. The request algebra models epistemic modesty: a programmer cannot assume a request succeeds; success must be earned and failure is first-class. This mirrors the Stoic distinction between what is in our power (making the request) and what is not (the outcome).

3. Execution state

Definition 3.1 (State). An execution state is a tuple

σ = (A, L, B)

• A — the arena: a growable pool of memory blocks. Allocation aalloc(n) appends to the current block; memory is never freed and never moved during a run (block-based, stable pointers).
• L — the layer stack: a chain of scopes l₀ → l₁ → ... → lₖ (program layer, area layers, method scopes). Variable lookup walks the chain (var_get_layer).
• B — the booth registry: the set of phone-booth memory regions (see §5).

Definition 3.2 (Transition). A request q transforms state:

σ --q--> σ'

The transition is total (2.3) and deterministic in single-threaded execution (the interpreter is a pure sequential machine; no observable nondeterminism without threads).

4. Layers and reference resolution

Definition 4.1 (Layer). A layer is a finite map from names to values: l : Name ⇀ Value. Layers form a chain ordered by scope depth.

Axiom 4.2 (Shadowing). Name resolution returns the binding of the innermost layer containing the name:

lookup(name, l₀→...→lₖ) = lᵢ(name)   where i = min{j : name ∈ dom(lⱼ)}

Definition 4.3 (Smart reference). A smart reference is a typed triple

ref = (perm, follow, target)

• perm ∈ {r, w, m, rw, rm, wm, rwm} — permission stack.
• follow ∈ {u, f, a, t} — resolution layer (program / method / area / thread).
• target — an lvalue: variable slot, array element, or object field.

Axiom 4.4 (Permission). For every reference operation op:

op(ref) = Ref("reference is read-only, cannot write")   if w ∉ perm ∧ op = write
op(ref) = Ref("reference is write-only, cannot read")   if r ∉ perm ∧ op = read
op(ref) = Ref("pointer moved out of bounds")            if m ∉ perm ∧ op = move

The 7 × 4 = 28 reference types are exactly the non-empty subsets of {r, w, m} crossed with {u, f, a, t}.

5. The phone-booth memory model

Definition 5.1 (Phone booth). A phone booth is a fixed memory region with a state flag:

booth = (region, in_use)

Axiom 5.2 (Booth discipline). For a phone-booth method m:

1. Reset: on entry, the region is cleared (allocator head reset) — no allocation, no fragmentation, zero memory movement.

2. Exclusivity: in_use is set for the duration of the call. Any entry while in_use is refused:

   ⟦m(a⃗)⟧ = Ref("phone-booth method m does not support recursion")
   

   This makes recursion impossible by construction — the booth is a single booth; one cannot take two calls in it at once.

3. Reuse: after the call, the region is retained (not freed); the next call reuses it.

4. Isolation: @call booths are per-thread (boothₜ for thread t); @ucall has a single global booth. Two threads calling the same @call method use disjoint regions — no interference.

Theorem 5.3 (Booth isolation). If m is @call, concurrent invocations of m from distinct threads touch disjoint memory.

Proof sketch. Each thread owns a distinct booth region (5.2.4); allocations inside the method come from its own region (5.2.1); hence no shared mutable state exists between the invocations. ∎

Corollary 5.4 (No recursion). No phone-booth method can call itself, directly or transitively, because every re-entry sees in_use and is refused (5.2.2).

Metaphor. A phone booth: one caller at a time; the booth is cleaned between calls but never demolished; every street corner (thread) has its own booth so callers never queue on each other. Recursion is the attempt to be inside the booth while you are already inside it — the door refuses.

6. Semantic properties

Theorem 6.1 (Determinism). In a single-threaded run, for any program P and initial state σ₀, the execution trace σ₀ → σ₁ → ... is unique.

Proof sketch. Every transition (3.2) is deterministic (each request has a unique result by 2.3, and the interpreter performs no randomized or time-dependent choices). ∎

Theorem 6.2 (Arena stability). Pointer values returned by aalloc remain valid for the entire run.

Proof sketch. Blocks are only appended, never moved or freed (3.1). ∎

Theorem 6.3 (Failure locality). A refusal in a sub-request cannot corrupt the enclosing state: σ --q--> σ' with ⟦q⟧ = Ref(r) modifies no observable bindings of L.

Proof sketch. Refusals return before any assignment is committed; the transition applies the request's side effects only on Res. ∎

7. Discussion

The BR model separates three concerns cleanly:

Concern	Model element
What a program is	stream network (Def. 1.1)
How operations behave	request algebra (Def. 2.1–2.5)
Where state lives	arena + layers + booths (Def. 3.1, 5.1)

The request algebra is what makes BioLang's error handling algebraic rather than exceptional: refusals are ordinary values, so every function is total — there is no "undefined behaviour" channel, only Ref.

See Bio Task Manager (BTM) Model for the formal treatment of threads, tasks, and scheduling.