 Probabilistic program

A probabilistic program maps elementary random choices to outputs and observation weights. Its mathematical meaning can be specified by the pushforward measure on outputs, normalized after conditioning when the observation has finite positive mass. Different random-choice spaces can implement the same output law.