Index back

\(\mathbf{T}\)-calculus (Bellman calculus) is a declarative language and functional programming system for expressing modular Bellman problems. It provides a well-defined computational representation of general Bellman operators and their composition into economic models — without imposing any solver-specific details or modelling choices.

Expressive — define a concrete mathematical Bellman operator connecting the math to model specification and computational implementation
Modular — compose stages, periods and nests from reusable building blocks
Implementation-agnostic — specify what the economics says, not how to compute it

Syntax, semantics, and scope¶

The syntax and semantics of \(\mathbf{T}\)-calculus maintain two explicit maps — from the declarative syntax onto the abstract mathematical problem (the economic model a researcher describes), and from the calibrated model onto executable computational objects.

\(\mathbf{T}\)-calculus does not introduce new economic theory or new numerical methods. The Bellman operator — the canonical object at the heart of stochastic behavioural modelling — already exists in the literature; what has been missing is a formal, declarative framework for representing it. \(\mathbf{T}\)-calculus fills that gap: the syntax specifies what mathematical operations a stage performs (expectations, maximizations, transitions) while remaining agnostic about how they are computed. Solver algorithms, discretisation schemes, and programming-language choices all live outside the model declaration.

Using \(\mathbf{T}\)-calculus requires commitment only to the objects that define a Bellman operator — state variables at each perch, shocks and their timing, transitions between perches, and rewards. It does not impose a particular solution method (VFI, PFI, EGM, ...), a particular value representation (V-function vs Q-function), or a particular computational arrangement. These are methodization choices, not model specification; numerics live in a separate layer.

Economic modelling already involves three distinct layers: the mathematical model (the Bellman problem a researcher formulates on paper), the syntax (a declarative description of what the computational solution should do), and the code (the numerical implementation that actually runs). These layers exist in every project — but the mappings between them are typically implicit, ad hoc, and locked inside a particular solver. \(\mathbf{T}\)-calculus makes these mappings explicit and invertible:

\[ \text{Math Model} \;\overset{\Upsilon}{\longleftrightarrow}\; \text{Syntax} \;\overset{\rho}{\longleftrightarrow}\; \text{Executable Code} \]

scope of T-calculus

Υ (Upsilon): Syntax ↔ mathematical meaning — syntax maps to a precise mathematical object, and every well-defined mathematical object in the model has a syntactic counterpart
ρ (rho): Calibrated syntax ↔ numerical implementation — given methodization and calibration, each syntactic object maps to a computational object, and vice versa

Because both maps are invertible, a researcher can work at any layer and recover the other two: read the YAML and know the exact mathematical problem; inspect the code and trace back to the equation it implements; start from the mathematics and generate the declaration.

\(\mathbf{T}\)-calculus is founded on a rigorous framework integrating Bellman operator theory, (generalized) Markov Decision Processes, and declarative programming, making the language expressive for the complete class of Bellman problems while mapping cleanly to computation. The core unit is the stage — a modular Bellman operator with an ADC (Arrival–Decision–Continuation) information structure, where perches are nodes corresponding to information sets. The current implementation vehicle is a backwards-compatible extension of Dolo called dolo-plus.

Stages¶

A stage is the core unit of \(\mathbf{T}\)-calculus and represents a general Bellman operator. Its internal structure is a directed graph of three perches — information sets characterized by nested filtrations:

\[ \mathcal{F}_{\text{arvl}} \subseteq \mathcal{F}_{\text{dcsn}} \subseteq \mathcal{F}_{\text{cntn}}, \qquad \mathcal{F}_m := \sigma(x_m) \]

where \(x_m\) is the sufficient information state at perch \(m\). Each perch arises naturally within a Bellman problem:

Arrival (\(\mathcal{F}\_{\text{arvl}}\)) — information before any shocks are realized or decisions made
Decision (\(\mathcal{F}\_{\text{dcsn}}\)) — information after shocks are observed, on which the agent conditions its policy
Continuation (\(\mathcal{F}\_{\text{cntn}}\)) — full information after the agent's action and all within-stage uncertainty are resolved

Key variables appear with perch tags (e.g. z[_dcsn] ) and these tags are measurability claims: \(z[\_\text{dcsn}]\) means that \(z\) is a function of the information (or state variable) known at decision time. Importantly, concepts of future and past variables are generalized to information sets, allowing for modularity.

\[ \boxed{\begin{array}{c}\textbf{Arrival}\\x_a,\;\mathcal{F}_a\end{array}} \;\xrightarrow{\;\varepsilon\;\text{realized}\;}\; \boxed{\begin{array}{c}\textbf{Decision}\\x_v,\;\mathcal{F}_v\end{array}} \;\xrightarrow{\;\pi\;\text{chosen}\;}\; \boxed{\begin{array}{c}\textbf{Continuation}\\x_e,\;\mathcal{F}_e\end{array}} \]

This three-perch structure carries two dual families of operators that define how variables relate to each other between the perches.

