Skip to content

dolo-plus spec_0.1 — open ambiguities (working notes)

This file records open ambiguities that matter for spec_0.1/* and should be resolved (or explicitly deferred) before we lock down the v0.1 version.

2. “Shift across perches” is doing two different jobs (semantic measurability vs representation trick)

What the current rule says

The shift rule says:

  • you may shift a variable across perches only if it is measurable w.r.t. the target perch information set.

What the motivating example is

The motivating example is:

  • allow c[+1] for EGM because the policy is represented on the continuation grid.

Why this is ambiguous

These are not the same thing:

  • “Measurable w.r.t. \( \mathcal{F}_{+1} \)” is a semantic statement about random variables / information sets.
  • “Represent policy on continuation grid” is a representation / methodization statement (how you store/parameterize the function numerically), not a semantic measurability claim.

EGM is full of these “representation shifts”: you compute today’s c but index/parameterize it by a (post-decision state). That’s not “c happens at +1”; it’s “c is parameterized on the +1 grid”.

Why this matters

If we keep measurability as the only rule for interpreting perch shifts, we’ll hit contradictions as soon as:

  • the mapping from \(x[0]\) to \(x[+1]\) is not invertible, or
  • the control isn’t recoverable from \(x[+1]\), or
  • we want to allow “EGM-style” objects that are fundamentally solver artifacts.

Minimal deconfliction (without rewriting everything)

Make an explicit distinction in the spec between:

  • Perch evaluation (semantic): “this object is defined / measurable at perch \(i\)”
  • Perch representation (numerical): “this object is represented on the grid associated with perch \(i\)”

Then define c[+1] to mean representation shift, not semantic shift, at least in v0.1.

Concretely:

  • Keep measurability as the gatekeeper for semantic shifts (if we need them later).
  • For EGM-style, define c[+1] as a request: “store/construct the policy using continuation coordinates.”

This aligns with the two-layer SYM/T core idea: the meaning map \( \Upsilon \) shouldn’t depend on EGM representation choices; that lives in \( \rho \) / methodization.

3. Parameter declaration shape in dolo-plus SYM (label-keyed vs name-keyed)

This ambiguity is about whether dolo-plus SYM parameter declarations should follow the Foundations label → declaration-string pattern, or a more Dolo-compatible name → decorators pattern.

Option A — label-keyed “full declaration string” (Foundations-style)

Example (key is the label; value includes the symbol name):

symbols:
  parameters:
    discount_rate: β @in (0,1)

Pros:

  • closest to Foundations: "discount factor": β @in (0,1) (label carried in the YAML key).
  • very readable for humans; labels are first-class.

Cons:

  • downstream code must always parse the value string to recover the bare symbol name (β) safely.
  • easy to accidentally let the full string leak into the “name” path unless normalization is strict.
  • harder to provide a legacy “names-only” view without extra parsing.

Option B — name-keyed decorator payload (dolo-plus-compatibility style)

Example (key is the bare symbol name; value is decorator-only payload):

symbols:
  parameters:
    β: @in (0,1)

Pros:

  • keeps the canonical symbol name (β) explicit and stable (good for calibration lookup and old Dolo compilation paths).
  • decorator payload is small; full declaration string can be reconstructed as β + " " + decorator.

Cons:

  • label like “discount_rate” is not carried by default (unless we add an explicit label mechanism).

Open question:

  • In dolo-plus v0.1, do we want symbols.parameters keyed by labels (Option A) or keyed by bare names (Option B)?

4. Whether symbols should be a new class (SymbolsDict)

Status: Unresolved (implementation exists, design needs confirmation)

Current implementation

SymbolsDict is a new class that extends dict and provides dual access:

# Legacy access (vanilla Dolo compatibility)
symbols['parameters']  # -> ['β', 'γ', 'r']

# Structured access (dolo-plus mode)
symbols.decls['parameters']['β']  # -> SymbolDecl object
symbols.decls['parameters']['β'].value  # -> 0.96 (after calibration)
symbols.decls['parameters']['β'].domain  # -> ('interval', 'open', 0.0, 1.0)

Why this is ambiguous

The current approach inherits from dict to maintain backwards compatibility, but this creates questions:

  1. Is inheritance the right pattern? Dolo code uses symbols as a plain dict extensively. Inheriting from dict works, but it's unclear if this is the cleanest long-term design.

  2. Where should .decls live? Currently .decls is an attribute on SymbolsDict. Alternatives:

  3. Separate object: model.symbol_decls alongside model.symbols
  4. Method: model.get_symbol_decl('parameters', 'β')

  5. Keep as-is: model.symbols.decls['parameters']['β']

  6. Should SymbolDecl be mutable? Currently it's a mutable dataclass (.value is set after calibration). Should it be immutable with a separate calibrated view?

Options

  1. Keep as-is: SymbolsDict extends dict, provides .decls attribute
  2. Wrapper pattern: Keep symbols as plain dict, attach structured view via separate attribute on Model
  3. Full replacement: Make symbols a proper class with explicit methods for both views (breaking change)
  • dolo/compiler/symbols.py: SymbolsDict, SymbolDecl, DecoratorApp
  • dolo/compiler/model.py: SymbolicModel.symbols property

5. Do labelled sub-equations imply branching fan-out? (dcsn_to_cntn_*)

This ambiguity is about how to interpret named sub-equations (YAML mappings) when they appear under forward-transition keys, especially in branching stages.

The intended idea (fan-out via labels)

If a stage’s continuation is branch-keyed (e.g. poststates.own, poststates.rent), then it is tempting to allow:

  • equations.dcsn_to_cntn_transition as a mapping keyed by those same labels

and interpret the label → equation blocks as fan-out branches (multiple dcsn→cntn kernels), rather than as “just a named set of equations”.

Why this is ambiguous

We already use labelled sub-equations for a different purpose:

  • In mover blocks like cntn_to_dcsn_mover, labels (Bellman, InvEuler, …) represent different functional operators / computations on the same continuation value function, not branching.

So “subequations = fan-out” is not a valid global rule: backward induction often computes multiple objects from the same \(V^{>}\) even in non-branching stages.

Minimal resolution rule (proposed)

Treat labelled sub-equations under forward transitions as branch fan-out only when:

  • the stage is kind: branching, and
  • the sub-equation keys match the declared continuation-perch labels (poststates.{label}), and
  • each labelled block writes only to fields in its corresponding continuation perch.

Otherwise, treat labelled sub-equations as ordinary named components (not branches).

Pointers:

  • docs/development/dolo-plus-impl/spec_0.1l-branching.md §3.2 (branch transitions) and §11.2 (parsing rules).