Modularity and specification complexity (why composition helps)¶

This note is about description and verification complexity, not numerical runtime.

Description complexity: how large (or cognitively costly) a model specification is to write, read, and communicate.
Verification complexity: how hard it is to check well-formedness (types, interfaces, measurability/shift rules), and to validate local semantic properties.

The claim is that modular stage specifications (with explicit interfaces) can avoid a “curse of specification complexity”: the cost of describing a large model scales roughly like “sum of parts + interface glue”, rather than like a monolith on the full product state.

This does not say that solving a high-dimensional model is easy in general; it says that the model description can remain structured and local.

This note is easiest to read alongside the “object-first” view: write a well-typed perch wiring diagram before choosing any analytic/operator semantics. See: Object-first model specification.

A clean formal template: specs compose by gluing interfaces¶

Let Spec be a category of specifications where:

objects are well-typed model specs (e.g. stages, periods, nests) with explicit interfaces, and
morphisms are structure-preserving maps (e.g. renamings, inclusions, interface embeddings).

Composition is gluing along a shared interface. If \(S_1\) and \(S_2\) share a boundary/interface \(I\), the composite is a pushout/colimit:

\[ S_1 \xleftarrow{\;\iota_1\;} I \xrightarrow{\;\iota_2\;} S_2 \qquad\leadsto\qquad S_1 \amalg_I S_2. \]

In Bellman calculus terms:

A stage is a module with an arrival interface and a continuation interface (perches as information interfaces).
A connector/twister is the glue: it identifies the continuation fields of one module with the arrival fields of the next (possibly after renaming).

“Complexity = sum of parts + glue”¶

Choose any reasonable description-length functional \(L(\cdot)\) on specs, for example:

number of declared symbols/fields and their types,
total AST size of equation blocks (transitions, reward, constraints, mover sub-equations),
size/number of interface mappings (connector/twister renames).

Then the categorical gluing story naturally supports bounds of the form

\[ L(S_1 \amalg_I S_2)\ \lesssim\ L(S_1) + L(S_2) + L(I), \]

where \(L(I)\) is an interface coupling term (e.g. how many fields must be matched/renamed).

Another formal lens: succinctness of diagrams vs expanded operators¶

There is a second, complementary way to formalize “less complex” that does not rely on any particular logic:

Treat the modular model as a string diagram / DAG whose nodes are local mechanisms (stage morphisms, kernels, reward/constraint components) and whose wires are typed interfaces.
Treat a “single global operator written out explicitly” as the inlined expansion of that DAG into one monolithic expression/table.

Then “modular specification is less complex” can be stated as a succinctness claim: DAG/circuit-like representations can be exponentially more compact than their fully expanded equivalents. This is the general mathematical form of “don’t inline semantics”.

This lens aligns with factored MDPs / graphical models as a discrete special case: tables over full product state explode, while local factors remain small when coupling (width) is bounded.

Why this is the right “curse” to talk about¶

For large economic models, the numerical curse is dimensionality of approximation. The specification curse is different: monolithic descriptions force you to reason about the full joint object at once (symbols, transitions, constraints, timing), and to copy/paste changes for variants.

Bellman calculus targets the second curse: how hard it is to author and re-author the model.

Institutions: compositional meaning + modular verification¶

An institution (Goguen–Burstall) is an abstract framework connecting:

signatures (syntax),
sentences (axioms),
models (semantics),
satisfaction (\(\models\)),

in a logic-independent way.

Two key takeaways (from the institutions / institution-independent model theory literature):

Models of a composite spec are compatible families of models of the pieces (colimits in specs correspond to limits in models, up to equivalence). This formalizes “meaning is compositional.”
Under additional logical properties (e.g. interpolation), proof/verification obligations can be decomposed into:
local obligations for each module, plus
compatibility obligations on the shared interface.

This is the most direct “formal tone” justification for statements like:

\[ V(S_1 \amalg_I S_2)\ \approx\ V(S_1) + V(S_2) + V(I), \]

where \(V(\cdot)\) denotes verification effort.

Decorated/structured cospans: open systems with explicit boundaries¶

Another clean categorical formulation is to treat modules as open systems:

An “open stage” has a left boundary (arrival interface) and a right boundary (continuation interface).
The interior is decorated with structure (kernels, reward, constraints, mover recipes).

Composition is again by pushout along the shared boundary, and the universal property of the pushout explains the “sum of parts + interface” accounting: to define something out of the composite is equivalent to defining it out of each part in a compatible way on the boundary.

This viewpoint matches the BE-DDSL slogan: composition is interface compatibility.

Continuous state, nonstationary, staged models (what can be claimed carefully)¶

The categorical/specificational results above do not depend on finiteness or stationarity:

Interfaces and colimit composition make sense for continuous-state objects and time-varying (nonstationary) wiring.
Markov kernels can be treated abstractly as morphisms (e.g. in a Markov category / Kleisli category), so “compose kernels” remains well-defined.

What you should not overclaim:

These results do not by themselves imply a universal numerical speedup for solving continuous-state problems.
They justify that model specification and many semantic checks can be modular: local definitions + interface glue.

Relation to factored MDPs (discrete special case)¶

Factored MDPs provide a familiar discrete special case where the “monolithic vs modular” description-size contrast is explicit:

monolithic transition tables scale like a joint object on \(S=\prod_i S_i\),
factored (graphical) representations scale like “sum of local mechanisms + graph glue.”

Bellman calculus can be described as a typed, stage-first way to present and compose such factorisations (without restricting attention to finite stationary MDPs).

References (starting points)¶

Goguen, J.A. and Burstall, R.M. (1992). Institutions: Abstract Model Theory for Specification and Programming. Journal of the ACM 39(1), 95–146.
Diaconescu, R. (2008). Institution-Independent Model Theory. Birkhäuser.
Fong, B. (2015). Decorated Cospans. Theory and Applications of Categories 30(33), 1096–1120.
Baez, J.C. and Courser, K. (2020). Structured Cospans. Theory and Applications of Categories 35(48), 1771–1822.
Vagner, D., Spivak, D.I., and Lerman, E. (2015). Algebras of Open Dynamical Systems on the Operad of Wiring Diagrams. Theory and Applications of Categories 30(51), 1793–1822.
Boutilier, C., Dearden, R., and Goldszmidt, M. (2000). Stochastic dynamic programming with factored representations. Artificial Intelligence 121(1–2), 49–107.
Fritz, T. (2020). A Synthetic Approach to Markov Kernels, Conditional Independence, and Theorems on Sufficient Statistics. Advances in Mathematics 370:107239.