Forward transitions (kernels). Transition kernels are measurable maps defining state evolution between the perches. These induce forward movers — push-forwards on distributions:

\[ \begin{align} g_{ad} &: X_{\text{arvl}} \times W \to X_{\text{dcsn}} & &\text{(shock realization)} \\ g_{dc} &: X_{\text{dcsn}} \times C \to X_{\text{cntn}} & &\text{(action application)} \end{align} \]

\[ \mathcal{F}_{\text{arvl}}\,\mu_a = (g_{ad})_*(\mu_a \otimes \mu_w), \qquad \mathcal{F}_{\text{dcsn}}\,\mu_v = (g_{dc}(\cdot, \pi^*(\cdot)))_*\,\mu_v \]

Backward operators (Bellman movers). The backward movers transform value functions in the reverse direction:

\[ \begin{align} (\mathcal{B}_{\text{dcsn}}\,V_e)(x_v) &= \max_{a \in \Gamma(x_v)}\left\{u(a) + \beta\,V_e(g_{dc}(x_v, a))\right\} \\ (\mathcal{B}_{\text{arvl}}\,V_v)(x_a) &= \mathbb{E}_w\left[V_v(g_{ad}(x_a, w))\right] \end{align} \]

The full factored Bellman operator for a stage is:

\[ \mathbf{T} = \mathcal{B}_{\text{arvl}} \circ \mathcal{B}_{\text{dcsn}} : \mathcal{V}(X_{\text{cntn}}) \to \mathcal{V}(X_{\text{arvl}}) \]

Forward–backward duality. The forward and backward operators are conjugate duals: \(\langle \mathcal{F}\,\mu,\; V \rangle = \langle \mu,\; \mathcal{B}\,V \rangle\). \(\mathbf{T}\)-calculus syntax specifies the backward (problem) direction; the forward (simulation) direction is derived via conjugation.

\[ \underset{\xrightarrow{\quad\text{Forward (push-forward)}\quad}}{\text{arvl}\;\xrightarrow{\;\varepsilon\;}\;\text{dcsn}\;\xrightarrow{\;\pi\;}\;\text{cntn}} \qquad \underset{\xleftarrow{\quad\text{Backward (Bellman)}\quad}}{\text{cntn}\;\xleftarrow{\;\mathcal{B}_v\;}\;\text{dcsn}\;\xleftarrow{\;\mathcal{B}_a\;}\;\text{arvl}} \]

Between stages: a graph (category) of Bellman operators¶

Random variables as nodes, stages as edges. Variable names like a, w, k are not lambda-bound placeholders — they are fields (elements of \(L^2(\Omega)\)). A stage \(S\) is a directed edge: \(a \xrightarrow{S} b\) means \(S : \mathcal{V}(X_b) \to \mathcal{V}(X_a)\).

A \(\mathbf{T}\)-calculus model is a directed graph \(G = (V, E)\):

Graph element	\(\mathbf{T}\)-calculus meaning
Node \(v \in V\)	Random variable (field) \(v : \Omega \to X_v\)
Edge \((a, b) \in E\)	Stage \(S : \mathcal{V}(X_b) \to \mathcal{V}(X_a)\)
Path \(a \to b \to c\)	Composed operator \(S_1 \circ S_2\)

Composition via shared fields. Two stages compose iff they share a random variable at their interface — the same mathematical object, not merely the same string label:

\[ \langle S_1, S_2 \rangle \text{ is valid} \iff X_{\mathrm{cntn}}(S_1) \cong X_{\mathrm{arvl}}(S_2) \]

When names differ but fields are isomorphic, an explicit connector (intra-period) or twister (inter-period) provides the identification \(\tau : X_{\mathrm{cntn}}(S_1) \xrightarrow{\sim} X_{\mathrm{arvl}}(S_2)\).

Periods as subgraphs. A period \(P = (V_P, E_P, a_{\text{entry}}, b_{\text{exit}})\) is a connected subgraph. A nest (lifecycle) is a sequence of period subgraphs connected by twisters:

\[ M = \langle P_0,\; \tau_0,\; P_1,\; \tau_1,\; \ldots,\; P_T \rangle \]

\[ \underbrace{S_1 \to S_2}_{P_0} \;\xrightarrow{\;\tau_0\;} \underbrace{S_3 \to S_4}_{P_1} \;\xrightarrow{\;\tau_1\;} \underbrace{S_5 \to S_6}_{P_2} \]

The category view. The graph view lifts to a category: stages as objects, connectors as morphisms, wiring as composition (identities correspond to no-op connectors). This is the right abstraction when models are not linear time-indexed scripts — branching, reuse, and merging are all natural.

The MDP guarantee. If the composition graph is (1) directed acyclic or single-cycle, (2) connected, and (3) well-typed, then it defines a valid MDP and backward induction computes the value function.

GitHub · Dolo (upstream) · Changelog