Chapter 15
Glossary
| Symbol | Meaning | Where |
|---|---|---|
| Γ, γ | Context type; a state. | §3.1 |
| ∂Γ = Γ × (Γ→Γ) | Effect context: state + accumulator φ. track, recover; soundness invariant φ(γ)=γ₀. | Defs 2, 3, 6; Thm 7 |
| 𝔗Γ | Twisted-composition monoid of (f, g) pairs. | Def 1 |
| 𝔈Γ, 𝔈Γ*, ⋄, η | Effect function Γ→Γ×(Γ→Γ); witnessed (g(δ)=γ); composition; unit. | Defs 8, 9; Thm 10 |
| effectΓ | Lift 𝔈Γ → 𝔈∂Γ; its inverse is track(g, pr₁∘e). | Def 12; Thms 13–15 |
| ℑΓ, ℑΓ*, ℑΓ^S | Effect iterator (generator); witnessed; witnessed up to ≃_S. | Defs 17, 37 |
| Σ, get, set | Coeffect context (k:K)⇀𝒱ₖ; read; provide-with-inverse. | Defs 19–20 |
| 𝔇, σ ⊧ d, notify_d | Specification (set of keys); satisfaction; classification activating/deactivating/neutral. | Defs 21–22 |
| Σiso, ρ, R | Isolation: realm table, realm identifiers; access σ(ρ(k)). | Defs 24–25 |
| Σinter, ι, ℳₖ, ⊕ₖ | Interception: context metadata, per-key monoid; value = σ(k)(d(k) ⊕ ι(k)), right-biased. | Defs 26–27 |
| Γ∞ | μΓ. Γ × (Γ→Γ) × Σ — the unified, recursive context. | Def 28 |
| (𝒱ₖ, 𝒜ₖ, witness) | A coeffect at a key: value type, operations, commutativity proof. | Defs 29, 46 |
| ≃ₖ, ≃_S, ≃ | Indistinguishability under 𝒜ₖ's tests; on contexts at keys S; on whole states incl. control fields. | Defs 31, 33, 34; Def 58 |
| 𝔐(i), reach(i), len(i) | Transformation monoid of an iterator; reachable iterators; longest chain. | Def 40 |
| independent; commutative key; entangled | Def 42; Def 44; fibers whose provision meets the other's keys (Def 65). | §3.4, §4.3.2 |
| ℭΓ ∋ (d, p, e) | Component: declares, provides, effect iterator. | Def 48 |
| fiber ⟨d,p,e,π,σ,τ,θ⟩ | Instantiation: parent, own table, retired flag, lifecycle state. | Def 49 |
| θ | Inactive | Reloading(i,g,ω) | Active(g,ω) | Unloading(g,ω). | Def 49 |
| ω, target_n, relied_n, installed_n, quiet | Committed view; target view; "some installed fiber's ω names n"; θ ≠ Inactive; every fiber at target. | Defs 49, 53, 54 |
| σ_γ, provider_k | ⋃ tables of Active fibers; the one Active fiber binding k. | Def 50 |
| episode; Ψᵗ / editᵗ | Maximal interval a fiber is installed; a step's state-map half / control-edit half. | Def 58 |
| ≺, ⊲, A | pₙ∩dₘ≠∅; ≺ ∪ parent; support set. | Defs 72, 74 |
| total on provision | A finishing activation installs all of p. | Def 76 |
| Cordis names | ctx.effect, ctx.provide/get/set, ctx.isolate/intercept, ctx.plugin (paper: use), inject, provide, fiber.store (paper: committed), runner.epoch (paper: fiber.target), fiber.inertia, FiberState. | §5, ch. 10 |