Framework Lexicon
Part of the cognition series. Reference post — updated as vocabulary sharpens.
Several mathematical communities have independently formalized overlapping structures under different names. This post maps the translations.
If you’re here because you found your name: The Rosetta stone below maps your work to parallel results in other communities. The dashes mark where one community has no term for a concept the other has named.
Authors cited: Fritz, Spivak, Gaboardi, Katsumata, Kura, Jacobs, Liell-Cock, Staton, Perrone, Leinster, Baez, Sato, Chen, Vigneaux, Rezagholi.
Rosetta stone: same objects, different names
Corrections welcome — june@june.kim.
| PL theory | Categorical probability | Shared object | Framework | Confidence |
|---|---|---|---|---|
| Kleisli(D) Jacobs 2014 | FinStoch Fritz 2020 | Category of finite sets + stochastic matrices | Ambient category post | Exact. Same category |
| Hoare triple {P} c {Q} Gaboardi 2021 | — | Predicate on morphism outputs, preserved under composition | Contract post | Plausible. Same role; grades differ |
| Restricted pointwise order Kura-Gaboardi 2026 Def 7 | — | Post(N) implies Pre(N+1), restricted to support | Handshake Comp.lean | Exact. forward_triple chains four COMP rules through real pre/postconditions. Each stage's postcondition is the next stage's precondition — the restricted pointwise order, machine-checked. |
| wp via poset fibration over Kleisli(D) Jacobs 2014 | Posetal imperative category Staton 2025 Cor. 76 | Predicate logic over a stochastic category | "Fibration" post | Exact. Staton proves Hoare rules over Stoch (Thm 79) |
| Graded Freyd category Gaboardi 2021 | Graded Markov category Liell-Cock & Staton 2025 | Effectful computation with tracked side-effects | Stage + contract Lean | Plausible. Freyd vs. Markov differ on exponentials |
| Divergence on monad Sato-Katsumata 2023 | Enriched Markov category Perrone 2023 | Metric on morphism spaces for verification | NonExpanding Lean | Plausible. Different enrichment categories |
| — | Possibilistic shadow Υ Fritz et al. 2023 | Possibilistic collapse of a probabilistic morphism | Support typeclass Support.lean | Exact. support_bind = monad multiplication |
| — | supp : V ⇒ H Fritz-Perrone-Rezagholi 2021 | Monad morphism: valuations → closed subsets | support_bind Support.lean | Exact. Same composition law |
| — | Static idempotent Fritz et al. 2023 Prop 4.4.1 | Idempotent that stabilizes after one step | IterationStable Contracts.lean | Plausible. Ours is weaker than Fritz's splitting |
| — | Magnitude Leinster 2021 | Categorical cardinality / effective species count | Diversity post | Speculative. No composition law for magnitude |
| Free ℕ-semimodule monad Kidney & Wu 2021 | Double dualization Fritz-Perrone-Rezagholi 2021 | Counting monad parameterized by semiring S | Gap supp composed with |·| | Speculative. Exists on Set, not via double dualization on Top |
| Selection relation on parametrised optics Capucci et al. 2021 | — | "What is a goal but a predicate on a system?" Compositional predicate on morphisms. | Contract post | Plausible. Same role (behavioral predicate); different ambient structure (optics vs. Kleisli) |
| Nash equilibrium as compositional predicate Ghani-Hedges et al. 2018 | — | Equilibrium checked locally on subgames, preserved under game composition | Contract preserved under composition Lean | Plausible. Structural parallel; games ≠ pipelines |
| Bayesian lens / statistical game Smithe 2021 | Bayesian inversion in Markov category Braithwaite-Hedges-Smithe 2023 | Optic with forward (inference) and backward (learning) pass over stochastic morphisms | Forward pipeline + Consolidate post | Plausible. Both have forward+backward; optic composition ≠ Kleisli composition |
| — | Dagger structure on kernels Parzygnat 2020 | Bayesian inversion as categorical involution on morphisms | Consolidate (backward pass) post | Speculative. Consolidate updates policy; dagger inverts morphisms. Related but not the same operation |
| Effect algebra predicates (X → 1+1) Cho-Jacobs 2015 | — | Predicates as effects, not subobjects. States/effects duality. | Contract Lean | Plausible. Both are predicates on outputs; effect algebras are quantitative, ours are Boolean |
| Partial correctness Standard PL | Partial Markov categories Di Lavore-Roman-Sobocinski 2025 | Morphisms can fail. Observations, normalization, conditioning in restriction categories. | — (pipeline assumes total morphisms) | Plausible. Pipeline stages don't fail; but Filter's rejection maps to partiality |
| Program equivalence metrics Panangaden 2009 | — | Bisimulation metrics = behavioral distance between stochastic processes | — (no framework analog) | Speculative. Could connect to magnitude as behavioral distance. Nobody has tried. |
Pipeline structure
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Operad algebra | Spivak 2013 | The six roles are boxes in a wiring diagram. Typed ports constrain which boxes connect. | Pipeline |
| Type forcing | Type Forcing post + Lean proof | Given the six interface types, the supplier assignment is unique. Pipeline topology is forced. | Wiring uniqueness |
| Stoch — Markov category | Fritz 2020 | The category the pipeline lives in. Measurable spaces + Markov kernels. Copy/delete structure. | Ambient category |
| Kleisli arrow α → M β | Standard | Each pipeline stage is a monadic kernel. When M = Id, it's a deterministic function. | Kernel |
| Kleisli composite of five kernels | Lean proof (Pipeline.lean) | Perceive → Cache → Filter → Attend → Remember. Five morphisms composed via >=>. | Forward pipeline |
| Traced monoidal category | Joyal-Street-Verity 1996 | Remember's output feeds Perceive's input. The loop closes via a trace operator. | Feedback loop |
| Forward + Consolidate | Lean proof (Pipeline.lean) | One complete iteration: forward pass produces ranked output, Consolidate updates policy. | Cycle |
Deterministic / stochastic boundary
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Copy-natural morphism | Fritz 2020 §10 | Filter is deterministic: same input, same gate. Commutes with copy. Lives in Cdet. | Deterministic morphism |
| Copy-non-natural morphism | Fritz 2020 | Attend must be stochastic: deterministic selectors cycle, killing diversity. | Stochastic morphism |
| Cartesian subcategory Cdet | Fritz 2020 §10 | Filter lives inside. Attend crosses out. Cdet closed under composition — two det morphisms compose to det. | Cdet boundary |
| Pigeonhole → state collision | Lean proof (Stochasticity.lean, Pigeonhole.lean) | Deterministic transducer over Fin N must collide within N+1 steps. Confusion → error. | Stochasticity is mandatory |
Information theory
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| F(f) = c(H(p) − H(q)) | Baez-Fritz-Leinster 2011 | The pipeline's information budget. Unique form under functoriality + convex-linearity + continuity. FinProb only. | Information loss |
| Functorial nonneg loss accumulates | Baez-Fritz-Leinster 2011 | Information only decreases through pipeline stages. Post-processing can't recover lost bits. | DPI |
| t ≤ s iff t = c ∘ s (a.s.) | Fritz 2020 Def 16.1 | Consolidate's output is a sufficient statistic. Retains task-relevant info, discards the rest. | Informativeness preorder |
| Distance from determinism | Fritz-Gonda-Perrone-Rischel 2024 | Measures how far a morphism is from being deterministic. Enriched Markov categories. | Categorical entropy |
| Divergences in enriched hom-spaces | Perrone 2023 | Fisher metric lives in the enrichment. Potential home for Consolidate's update dynamics. | Info geometry |
| Magnitude / Hill number | Leinster 2021 | Hill at q=0 = support size = species richness. Diversity IS categorical cardinality (magnitude). | Diversity |
Support and possibilism
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Possibilistic shadow Υ : C → SetMulti | Fritz et al. 2023 | The Lean proof's Support class IS this. Collapses probabilistic to possibilistic. support_bind = monad multiplication for supp : V ⇒ H. | Support typeclass |
| Unit of Hoare hyperspace monad H | Fritz-Perrone-Rezagholi 2021 | σ(x) = cl({x}). Pure computation has singleton support. | support_pure |
| supp(E(ξ)) = U(supp#(supp(ξ))) | Fritz-Perrone-Rezagholi 2021 | Support of composite = closure of union of conditional supports. Bind distributes support via existential. | support_bind |
| Closed subsets, lower Vietoris topology | Fritz-Perrone-Rezagholi 2021 | The codomain of the support monad morphism. Algebras are complete join-semilattices. | Hoare hyperspace H |
| Functorial iff causal | Fritz et al. 2023 Thm 3.1.19 | Causality axiom = composition condition for supports. The pipeline is causal. | Support is functorial |
| Static idempotent (e =e id) | Fritz et al. 2023 | Iteration-stable = static idempotent. Splitting = having a support (Prop 4.4.1). Fixed-point structure captured by support object. | IterationStable |
| Gap: |Υ(p)| as lax functor | Nobody yet | Cardinality of possibilistic shadow. Would connect Leinster magnitude to Fritz support. Missing bridge for diversity. | Diversity (Attend) |
Contracts and composition
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Predicate on outputs (β → Prop) | Lean proof | Each pipeline stage carries a postcondition. All six contracts quantify over the support of the kernel. | Contract |
| Hoare postcondition | Gaboardi et al. ESOP 2021 | Graded Hoare logic gives pre/postconditions for graded monads categorically. ContractPreserving IS a Hoare triple. | ContractPreserving |
| Restricted pointwise order | Kura-Gaboardi et al. 2026 Def 7 | f ≤P g iff ordering holds where predicate is non-bottom. Post(N) implies Pre(N+1), restricted to support. forward_triple chains four COMP rules through real pre/postconditions — machine-checked. | Handshake (Comp.lean) |
| Graded monad lifting | Kura-Gaboardi et al. 2026 | Lifting through predicate fibration PredΩ(C) → C. Interpreting in total category preserves fibrational structure. | Contracts propagate |
| PredΩ(C) → C | Jacobs 2001 | Standard construction. SCCompC gives dependent types on top. The fiber over each morphism carries its contracts. | Predicate fibration |
| Para construction Cγ(X,Y) = C(γ⊗X, Y) | Liell-Cock & Staton POPL 2025 | The grade is a tensor factor. Grading and stochastic semantics are the same structure. | Graded monad = Markov cat |
| Op-lax functor R : ImP → Kl(CP) | Liell-Cock & Staton 2025 Thm 5.6 | R(g∘f) ⊆ R(g)∘R(f). Composing in ImP gives tighter uncertainty sets than composing in the quotient. Subset = refinement. | Tighter bounds under composition |
| Bop → PreMon | Kura-Gaboardi et al. 2026 Def 6 | The grading monoid varies with the base index. Effects (contracts) are value-dependent, not just type-dependent. | Indexed preordered monoid |
Variational derivations
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Optimality over feasible set | Lean proof | Element-level: x is feasible and no feasible y has lower cost. Used for Consolidate and Filter. | MinimizesOn |
| Incumbent is always admissible | Lean proof | The current policy is always a feasible candidate. Optimal output ≤ incumbent. Derives Consolidate's lossiness. | self_feasible |
| Nontrivial feasible reduction exists | Lean proof | For every input, a strictly smaller feasible output exists. Minimality + witness → strict reduction. Derives Filter's gating. | strict_witness |
| Contract as optimality condition | Lean proof | Constructors that build contract structures from optimization problems. Plug into existing handshake machinery. | fromOptimal |
Open bridges
| Bridge | Connects | Would give us | Search terms |
|---|---|---|---|
| Hoare logic over Markov category | Bonchi-Di Lavore-Roman-Staton 2025 | CLOSED. Stoch is a posetal imperative category (Cor. 76). All Hoare rules (SKIP, COMP, ASSIGN, LOOP, WHILE...) derived as theorems (Thm 79). Predicates = morphisms X → 1. Triples = inequalities in posetal structure. | Staton's "imperative category" = traced distributive copy-discard category. Markov categories ARE copy-discard categories. Paper explicitly names Stoch and proves the rules. |
| Semiring-valued monad via change of base | Fritz-Perrone-Rezagholi supp : V ⇒ H + Leinster magnitude | Diversity contract derived variationally — DPP maximizes support cardinality under capacity | Double dualization uses a semiring S: {0,1} → reachability, [0,∞) → probability. (ℕ, +, 0) → counting. Not via double dualization, but the free ℕ-semimodule monad (= multiset monad) exists on Set. Jacobs proves a distributive law M∘D → D∘M (multiset over distribution). Compose with support to track cardinality. |
| Categorical DPPs | Exterior algebra functor + Markov categories | The concrete Attend mechanism (DPP kernel) with categorical semantics | determinantal point process categorical; DPP monoidal; L-ensemble categorical |
| Coding theorems | Fritz entropy + Shannon theory | Consolidate's compression as a categorical rate-distortion theorem | rate-distortion Markov category; Wyner-Ziv categorical |
| Natural gradient as morphism | Perrone info geometry + optimization | Consolidate's update step as a gradient flow on the statistical manifold | natural gradient categorical; gradient descent enriched Markov |
Authors and papers
| Author | Paper | What it does |
|---|---|---|
| Tobias Fritz | Markov categories (2020) | Defines the ambient category for stochastic morphisms. Copy-naturality distinguishes deterministic from stochastic. Informativeness preorder captures sufficient statistics. |
| Markov Categories and Entropy (2024) | Defines entropy categorically as distance from determinism. Enriched Markov categories with divergences on hom-sets. Data processing inequality proved abstractly. | |
| Supports and idempotent splitting (2023) | Defines supports abstractly in Markov categories. Supports are functorial iff the category is causal. Static idempotents split iff they have supports. | |
| Fritz, Perrone, Rezagholi | Support as monad morphism (2021) | Proves supp : V ⇒ H is a monad morphism from valuations to Hoare hyperspace. Both constructed via double dualization against different semirings. |
| Baez, Fritz, Leinster | Entropy characterization (2011) | Shannon entropy is the unique functorial, convex-linear, continuous information loss assignment in FinProb, up to scale. |
| Sam Staton | Program Logics via Distributive Monoidal Categories (2025) | Derives Hoare logic from traced distributive copy-discard categories ("imperative categories"). Proves Stoch is a posetal imperative category. All Hoare rules follow as theorems. |
| Compositional Imprecise Probability (POPL 2025) | Graded monads over Markov categories for imprecise probability. The para construction makes the graded model itself a Markov category. | |
| Marco Gaboardi | Graded Hoare Logic (ESOP 2021) | Hoare triples parameterized by a preordered monoid grade. Categorical semantics via graded Freyd categories over coherent fibrations. Instantiated for cost, privacy, and probability. |
| Indexed graded monads (2026) | Graded monads parameterized fibrewise over a predicate fibration. Restricted pointwise order propagates pre/postconditions through composition. | |
| Shin-ya Katsumata | Divergences on Monads (MSCS 2023) | Divergences on a monad = enrichments of its Kleisli category. Connects metric structure on morphism spaces to relational Hoare logic. Instantiated for differential privacy and cost. |
| Bart Jacobs | Weakest preconditions in fibrations (2014) | Derives wp-semantics from order-enriched Kleisli categories via poset fibrations. Instantiated for the distribution monad — whose Kleisli category is FinStoch. |
| Structured Probabilistic Reasoning (2025 draft) | Book-length treatment of distributions, predicates, channels, conditioning via effectus theory. Cites Fritz extensively but uses his own formalism. FPred fibration for fuzzy predicates. | |
| Tom Leinster | Entropy and Diversity (2021) | Hill diversity numbers are the unique axiomatic diversity measures. Diversity is a special case of magnitude — the categorical generalization of cardinality for enriched categories. |
| Paolo Perrone | Categorical Information Geometry (2023) | Information geometry inside enriched Markov categories. Divergences in hom-spaces recover Shannon/Renyi entropy, DPI, and the Gini-Simpson index. |
| David Spivak | Operad of wiring diagrams (2013) | Typed ports and supplier assignment for composing boxes in wiring diagrams. Gives the syntax layer — which boxes connect to which. |
| Kidney & Wu | Algebras for Weighted Search (ICFP 2021) | Free semimodule monad parameterized by arbitrary semiring S. S = ℕ gives multiset monad (counting). S = [0,1] gives probability. Unifies search and probability via semiring choice. |
| Chen & Vigneaux | Categorical Magnitude and Entropy (2023) | Unifies Shannon entropy and log(magnitude) for finite categories with probability. Recovers magnitude under uniform distribution. Invariant of individual categories, not a functor on morphisms. |
| Luca Reggio | Semiring-valued measures (2020) | Codensity monad of finite S-semimodules gives S-valued measures on Stone spaces. Change-of-semiring framework for codensity monads. Requires finite semirings. |
| Kenta Cho | Introduction to Effectus Theory (2015) | With Jacobs. Predicates as effect-algebra-valued maps (X → 1+1), not subobjects. States/effects duality with Born rule. Parallel formalism to Markov categories. |
| Dario Stein | Probabilistic Programming with Exact Conditions (2023) | With Staton. Internal language of CD categories gives precise correspondence between Markov categories and a class of programming languages. Exact conditioning as categorical structure. |
| Eigil Rischel | Infinite products and zero-one laws (2020) | With Fritz. Kolmogorov and Hewitt-Savage zero-one laws proved in categorical probability. Exchangeability and independence axiomatized. |
| Tomáš Gonda | Markov Categories and Entropy (2024) | With Fritz, Perrone, Rischel. Categorical entropy recovers Shannon, Renyi, and the Gini-Simpson index used in ecology — direct bridge to Leinster's diversity. |
| Arthur Parzygnat | Quantum Markov categories (2020) | Bayesian inversion as dagger structure on morphisms. Three levels of reversibility: inverses, disintegrations, Bayesian inverses. No-broadcasting theorem. |
| Elena Di Lavore | Partial Markov Categories (2025) | With Roman, Sobocinski. Blends Fritz's Markov categories with restriction categories. Observations, Bayes' theorem, Pearl's and Jeffrey's updates in categorical terms. |
| Prakash Panangaden | Labelled Markov Processes (2009) | Continuous-state probabilistic transition systems as coalgebras. Bisimulation metrics = behavioral distance between processes. Logical characterization of bisimulation. |
| Jules Hedges | Compositional Game Theory (2018) | With Ghani, Kupke, Forsberg. Nash equilibrium as a compositional predicate on strategy profiles — checked locally on subgames. Open games via string diagrams. |
| Mixed Strategies (2020) | With Ghani, Kupke, Lambert. Relational Kleisli lifting of the probability monad lifts equilibrium predicates from pure to probabilistic games. | |
| Matteo Capucci | Towards Foundations of Categorical Cybernetics (2021) | With Gavranović, Hedges, Rischel. Selection relations on parametrised optics. "What is a goal but a predicate on a system?" Goals unify optimization, homeostasis, learning, equilibria. |
| Toby Smithe | Bayesian Lenses. Statistical Games (2021) | Bayesian inversions compose as lenses in a Markov category. Statistical games = optics + free-energy objective. Explicit bridge between Fritz and the cybernetics community. |
| Ho, Wu, Raad | Bayesian Separation Logic (POPL 2026) | Hoare logic for Bayesian probabilistic programming. Model is s-finite kernels. Internal Bayes' theorem via disintegration. Frame rule = probabilistic independence. |
Updated 2026-03-21. Previous vocabulary: Type Forcing (Spivak), Ambient Category (Fritz).