0.2 From syntax to formal problem definition (dolo-plus SYM → mathematical problem)¶

This note explains how to read a dolo-plus stage YAML as a precise dynamic optimization problem, using:

packages/dolo/examples/models/doloplus/consumption_savings_iid_egm_doloplus/stage.yaml (including the YAML comments), and
AI/working/AAS/23012026/consumption_savings_iid_egm_doloplus-stage-notes.md.

The goal is to make explicit which mathematical objects are declared, which are implicitly defined by equalities, and which are method/representation choices (EGM).

1. What the SYM file declares¶

In stage.yaml, the symbols: block declares:

Spaces (domains): Xb, Xw, Xa, Y.
Perch groups (ADC dialect):
prestate: \(b \in X_b\) (arrival perch)
exogenous: \(y \in Y\) with \(y \sim \mathcal{N}(\mu_y,\sigma_y)\) (shock edge)
states: \(w \in X_w\) (decision perch)
poststates: \(a \in X_a\) (continuation perch)
controls: \(c \in \mathbb{R}_+\) (chosen at decision perch, even if represented elsewhere)
Perch value objects:
V: @in R (value)
dV: @in R+ (marginal/shadow value object used by EGM)

Interpretation: the YAML is not directly a functional program; it is a symbolic specification that must be mapped to formal objects (functions/operators) by SYM → CORE rules.

2. Timing / perches / information¶

This example is built around the timing idea “shock realized between arrival and decision”:

Arrival perch: the state is \(b\) (assets brought in).
Between perches: an income shock \(y\) is realized and then observed.
Decision perch: the decision state is \(w\), and the agent chooses \(c\).
Continuation perch: the post-decision state is \(a\), which becomes next period’s arrival asset state.

So the filtration / information sets satisfy (informally): at decision time you know \((b,y)\), hence you know \(w\); at arrival time you do not.

This is exactly why the dcsn_to_arvl_opr contains the expectation operator (see Section 5 below).

3. Equalities as implicit maps (the key SYM rule)¶

The YAML comments stress an important convention:

“Equality blocks as implicit function definitions”: transition equations are not “new functions” written explicitly, but in SYM they implicitly define maps (AAS note).

Concretely, the transition equalities define maps between perch objects:

3.1 Arrival → Decision transition (`arvl_to_dcsn_transition`)¶

w = exp(y) + b*r

Mathematically, this implicitly defines the map:

\[ \mathrm{g}_{\prec\sim}: X_b \times Y \to X_w,\qquad w = \mathrm{g}_{\prec\sim}(b,y) := e^{y} + r\,b. \]

3.2 Decision → Continuation transition (`dcsn_to_cntn_transition`)¶

a = w - c

This implicitly defines:

\[ \mathrm{g}_{\sim\succ}: X_w \times \mathbb{R}_+ \to X_a,\qquad a = \mathrm{g}_{\sim\succ}(w,c) := w-c. \]

The YAML comments explicitly connect this to T core reading (formerly “DDSL-CORE”):

"define \(\mathrm{g}_{\sim\succ}\) as \(w,c \mapsto a\), via the following"
AAS naming rule-of-thumb: \(\mathrm{g}_{\sim\succ}\) is often the object we refer to as a_fn.

3.3 Continuation → Decision inverse map (`cntn_to_dcsn_transition`)¶

w = a + c

There is a comment tension worth resolving explicitly:

The YAML comment says this “is not defining a transition equation so it needs to be defined as new function…”.
Under the SYM convention above, it is still an equality and therefore does implicitly define a map:

\[ \mathrm{g}_{\sim\succ}^{-1}: X_a \times \mathbb{R}_+ \to X_w,\qquad w = \mathrm{g}_{\sim\succ}^{-1}(a,c) := a+c. \]

The important subtlety is not whether it defines a map, but what role it plays:

\(\mathrm{g}_{\sim\succ}\) is the forward (simulation) direction from \((w,c)\) to \(a\).
\(\mathrm{g}_{\sim\succ}^{-1}\) is an inverse-style wiring used by EGM to recover decision-grid objects from continuation-grid objects.

This aligns with the working note’s open point: keep the semantic perch straight (the LHS is a decision-perch state \(w\), even if some objects are represented on the continuation grid).

