Probabilistic program
= 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.