Evaluating memoized probabilistic programs

Evaluating a memoized program preserves the joint answer and cache distribution. This is the probabilistic specialization of the generic monad-morphism rule for memoize.

Main results

• Cslib.ProbComp.eval_memoize: evaluation commutes with a cached call.

References

Specializes IsMonadHom.map_memoize, adapted from Foundations/Control/Monad/Memoize.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

@[simp]

theorem Cslib.ProbComp.eval_memoize {Key Value : Type} [BEq Key] (compute : Key → ProbComp Value) (key : Key) (cache : List (Key × Value)) : (memoize compute key cache).eval = memoize (fun (q : Key) => (compute q).eval) key cache

Evaluate the underlying sampler, retaining the same answer and entire list cache.