Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
A Theory of Slicing for Imperative Probabilistic Programs
Beteiligte:
Amtoft, Torben;
Banerjee, Anindya
Erschienen:
Association for Computing Machinery (ACM), 2020
Erschienen in:
ACM Transactions on Programming Languages and Systems, 42 (2020) 2, Seite 1-71
Sprache:
Englisch
DOI:
10.1145/3372895
ISSN:
0164-0925;
1558-4593
Entstehung:
Anmerkungen:
Beschreibung:
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.