A lookup table for every piece of notation in the book, in the order you meet it. "Read as" is what to say in your head; "Primer §" points at the explanation in chapter 3.
| Symbol | Read as | Meaning | Primer § |
|---|
| X → Y | function from X to Y | Total pure function. | 2 |
| X ⇝ Y | impure function | May touch the world. Used only to motivate making the world explicit. | 2 |
| X ⇀ Y | partial function | Defined on some inputs; dom(·) is where. | 2, 5 |
| x ↦ e | x maps to e | Anonymous function x => e. | 2 |
| λx. e | lambda x | Same as x ↦ e. | 2 |
| f ∘ g | f after g | Composition; g runs first. | 1 |
| id, id_Γ | identity | Returns its argument. | 1 |
| (a : A) → B(a) | for all a of type A | Dependent function; in proofs, "for every a, …". | 9 |
| (a : A) × B(a) | an a together with a B(a) | Dependent pair; used for "value plus proof about it". | 9 |
| μX. F(X) | the recursive type X = F(X) | Generators, lists, nested contexts. | 7 |
| let (a, b) = e in … | destructure | const [a, b] = e. | 3 |
| ≔ | is defined as | Definition, not an equation to solve. | — |
| Symbol | Read as | Meaning | Primer § |
|---|
| X × Y | pairs of X and Y | Product type. | 3 |
| pr₁, pr₂ | first, second | Projections. pr₂,₃ = second and third components. | 3 |
| Maybe(X); Nothing; Just(x) | optional X | Absent or present. | 7 |
| Either(E, X) | error or value | Used for failure (§4.4). | 7 |
| Set(K) | sets of keys | The type of an inject list. | — |
| dom(σ) | domain of σ | Keys the dictionary has. | 5 |
| σ(k), σ[k ↦ v], σ ∖ k | lookup, insert, remove | Dictionary operations (functional: they return new dictionaries). | 5 |
| σ|_S | σ restricted to S | Keep only keys in S. | — |
| ⋃, ∩, ∖, ⊆, ∅ | union, intersection, difference, subset, empty | Ordinary set notation. | — |
| ∀, ∃, ∧, ∨, ¬, ⇒ | for all, exists, and, or, not, implies | Ordinary logic. | — |
| Symbol | Name | Meaning in the paper | Chapter |
|---|
| Γ, γ | Gamma | The context (world) type; a particular world. γ₀: the initial world. | 4 |
| ∂Γ | "del Gamma" | Effect context: Γ × (Γ → Γ), world + accumulator. ∂²Γ = ∂(∂Γ). | 4 |
| φ | phi | The accumulator: composite of all undos so far. | 4 |
| δ, ε | delta, epsilon | Intermediate worlds in a computation. (Not the calculus of limits.) | 4 |
| η | eta | The unit effect γ ↦ (γ, id). | 4 |
| Σ, σ | Sigma | The coeffect context (service table) type; a particular table. σ_γ: the table derived from world γ. | 5 |
| 𝒱ₖ | V sub k | The value type at key k. | 5 |
| ρ, R | rho | Realm table; realm identifiers (isolation). | 5 |
| ι, ℳₖ, ⊕ₖ, εₖ | iota; M sub k | Context-carried metadata; the metadata type at k, its merge, its empty value (interception). | 5 |
| 𝒜ₖ | A sub k | The operations a holder of key k may perform. | 6 |
| Γ∞ | Gamma infinity | The unified recursive context. | 6 |
| ≃, ≃ₖ, ≃_S | equivalent | Observational equivalence: on values at key k; on tables at keys S; on whole states. | 6 |
| π, σ, τ, θ, ω | pi, sigma, tau, theta, omega | Fiber fields: parent, own table, retired flag, lifecycle state, committed view. | 8 |
| Ψᵗ | Psi | The state-changing half of step t. | 9 |
| χ | chi | A renaming of fiber names. | 9 |
| Decorated | Read as | Meaning | Chapter |
|---|
| 𝔗Γ | T Gamma | Pairs (f, g) under twisted composition. | 4 |
| 𝔈Γ, 𝔈Γ* | E Gamma (starred) | Effect functions; witnessed ones. | 4 |
| ℑΓ, ℑΓ*, ℑΓ^S | I Gamma | Effect iterators; witnessed; witnessed up to ≃_S. | 4, 6 |
| 𝔇Σ, 𝔓Γ | D, P | Specifications (inject sets); provisions (provide sets). | 5, 8 |
| 𝔐(i) | M of i | Transformation monoid of iterator i. | 7 |
| ℭΓ, 𝔉Γ, 𝔑 | C, F, N | Components; fibers; fiber names. | 8 |
| ℑ^𝒜_Σ(S, P) | context-mediated iterators | Iterators built only from operations at keys S, provisions at keys P, instantiations. | 6 |
| Symbol | Meaning | Chapter |
|---|
| track(f, g), recover | Push an undo onto the accumulator; run the accumulator. | 4 |
| f ⋄ g | Effect composition (world threaded, undos twisted). | 4 |
| effectΓ, effect^iter_Γ | Lift an effect function / iterator to act on the effect context. | 4 |
| get, set, isolate, intercept | Read; provide-with-undo; redirect a key's realm; add access metadata. | 5 |
| σ ⊧ d | Table satisfies specification (all keys present). ⊭: does not. | 5 |
| notify_d(σ, σ′) | activating / deactivating / neutral. | 5 |
| reach(i), len(i) | Iterators reachable from i; longest step chain. | 7 |
| installed_n, target_n, relied_n, quiet | θ ≠ Inactive; target view; "some installed fiber committed a key to n"; every fiber at its target. | 8 |
| provider_k(γ) | The one Active fiber binding k. | 8 |
| n ≺ m | pₙ ∩ dₘ ≠ ∅: n may provide for m. | 9 |
| m ⊲ n | m ≺ n or m is n's parent (support relation). | 9 |
| A | The support set. | 9 |
| γ ⇒ δ, γ ⟶ δ | An orchestration step; a lifecycle step. | 8 |
| γᵗ, θₙᵗ, stepᵗ | State after t steps; a field of it; the rule applied there. | 9 |
| Word | Here it means |
|---|
| monoid | A set with an associative operation and a unit. Only used for "effects can be sequenced". |
| homomorphism | A map that respects sequencing: h(a ∘ b) = h(a) ∘ h(b). |
| witness / witnessed | A promise, bundled with the value, that a property holds (an inverse reverts; a key's operations commute). Not checked by the runtime. |
| lift | Turn a function on X into one on a richer structure containing X (world → world+accumulator; value → whole table). |
| inverse | Always a left inverse: g ∘ f = id. Nothing is said about f ∘ g. |
| local / global | A guarantee about one component by itself / about every component in an arbitrary interleaving. |
| denotation / realization | What an operation means (new state, undo) / how the host actually does it (mutate, or derive a child). |
| episode | One maximal interval during which a fiber is installed (θ ≠ Inactive). |
| quiescent | No fiber has anything left to do: every one sits at its target. |
| entangled | Two fibers where one provides a key the other declares or provides. |
| inertial | A host that cannot abort an in-flight step; it lets the step land and then reacts. |
| total on provision | A component that, when it finishes activating, has installed every key it said it would. |