I was wondering whether the concept of sampling from a probability distribution can be formalized in a functional manner, so that for example one can talk about the composition of a function that returns distributions with the sampling function. In theory, it should look something like this:
$$ \texttt{sample}：\bigcup_{X∈} (X) → \bigcup_{X∈}X， p ↦ \operatorname{\texttt{sample}}(p) $$
- $$ is the universe of all sets of sample spaces we might be interested in.
- $(X)$ is the set of all probability distributions on $X$.
- $\texttt{sample}$ is non-deterministic.
However, by definition, a function in ZFC is deterministic, so $\texttt{sample}$ does not exists. (aside from other issues like $$ being potentially a proper class and not a set.)
Questions
- Why is it that our foundations do not allow the definition of $\texttt{sample}$? It seems like an object one would like to use and talk about. Non-deterministic functions are ubiqutos in application
- Are there alternative foundations that allow a rigorous definition of $\texttt{sample}$?