A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories

TL;DR

This paper develops a categorical semantics for stochastic memoization and name generation in probabilistic programming, validating data flow transformations and bridging traditional probability with higher-order models.

Contribution

It introduces the first model of stochastic memoization for constant Bernoulli functions with non-enumerable types using presheaf categories and a novel probability monad.

Findings

Validates data flow transformations in stochastic memoization

Bridges traditional probability theory with higher-order probabilistic models

Provides a categorical semantics for a minimal probabilistic programming language

Abstract

Stochastic memoization is a higher-order construct of probabilistic programming languages that is key in Bayesian nonparametrics, a modular approach that allows us to extend models beyond their parametric limitations and compose them in an elegant and principled manner. Stochastic memoization is simple and useful in practice, but semantically elusive, particularly regarding dataflow transformations. As the naive implementation resorts to the state monad, which is not commutative, it is not clear if stochastic memoization preserves the dataflow property -- i.e., whether we can reorder the lines of a program without changing its semantics, provided the dataflow graph is preserved. In this paper, we give an operational and categorical semantics to stochastic memoization and name generation in the context of a minimal probabilistic programming language, for a restricted class of functions. Our contribution is a first model of stochastic memoization of constant Bernoulli functions with a non-enumerable type, which validates data flow transformations, bridging the gap between traditional probability theory and higher-order probability models. Our model uses a presheaf category and a novel probability monad on it.