Probabilistic Semantics and Probabilistic Logic
Monday, February 8, 2010
5130 Upson Hall
In this talk I will describe two complementary but equivalent
semantics for a high-level probabilistic programming language.
One of these interprets programs as continuous linear operators
on a space of measures. This is a "forward-moving"
semantics analogous to powerdomain transformers for nondeterministic
programs. The other is a measurable-function transformer semantics.
It is a "backward-moving" semantics analogous to predicate transformers.
The two semantics are dual in the sense of Stone duality.
I will then describe a logic based on these semantics called
PPDL. It is more arithmetic in nature than truth-functional,
thus it might better be called a calculus than a logic.
It satisfies a small model property and can be
decided in polynomial space, thus is amenable to model-checking.
I will give an example of its use in deriving
mechanically the expected length of a random walk.