A Theory of Slicing for Probabilistic Control Flow Graphs
by Torben Amtoft and Anindya Banerjee.
Abstract: The task of program slicing is to remove the parts of a program that are irrelevant in a given context. In probabilistic programs, where variables may be assigned random values from a given distribution, and undesirable combinations of values may be removed by ``observe'' statements, the standard notions of data and control dependence no longer suffice for semantically correct slicing, as demonstrated by Hur et al. in recent work. This paper presents a theory for slicing probabilistic programs, represented as control flow graphs whose nodes transform probability distributions. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. We state correctness in terms of observational equivalence between the behaviors of the sliced program and of the original. A program's behavior is its final probability distribution and we demand equality modulo a constant factor so as to allow the removal of ``observe'' statements that do not introduce any bias in the final distribution. This will be the case if the variables tested by ``observe'' statements are probabilistically independent of those variables relevant for the final value. To ensure this, a key feature of our syntactic conditions is that they involve two disjoint slices, such that the variables of one are probabilistically independent of the variables of the other.