0.1f Constraints

Spec 0.1f — VFI Control Bounds via ⊥ Declarations

Status: Implemented Scope: Vanilla Dolo enhancement (not dolo-plus pipeline)

1. Goal

Enable Value Function Iteration (VFI) solvers to read control bounds directly from the model YAML by allowing ⊥ (up tack) bound declarations within the value equation block.

Currently: - Bounds are only parsed from arbitrage block using ⟂ (complementarity) syntax - VFI solver expects controls_lb(m, s, p) and controls_ub(m, s, p) functions - These functions don't exist unless arbitrage equations are defined - VFI models that use felicity/value (not arbitrage) cannot specify bounds

This spec introduces the ⊥ prefix for bound constraints within the value block.

---

2. Motivation

VFI solves:

V(s) = max_x { felicity(s, x) + β * E[V(s')] }
       s.t.  lb(s) <= x <= ub(s)

The solver needs callable bound functions:

lb = controls_lb(m, s, parms)  # returns array of lower bounds
ub = controls_ub(m, s, parms)  # returns array of upper bounds

Current workaround: Define dummy arbitrage equations just to attach ⟂ bounds — semantically incorrect for VFI models.

Proposed: Use ⊥ prefix to declare bounds within the value block.

2.1 Formal semantics (constraints define the feasible set Γ)

This spec is easiest to interpret using the same "syntax → formal problem" reading used elsewhere in this repo: 06-from-syntax-to-formal-problem-definition.md.

In the formal dynamic program, bounds are not "extra equations" and they do not define implicit maps like transition equalities do. Instead, bounds specify the feasible (constraint) correspondence for the maximization step:

\[ x \in \Gamma(m,s,p),\qquad \Gamma(m,s,p) := \{x : \mathrm{lb}(m,s,p)\le x \le \mathrm{ub}(m,s,p)\}. \]

So a line like:

⊥ 0.0 <= c[t] <= w[t]

is a declarative constraint-set statement ("\(c\) is chosen subject to \(0\le c\le w\)"), i.e. it defines \(\Gamma(\cdot)\) for VFI.

Important (timing/semantics):

• In Dolang+ semantics, a control is chosen at the decision perch (even if some representations evaluate policies on other grids).
• In vanilla Dolo VFI, the maximization is implemented by the solver; the value: block provides the objective and ⊥ lines provide the solver's box constraints.

Infinity constants:

• inf is treated as \(+\infty\) (and -inf as \(-\infty\)), so e.g. ⊥ 0 <= n[t] <= inf is valid.

---

3. Syntax

3.1 Symbol choice: ⊥ (up tack)

• Symbol: ⊥ (U+22A5, "up tack" or "bottom")
• Meaning: Marks a bound constraint line (as opposed to an equation)
• Relation to ⟂: Visually related but semantically distinct:
• ⟂ = complementarity (equation ⟂ constraint, used in arbitrage)
• ⊥ = bound constraint (standalone, used in value/VFI)

3.2 Bounds within value block

value: |
    V[t] = u[t] + beta*V[t+1]
    ⊥ 0.0 <= c[t] <= w[t]

3.3 Multiple controls

value: |
    V[t] = c[t]^(1-sigma)/(1-sigma) - chi*n[t]^(1+eta)/(1+eta) + beta*V[t+1]
    ⊥ 0.0 <= n[t] <= inf
    ⊥ 0.0 <= i[t] <= y[t]

3.4 State-dependent bounds

value: |
    V[t] = log(c[t]) + beta*V[t+1]
    ⊥ 0.01 <= c[t] <= w[t]

The upper bound w[t] is a state variable — bounds can depend on (m, s, p).

---

4. Parsing rules

4.1 Grammar additions (dolang)

Add to grammar.lark:

bound_constraint: _UPTACK double_inequality
_UPTACK: "⊥"

Extend block parsing to recognize bound_constraint lines within value blocks.

4.2 Line classification

Within a value: | block, lines are classified as: - Equation line: Contains = (the Bellman equation) - Bound line: Starts with ⊥ followed by lb <= x[t] <= ub

V[t] = u[t] + beta*V[t+1]     →  equation (parse as equality)
⊥ 0.0 <= c[t] <= w[t]         →  bound (parse as bound_constraint)

4.3 Bound ordering

Bounds must be declared in the same order as symbols.controls:

symbols:
    controls: [n, i]   # order matters

value: |
    V[t] = ...
    ⊥ 0.0 <= n[t] <= inf    # first bound → first control (n)
    ⊥ 0.0 <= i[t] <= y[t]   # second bound → second control (i)

Parser validates that the variable in each ⊥ declaration matches the expected control at that index.

4.4 Output functions

Extracted bounds compile to: - controls_lb(m, s, p) → returns [lb_0, lb_1, ...] - controls_ub(m, s, p) → returns [ub_0, ub_1, ...]

These are the exact function names VFI expects (see value_iteration.py lines 53-54).

---

5. Recipe additions

Add to recipes.yaml:

controls_lb:
    optional: True
    recursive: True
    eqs:
        - ['exogenous', 0, 'm']
        - ['states', 0, 's']
        - ['parameters', 0, 'p']

controls_ub:
    optional: True
    recursive: True
    eqs:
        - ['exogenous', 0, 'm']
        - ['states', 0, 's']
        - ['parameters', 0, 'p']

---

6. Implementation changes

6.1 dolang/grammar.lark

Add bound constraint rule:

bound_constraint: _UPTACK double_inequality
_UPTACK: "⊥"

Update start and block rules to recognize bound constraints:

?start: equation | predicate | bound_constraint

value_block: _NEWLINE? equation (_NEWLINE equation | _NEWLINE bound_constraint)* _NEWLINE?

6.2 dolo/compiler/model.py

1. When parsing value block, split lines into equations vs bound constraints:

   if g == "value":
       equations = []
       bounds_lb = []
       bounds_ub = []
       for line in block_lines:
           if line.strip().startswith("⊥"):
               # Parse as bound_constraint
               parsed = parse_string(line, start="bound_constraint")
               # Extract lb, variable, ub from double_inequality
               bounds_lb.append(extract_lb(parsed))
               bounds_ub.append(extract_ub(parsed))
           else:
               # Parse as equation
               equations.append(line)
       d["value"] = equations
       if bounds_lb:
           d["controls_lb"] = bounds_lb
           d["controls_ub"] = bounds_ub
   

2. Validate bound variable order matches symbols.controls.

6.3 dolo/compiler/factories.py

Add handling for controls_lb and controls_ub equation types (line ~72):

if eq_type in ("arbitrage_lb", "arbitrage_ub", "controls_lb", "controls_ub"):
    specs = {
        "eqs": recipes["dtcc"]["specs"]["arbitrage"]["complementarities"]["left-right"]
    }

6.4 dolo/algos/value_iteration.py

Update to use model.x_bounds fallback (recommended):

# Current (lines 53-54):
controls_lb = model.functions["controls_lb"]
controls_ub = model.functions["controls_ub"]

# Proposed:
if model.x_bounds is not None:
    controls_lb, controls_ub = model.x_bounds
else:
    raise ValueError("VFI requires control bounds. Add ⊥ declarations to value block.")

This leverages the existing model.x_bounds property which already checks both controls_* and arbitrage_* functions.

---

7. Edge cases and gotchas

7.1 Old-style YAML list form

The parser currently handles two YAML styles for equation blocks:

Block scalar (recommended for ⊥):

value: |
    V[t] = u[t] + beta*V[t+1]
    ⊥ 0.0 <= c[t] <= w[t]

List form (legacy):

value:
    - V[t] = u[t] + beta*V[t+1]
    - ⊥ 0.0 <= c[t] <= w[t]      # WILL FAIL with current parser

The list form parses each item with start="equation", which does not recognize ⊥ as a valid start token. Implementation must either: - Extend list-form parsing to detect and handle ⊥ lines, OR - Reject ⊥ in list form with a clear error message recommending block scalar syntax

Recommendation: Support block scalar only for ⊥ bounds. Add validation that rejects ⊥ in list form with helpful error:

Error: Bound constraints (⊥) must use block scalar syntax.
Change:
    value:
        - V[t] = ...
        - ⊥ 0 <= c[t] <= w[t]
To:
    value: |
        V[t] = ...
        ⊥ 0 <= c[t] <= w[t]

7.2 Control variable time-index validation

The existing arbitrage complementarity validation (model.py lines 210-222) requires the bounded variable to be a timed variable at t=0:

expected = (self.symbols["controls"][i], 0)  # e.g., ("c", 0) for c[t]
if (v, t) != expected:
    raise Exception(f"Incorrect variable in complementarity...")

Edge cases to handle:

Syntax	Valid?	Notes
⊥ 0 <= c[t] <= w[t]	✓	Standard form
⊥ 0 <= c <= w[t]	✗	Missing time index on c — reject
⊥ 0 <= c[t-1] <= w[t]	✗	Wrong time index — reject
⊥ 0 <= c[t+1] <= w[t]	✗	Wrong time index — reject

Implementation: Reuse existing validation logic. Reject non-timed or wrong-time variables with clear error:

Error: Bound variable must be a control at time t.
Found: c (no time index)
Expected: c[t]

7.3 Default bounds behavior

Current state: value_iteration.py directly accesses model.functions["controls_lb"] with no fallback. Models with value but no ⊥ lines will raise KeyError.

Options:

Option	Behavior	Pros	Cons
A. Require bounds	Error if no ⊥ for VFI models	Explicit, catches mistakes	More verbose for simple models
B. Default to ±inf	Generate controls_lb = [-inf, ...], controls_ub = [+inf, ...]	Convenient	May hide missing constraints
C. Use model.x_bounds fallback	Check controls_* → arbitrage_* → error	Unified interface	Slightly more complex

Recommendation: Option C — use model.x_bounds property.

The property already exists (model.py lines 1020-1032):

@property
def x_bounds(self):
    if "controls_ub" in self.functions:
        fun_lb = self.functions["controls_lb"]
        fun_ub = self.functions["controls_ub"]
        return [fun_lb, fun_ub]
    elif "arbitrage_ub" in self.functions:
        fun_lb = self.functions["arbitrage_lb"]
        fun_ub = self.functions["arbitrage_ub"]
        return [fun_lb, fun_ub]
    else:
        return None

This allows: 1. VFI models with ⊥ bounds → uses controls_lb/ub 2. Legacy models with arbitrage + ⟂ → falls back to arbitrage_lb/ub 3. Models with neither → clear error from VFI solver

7.4 recipes.yaml gap

Current state: recipes.yaml has no entry for controls_lb or controls_ub. The factory will fail when trying to compile these equation types.

Required addition (as specified in Section 5):

controls_lb:
    optional: True
    recursive: True
    eqs:
        - ['exogenous', 0, 'm']
        - ['states', 0, 's']
        - ['parameters', 0, 'p']

controls_ub:
    optional: True
    recursive: True
    eqs:
        - ['exogenous', 0, 'm']
        - ['states', 0, 's']
        - ['parameters', 0, 'p']

Note: The signature (m, s, p) matches the existing arbitrage complementarities spec at recipes["dtcc"]["specs"]["arbitrage"]["complementarities"]["left-right"].

7.5 Number of bounds vs number of controls

Validation required: The number of ⊥ declarations must match len(symbols.controls).

symbols:
    controls: [n, i]    # 2 controls

value: |
    V[t] = ...
    ⊥ 0 <= n[t] <= inf  # only 1 bound — ERROR

Error message:

Error: Number of bounds (1) does not match number of controls (2).
Missing bounds for: i

---

8. Example: Full VFI model

name: consumption_savings_vfi

symbols:
    exogenous: [e_y]
    states: [w]
    controls: [c]
    values: [V]
    rewards: [u]
    parameters: [beta, gamma, r, sigma_y]

definitions:
    y[t]: exp(e_y[t])

equations:

    transition:
        - w[t] = (w[t-1] - c[t-1]) * r + y[t]

    felicity:
        - u[t] = c[t]^(1-gamma) / (1-gamma)

    value: |
        V[t] = u[t] + beta*V[t+1]
        ⊥ 0.01 <= c[t] <= w[t]

calibration:
    beta: 0.96
    gamma: 2.0
    r: 1.03
    sigma_y: 0.1
    w: 1.0
    c: 0.5
    V: 0.0
    u: c^(1-gamma)/(1-gamma)

exogenous: !Normal
    Sigma: [[sigma_y**2]]

domain:
    w: [0.1, 10.0]

options:
    grid: !Cartesian
        orders: [100]

Multiple controls example (RBC):

value: |
    V[t] = c[t]^(1-sigma)/(1-sigma) - chi*n[t]^(1+eta)/(1+eta) + beta*V[t+1]
    ⊥ 0.0 <= n[t] <= inf
    ⊥ 0.0 <= i[t] <= y[t]

Usage:

from dolo import yaml_import
from dolo.algos.value_iteration import value_iteration

model = yaml_import("consumption_savings_vfi.yaml")
result = value_iteration(model, verbose=True)

---

9. Backwards compatibility

• Arbitrage models: Unchanged. arbitrage + ⟂ continues to produce arbitrage_lb/ub.
• Time iteration: Uses arbitrage_lb/ub — unaffected.
• VFI models: Can now use value block with ⊥ bound declarations.
• Symbol distinction:
• ⟂ (U+27C2) = complementarity (in arbitrage)
• ⊥ (U+22A5) = bound constraint (in value)

---

10. Acceptance criteria

10.1 Core functionality

• [ ] Grammar updated: bound_constraint rule added to grammar.lark
• [ ] ⊥ declarations parsed from value block (block scalar form)
• [ ] Bounds compiled to controls_lb/controls_ub functions
• [ ] recipes.yaml includes controls_lb and controls_ub specs
• [ ] VFI solver uses model.x_bounds fallback
• [ ] VFI solver runs on models using new syntax

10.2 Validation

• [ ] Bound variable order validated against symbols.controls order
• [ ] Bound variable time-index validated (c[t] required, not c or c[t-1])
• [ ] Number of bounds validated against number of controls
• [ ] State-dependent bounds (e.g., c[t] <= w[t]) work correctly

10.3 Error handling

• [ ] Clear error for ⊥ in list-form YAML (recommend block scalar)
• [ ] Clear error for missing time index on bounded variable
• [ ] Clear error for wrong time index on bounded variable
• [ ] Clear error for mismatched control name in bound
• [ ] Clear error for wrong number of bounds vs controls
• [ ] Clear error for VFI model with no bounds defined

10.4 Backwards compatibility

• [ ] Existing arbitrage + ⟂ models continue to work unchanged
• [ ] model.x_bounds returns arbitrage_lb/ub when controls_lb/ub not present
• [ ] Time iteration solver unaffected

---

11. Future extensions

• Unified x_bounds interface: model.x_bounds property already checks both controls_* and arbitrage_* (see model.py line 1020-1032). Ensure this works seamlessly.
• Bounds in felicity block: Could extend if needed for alternative model structures.
• General inequality constraints: g(x) <= 0 beyond box bounds (would require different solver).

Christopher Carroll and Akshay Shanker — repository in development, please do not cite.