A one-dimensional chain of four states; Goal is the absorbing target.

Move left or right; edges are clamped.

Deterministic transition.

>>> step R S0
S1

>>> step L S0
S0

>>> step R S2
Goal

State reward: living penalty, goal bonus.

>>> reward S0
-1.0

>>> reward Goal
10.0

One-step Bellman backup for a fixed deterministic policy.

One-step Bellman optimality backup.

Finite-horizon value iteration from the zero value function.

>>> valueIter 0 0.9 S0
0.0

>>> valueIter 1 0.9 S0
-1.0

>>> valueIter 2 0.9 S0
-1.9

Greedy policy with respect to a value function.

State-dependent score modality. Not exported by Prob because it leaks the input into the scalar map; useful for RL rewards.

Transition as a Prob morphism.

Reward as a state-dependent score modality.

Bellman backup for a fixed action, expressed as three Prob morphisms: reward, then discount, then transition. The contravariant composition in Prob reads right-to-left on continuations, so the written order is the operational order.

Apply a Prob Bellman backup to a value function at a state.

N-step discounted return via Prob composition.

Composes 'bellmanP gamma a' n times via the Category instance, then applies the result to a zero continuation. By the laws of Prob Category composition, this is the n-step Bellman backup: reward on each step, discounted and summed.

>>> discountedReturn 0.5 R 4 S0
-0.5

Closed-form discounted return on a deterministic chain.

Σ_{t=0}^{n-1} γ^t · reward(step^t(a, s)). All terms are exact in Double when γ is a dyadic rational (e.g. 0.5) and rewards are integers.

>>> closedFormReturn 0.5 R 4 S0
-0.5

Step a finite-state stochastic Moore machine by expectation, exactly as in the circuits keystone, but specialised to 'Mono i o' with full state observation.

The gridworld as a controlled stochastic Moore machine.

Input: action (L or R). Output: full state observation.

MDP interface: action in, next-state and reward out.

This matches the instance-table claim that the MDP row uses Mono a (s', r). The reward is pinned on the current state to match bellmanSystem / bellmanOpt.

Check one deterministic MDP step by continuation.

POMDP interface: hidden state carried as a Const position, external loop is action in / observation out.

This matches the instance-table claim that the POMDP row uses a state-hiding Prod (Const s) (Mono a o). The Const s position exposes the hidden state as output but supplies no direction, so the external agent cannot feed it back as input.

Check one deterministic POMDP step by continuation.

POMDP observation: coarse location, not the true state.

Coarse observation function.

One-step Bellman optimality backup via 'System (Prob)'.

Reward is pinned on the current state (matching bellmanOpt); the System runner computes the expected discounted future value of the next state.

Finite-horizon value iteration using the System runner.

Min-plus tropical semiring over Double.

Finite-horizon shortest-path cost to goal.

>>> getTropical (shortestPath 0 S0)
Infinity

>>> getTropical (shortestPath 1 S0)
Infinity

>>> getTropical (shortestPath 2 S0)
Infinity

>>> getTropical (shortestPath 3 S0)
3.0

>>> getTropical (shortestPath 3 Goal)
0.0