Randomized Programming and Probabilistic Reasoning in Type Theory
by James Cheney
Randomness and probability are core concepts in computer science, used
in randomized algorithms, average case analyses of deterministic
algorithms, and decision-making systems in AI. We want to incorporate
random computations and probabilistic reasoning into NuPRL, for example
to analyze and verify randomized gossip for Ensemble. However, there
are some basic conflicts between the usual notions of probability and
randomness that keep this from being striaghtforward. I'll present a
number of approaches to doing probability in NuPRL and discuss their
merits and drawbacks.
This is work in progress and I don't have all the answers. I plan to leave time at the end for discussion. I'd especially like to find out whether my approach sounds OK to the people working with Ensemble, or if not what should change.