Bellman operator
Economoist.Bellman computes one Bellman optimality update. At each output state, it takes the larger of two action values: immediate reward plus discounted expected continuation value. The package implements this for two states and three states, with two actions per state. The outputs are separate functions, such as bellman_state0 and bellman_state0_n3.
Checked properties
Section titled “Checked properties”properties/bellman.ch checks the exported functions under nonnegative transition entries, transition rows summing to one, and a discount 0 < g < 1. Each property concerns one application of the operator. Both state sizes have these goals:
| Goal at two states | Goal at three states | What it checks |
|---|---|---|
bellman_monotone | bellman3_monotone | For output state 0, entrywise v ≤ w implies (Tv)₀ ≤ (Tw)₀. |
bellman_bounded | bellman3_bounded | For output state 0, if b, rmax ≥ 0, continuation values lie in [-b, b], and both action rewards lie in [-rmax, rmax], then (Tv)₀ lies in [-(rmax + g b), rmax + g b]. |
bellman_contraction_state0, bellman_contraction_state1 and their _lower goals | bellman_contraction_state0_n3, bellman_contraction_state1_n3, bellman_contraction_state2_n3 and their _lower goals | At every output state, the upper and lower goals together give |(Tv)ₛ - (Tw)ₛ| ≤ g ‖v-w‖∞. |
The monotonicity and boundedness claims apply to output state 0. The contraction claims cover every output state at the listed sizes; together, their per-state bounds imply the vector sup-norm bound for those cases.
The assumptions on the transition probabilities support the difference bound.
The discount g < 1 makes its contraction factor strictly less than one.
The checked contraction applies once, at two or three states with two actions. It does not prove convergence of value iteration, existence or uniqueness of a fixed point, or the same result for arbitrary state and action counts. The separate state-0 monotonicity and boundedness checks must not be read as vector-wide prover results.
SMT interprets these f32 expressions over the reals. It does not certify
the corresponding floating-point executions.