Monday, February 8, 2010
4:00pm

5130 Upson Hall

Abstract:

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.