A Theory of Slicing for Imperative Probabilistic Programs

Abstract

Dedicated to the memory of Sebastian Danicic. We present a theory for slicing imperative probabilistic programs containing random assignments and "observe" statements for conditioning. We represent such programs as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. This allows direct adaptation of standard machinery such as data dependence, postdominators, relevant variables, and so on, to the probabilistic setting. We separate the specification of slicing from its implementation: (1) first, we develop syntactic conditions that a slice must satisfy (they involve the existence of another disjoint slice such that the variables of the two slices are probabilistically independent of each other); (2) next, we prove that any such slice is semantically correct; (3) finally, we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. Our results carry over to the slicing of structured imperative probabilistic programs, as handled in recent work by Hur et al. For such a program, we can define its slice, which has the same "normalized" semantics as the original program; the proof of this property is based on a result proving the adequacy of the semantics of pCFGs w.r.t. the standard semantics of structured imperative probabilistic programs.