4. The formal dynamic problem (consumption–savings with IID income)¶

Given parameters \((\beta,\gamma,r)\) and IID shock \(y \sim \mathcal{N}(\mu_y,\sigma_y)\), the economic problem is:

State (arrival): \(b \in X_b\)
Shock (arrives before choice): \(y \in Y\)
Decision state: \(w = \mathrm{g}_{\prec\sim}(b,y)\)
Control: choose \(c \in \Gamma(w)\) (typically \(\Gamma(w)=\{c\in\mathbb{R}_+ : 0 \le c \le w\}\))
Poststate: \(a = \mathrm{g}_{\sim\succ}(w,c)\)
Inter-stage link (next arrival): \(b' = a\)

Utility is CRRA:

\[ u(c) = \frac{c^{1-\gamma}}{1-\gamma}. \]

4.1 Perch-value Bellman factorization (expectation location)¶

The stage is written with two value objects:

\(\mathrm{v}_{\sim}(w)\): post-shock decision value (max happens here)
\(\mathrm{v}_{\prec}(b)\): pre-shock arrival value (expectation happens here)

Formally:

\[ \mathrm{v}_{\sim}(w) = \max_{c \in \Gamma(w)} \left\{ u(c) + \beta\,\mathrm{v}_{\succ}(a) \right\} \quad\text{with}\quad a = \mathrm{g}_{\sim\succ}(w,c), \]

\[ \mathrm{v}_{\prec}(b) = \mathbb{E}_{y}\left[\,\mathrm{v}_{\sim}(\mathrm{g}_{\prec\sim}(b,y))\,\right]. \]

Here \(\mathrm{v}_{\succ}\) is the continuation value function (the fixed-point object when stages are linked across time).

5. How the mover blocks correspond to operators (EGM-style)¶

The YAML uses “operators/movers” (*_opr) to encode backward steps. For this example:

cntn_to_dcsn_opr is the decision/optimization operator \(\mathbb{B}\) (no expectation).
dcsn_to_arvl_opr is the expectation-location operator \(\mathbb{I}\) (integrates over the shock edge).

5.1 `cntn_to_dcsn_opr` (optimization + EGM representation)¶

The Bellman sub-equation is:

V = max_{c}((c^(1-γ))/(1-γ) + β*V[>])

Read as defining the function \(\mathrm{v}_{\sim}(\cdot)\) from the continuation object \(\mathrm{v}_{\succ}(\cdot)\).

The EGM-specific piece is the inverse Euler step:

c[>] = (β*dV[>])^(-1/γ)

The crucial reading (from the foundations + AAS note) is:

c[>] is a representation choice: the policy is parameterized/evaluated on the continuation grid.
semantically, \(c\) is still chosen at the decision perch.

5.2 `dcsn_to_arvl_opr` (expectation location)¶

The Bellman expectation block is:

V[<] = E_{y}(V)

This encodes the “shock is observed before choice” structure: expectation is outside the max.

The marginal object is carried similarly:

dV[<] = r * E_{y}(dV)

6. The substitution subtlety (why the YAML comments matter)¶

The stage.yaml comment expands:

\(V[>]\) as "syntax sugar" for something like \(\mathrm{v}_{\succ}(x_{\succ})\),
then identifies \(x_{\succ}\) with \(a\),
then replaces \(a\) by \(\mathrm{g}_{\sim\succ}(w,c)\).

The working note flags the key issue:

You must keep separate:
(i) definition of a map \(a = \mathrm{g}_{\sim\succ}(w,c)\) (an implicit map definition), and
(ii) evaluation at a particular policy \(c = c^\*(w)\).

The safe formal reading is:

For any candidate pair \((w,c)\), define \(a := \mathrm{g}_{\sim\succ}(w,c)\).
Evaluate \(\mathrm{v}_{\succ}(a)\).
Only after optimization do you substitute \(c=c^\*(w)\) and hence \(a=a^\*(w)=\mathrm{g}_{\sim\succ}(w,c^\*(w))\).

This is also where the project naming rule-of-thumb fits:

Forward transitions are often written as equalities (no _fn suffix in surface notes).
Backward movers produce function objects (it’s natural to talk about V_dcsn_fn, c_cntn_fn, etc.).