Probabilistic list traversal

The support of ordinary List.mapM consists exactly of the lists whose entries are supported by the corresponding calls. The relation also records the exact output length. These are semantic laws; computational efficiency is provided separately in Computability.Probabilistic.

Main results

• Cslib.ProbComp.mem_support_mapM_iff: pointwise support characterizes list traversal.
• Cslib.ProbComp.eval_mapM_splice: sample a designated coordinate before its surrounding traversal without changing the joint distribution.

theorem Cslib.ProbComp.mem_support_mapM_iff {α β : Type} (program : α → ProbComp β) (inputs : List α) (outputs : List β) : outputs ∈ (List.mapM program inputs).eval.support ↔ List.Forall₂ (fun (a : α) (b : β) => b ∈ (program a).eval.support) inputs outputs

The support of list traversal is exactly the pointwise support of the individual calls.

theorem Cslib.ProbComp.eval_mapM_splice {α β : Type} (program : α → ProbComp β) (before : List α) (middle : α) (after : List α) : (do let challenge ← program middle let front ← List.mapM program before let back ← List.mapM program after pure (front ++ challenge :: back)).eval = (List.mapM program (before ++ middle :: after)).eval

Sampling a designated coordinate before its prefix and suffix preserves the full traversal law. The three computations use independent randomness, and the returned order is unchanged.