1.1 Symbols and declarations¶

This section covers what you declare in a dolo-plus stage: symbol groups, decorator-based typing, and variable semantics.

1.1.1 SYM scope: keep YAML clean¶

We are narrowing the responsibility of dolo-plus YAML:

dolo-plus YAML is SYM: it should remain close to vanilla dolo YAML and be optimized for compatibility and translation.
T core owns functional declarations: we are not using T core-style function signature/body declarations inside dolo-plus YAML (e.g. no @mapsto, no @via, [_x] function bodies). Those live in T core artifacts instead.

This note (and the spec_0.1/* docs) therefore treat dolo-plus YAML as a compatibility layer that may carry additional metadata, but keeps legacy symbol names and Dolo's solve pipeline intact.

1.1.2 Decorator-based parameter registration¶

dolo-plus/symbols #dolo-plus/yaml¶

We want to register parameter meaning/typing information (e.g. \(\beta \in (0,1)\)) while preserving the ability to compile/solve with vanilla Dolo. Symbol declarations act as a typing function: given a bare symbol token, we should be able to determine which symbol group it belongs to (state, control, parameter, setting, shock, value, …).

Thus, symbols: is a named collection with (at least) the following groups:

states (decision-perch states)
prestate (arrival-perch states)
poststates (continuation-perch states)
controls
exogenous
values
parameters
settings
(optionally) spaces

Each group binds a bare name to a decorator-based type/meaning declaration, e.g. β: @in (0,1).

Perch-declared variables may be referenced with explicit perch tags for clarity: e.g., if m is declared in prestate, it is an arrival-perch object and may be written as m[<] (decision-perch objects are unmarked by default).

Rules (decorators)

The same decorator mechanism applies to all declared symbols (states, controls, shocks, settings, etc.). Parameters are just the first place we can safely add numeric validation via calibration.
Decorators must never become part of symbol names.

Caveats (implicit functions and sugar)

Functions are usually implicit in Dolo+ SYM: transition and mover equation blocks implicitly define the corresponding maps/operators; you typically declare variables (states, controls, shocks, values), not separate function signatures.
Intermediate names in equation blocks: equation payloads may introduce helper temporaries (e.g. u = ...). Treat these as block-local unless the name is also declared in symbols: (stage-global).
Arguments vs perch tags (sugar): perch tags (x[<], x, x[>]) are indices (measurability), not function application. Use f[x] for function evaluation and max_c{…} / argmax_c{…} / E_y(…) for operator application. See Symbol Conventions → Argument delimiters (and the “function arguments / intermediate evaluation” open question there).

Namespace and value-object conventions

All states and controls are part of a period namespace, i.e. cannot be overloaded.
x[<] remains a stage-level placeholder for “arrival state”.
Names can be connected by an interface.
Values are a local namespace / arguments to the stage.
Stage-level placeholder / Bellman argument is V[<] by default.
Value symbols can be customized.
- We can also declare [V_adj[>], V_nadj[>]], in which case this is interpreted as V[>] = [V_adj[>], V_nadj[>]].

Recommended Dolo+ SYM pattern:

symbols:
  states:
    w: @in R+
  controls:
    c: @in R+
  parameters:
    β: @in (0,1)
    γ: @in R+
    r: @in R+

calibration:
  β: 0.96
  γ: 4.0
  r: 0.03

Interpretation caveat

@in declarations specify domains, but the T-calculus foundations interpret these as fields / random variables on an underlying information space. Thus the domains above correspond to the realized support.
See above on sugaring: SYM treats symbols as functions only in the appropriate evaluation context.

This keeps:

the canonical bare parameter names (β, γ, r) available for calibration/compilation, and
decorator applications (e.g. @in (0,1), where @in is the decorator token) attached to the same symbols object (dolo-plus tooling can read/parse them; horse translation can recover a legacy "names-only" view).

1.1.3 Variables: perch objects vs perch value objects¶

It is useful to separate two kinds of objects that appear in the dolo-plus surface syntax:

Perch objects: plain tokens like b, w, a, y, c. Their perch is determined by the stage structure and/or declaration (e.g. prestate: [b], states: [w], poststates: [a], exogenous: [y], controls: [c]). In equations they can appear without indices if they are the native perch, but may be perch-tagged explicitly (e.g. b[<]) for clarity or if a shifted variable is deined.
- If a shifted variable is defined, its defintiion must be measurable with a non-native perch and that measurable function must be defined by an equation somewhere.
Perch value objects: perch-indexed objects like V[<], V, V[>] and dV[<], dV, dV[>]. Here the object's identity is the pair (token, perch): e.g. V[<] and V are different perch value objects within the same stage. These are to be referred to with the tag since they are defined at the decisin perch as the native:
Decision perch is unmarked: in SYM, the decision perch is the default. We do not require any special tag for decision-perch value objects.
Aliases accepted (v0.1): the parser may also accept V[_arvl] / V[_dcsn] / V[_cntn] for compatibility, but V[<] / V / V[>] is the preferred surface spelling going forward.

This distinction matters because mover equations explicitly relate different value objects across perches (often via operators like E_y(·)), while perch objects like b,w,a are stage-local labels that are typically bound to underlying state slots via the slot map (and may only be shifted when measurability permits).

Examples from this file:

transition equation uses perch objects: w = exp(y) + b*r
mover equation relates perch value objects across perches: V[<] = E_y(V)

For the corresponding mathematical notation for stage movers and kernels (including \(\mathbb{B}\), \(\mathbb{I}\), \(\mathrm{g}_{\prec\sim}\), \(\mathrm{g}_{\sim\succ}\)), see docs/dolo-plus-spec/reference/symbols-conventions.md.

1.1.4 Declaring variables and their canonical perches (v0.1 convention)¶

In v0.1 we use these symbol groups:

Group	Canonical perch (SYM)	Description
`prestate`	`[<]`	Arrival perch state
`states`	(unmarked)	Decision perch state
`poststates`	`[>]`	Continuation perch state
`controls`	(unmarked)	Decision variable(s)
`values`, `shadow_value`	`[<]` / (unmarked) / `[>]`	Perch value objects
`exogenous`	(edge)	Shocks; timing via `information_timing`

If a variable is written without an index, it is assumed to be at its canonical perch (but we often write indices explicitly to keep perch meaning visible).

Implementation note

Internally, the compiler may normalize perch tags to an abstract “slot” representation (e.g. arrival/decision/continuation slots). The SYM surface syntax should not require modellers to use numeric slot indices.

Note on expectations

The Dolo+ direction is to deprecate an expectations: symbol group as a modeller-facing primitive and instead use an explicit expectation operator E_y(·).
For v0.1 translation to the unchanged Dolo horse, the translator may still need to introduce Dolo's expectations token(s) and expectation block in the output Dolo YAML.
In Dolo+ stage files, we also avoid an explicit expectation: equation block; expectation is expressed by placing E_y(·) inside the appropriate mover sub-equation (the "expectation location" principle).

1.1.5 Shifting variables across perches (within-stage shift operator)¶

In dolo-plus, bracket indexing like c[>] is interpreted as a within-stage perch shift (not a time subscript).

Indexing restriction (v0.1)

In stage mode, explicit perch tagging is permitted only for tokens listed in dolo_plus.validation.allow_indexed_tokens AND any further implicit functions defined via equations (but measurability conditions must be met).
A recommended minimal set is the control, state variables and values x, V, dV, and (in EGM-style representations) c. (Examples also allow b,w,a,y so indices can be written explicitly for clarity if they are away from their native perch.)

Parser defensiveness (v0.1)

accept perch-tag aliases [_arvl], [_dcsn], [_cntn], as well as glyph tags [<], [>], and normalize internally
accept arrow tags like [<-], [-], [->] for compatibility (normalize internally)
accept numeric spellings like [1] and [+1] as the same slot, and accept [-1] (normalize internally; discouraged in SYM docs)
do not mix t-style indices (e.g. [t], [t+1]) with perch-tag / numeric slot indices in the same file unless explicitly in "plain Dolo mode"

Shift rule

You may shift a declared variable across perches only if the shifted object is measurable w.r.t. the target perch's state/information. Operationally, this is supported only when an equation block defines the shifted object as a measurable function of target-perch information.

Practical implication (shock between arrival and decision)

c[>] may be allowed: in EGM, the policy can be represented as a function of the continuation state x[>] (endogenous grid representation).
c[<] is not allowed usually: the control is chosen after observing y, so it is generally not measurable w.r.t. the pre-shock arrival information set.
Importantly, modeller-declared observed variables (e.g. prestate, states, poststates) can also be shifted across perches when measurability allows. This highlights that these declared variables are not the same thing as the underlying slot objects x[<], x, x[>], which represent the stage's underlying information sets. In fully observed models we often bind observed states to underlying slots (via the slot map), but in later iterations (e.g. POMDPs) these can diverge.
Legacy note: vanilla Dolo's "previous-period control" notation (e.g. controls[-1]) is treated as legacy/deprecated under ADC slot semantics and may be rejected by v0.1 validation depending on the declared shock edges.

Implementation hooks (v0.1)

dolo_plus.information_timing (shock edges), and
dolo_plus.validation.shift_rules (allowed/disallowed shifts).

1.1.6 Coproduct declarations in `poststates` (branching stages)¶

In a standard (non-branching) stage, poststates declares a flat list of continuation-perch state variables:

poststates:
  a: "@in R+"
  y: "@in Y_set"

This declares a single continuation state space \(\mathsf{X}_{\succ}\) whose elements are tuples \((a, y) \in \mathbb{R}_+ \times \mathcal{Y}\).

Named sub-blocks: declaring a coproduct¶

branching #co-product #interface¶

A branching stage (kind: "branching") declares poststates with named sub-blocks, each defining one summand of a coproduct:

poststates:
  own:
    a: "@in R+"
    H: "@in H_set"
    y: "@in Y_set"
  rent:
    w: "@in R+"
    y: "@in Y_set"

This declares the continuation state space as a coproduct (disjoint union) indexed by a discrete label set \(N_+ = \{\text{own}, \text{rent}\}\):

\[ \mathsf{X}_{\succ} \;=\; \coprod_{j \in N_+} \mathsf{X}_{\succ,j} \;=\; \underbrace{(\mathbb{R}_+ \times \mathcal{H} \times \mathcal{Y})}_{\mathsf{X}_{\succ,\text{own}}} \;\sqcup\; \underbrace{(\mathbb{R}_+ \times \mathcal{Y})}_{\mathsf{X}_{\succ,\text{rent}}} \]

An element of \(\mathsf{X}_{\succ}\) is a tagged pair \((j, x_j)\) where \(j \in N_+\) is the branch label and \(x_j \in \mathsf{X}_{\succ,j}\) is the branch-specific state.

Coproduct ≠ product

A product \(A \times B\) has elements \((a, b)\) — both components are always present.
A coproduct \(A \sqcup B\) has elements that are either from \(A\) or from \(B\), tagged by which summand they belong to.

The poststates sub-block declaration is a coproduct: at any given state, exactly one branch is active. The discrete label \(j\) selects which summand.

Special case: when all branches share the same continuous state space \(\mathsf{X}_c\), the coproduct \(\coprod_j \mathsf{X}_c \cong N_+ \times \mathsf{X}_c\) is isomorphic to a product of the discrete index and the common continuous space.

Declaration rules¶

Each sub-block name (e.g. own, rent) is a continuation perch label — it names one summand of the coproduct.
Sub-block names must be unique within poststates.
Variables within each sub-block follow the same @in / @def decorator rules as flat poststates declarations.
Variables in different sub-blocks may share names (e.g. both own and rent contain y). These are distinct variables — they live in different summands of the coproduct.
The presence of named sub-blocks in poststates implies kind: "branching". A stage must not mix flat declarations and sub-block declarations in poststates.

Interaction with movers and transitions¶

Each continuation perch label induces:

A branch-specific transition equation block: dcsn_to_cntn_transition.{label} (e.g. dcsn_to_cntn_transition.own; legacy: dcsn_to_cntn_own_transition). Uses the standard [>] tag for the branch's poststate variables.
A branch-specific forward mover (for simulation): dcsn_to_cntn_mover.{label} (legacy: dcsn_to_cntn_{label}_mover).

The backward mover cntn_to_dcsn_mover remains “equations-only”: it combines branch values directly in its Bellman equation (e.g. with max_d{…} or a weighted sum).

equations:
  dcsn_to_cntn_transition:
    own: |
      a[>] = a
      H[>] = H
      y[>] = y

    rent: |
      w[>] = (1+r)*a + H
      y[>] = y

  cntn_to_dcsn_mover:
    Bellman: |
      V = max_d{V_own[>], V_rent[>]}

Interaction with namespace composition¶

Each sub-block's variables participate in the period namespace independently. Composition between a continuation perch and a successor stage's arrival perch follows the standard namespace rule:

If field names match → implicit composition (no connector)
If field names differ → standard rename connector ({from, to, rename})

The coproduct structure is invisible to connectors — they just rename fields, as in any non-branching composition. See Spec 0.1l §3 for the full treatment.

Namespace ambiguity when parallel branches share arrival field names #ambiguity #branching

In the graph-theoretic view, arrival perches on parallel branches (e.g., owner_housing.arvl and renter_housing.arvl) represent distinct random variables — they are on separate paths in the DAG and can never connect to each other.

However, in the flat period namespace, if two parallel successor stages have the same arrival field names (e.g., both expect {a, y}), and the branching stage's continuation perch sub-blocks also output the same field names, the namespace alone cannot determine which continuation perch maps to which successor.

This ambiguity does not arise when the branch state spaces are heterogeneous (e.g., own has {a, H, y}, rent has {w, y}) — the field sets are distinguishable. It arises only when parallel branches share a common state space.

Open question: should we (a) require distinct arrival field names across parallel branches, or (b) allow shared names and require explicit connectors when the namespace is ambiguous? See Spec 0.1l §3.2 for discussion.

Value functions on a coproduct¶

Branch-specific value objects are declared in values:

values:
  V_own: "@in R"     # value function on `poststates.own`
  V_rent: "@in R"    # value function on `poststates.rent`

Mathematically, a value function on a coproduct decomposes into a family:

\[ \mathrm{v}_{\succ} \in \mathcal{V}(\mathsf{X}_{\succ}) \;\;\iff\;\; (\mathrm{v}_{\succ,j})_{j \in N_+} \in \prod_{j \in N_+} \mathcal{V}(\mathsf{X}_{\succ,j}) \]

Each V_{label} declared in values corresponds to one component \(\mathrm{v}_{\succ,j}\) of this family. The backward mover's aggregation expression (max_d{V_own[>], V_rent[>]}) combines them into the decision-perch value \(\mathrm{v}\).