Probabilistically Accurate Program Transformations
The standard approach to program transformation involves the use of discrete logical reasoning to prove that the applied transformation does not change the observable semantics of the program. This paper, in contrast, introduces a novel approach that uses probabilistic reasoning to justify transformations that may change the result that the program produces. The authors' approach provides probabilistic guarantees that the absolute value of the difference between the results that the transformed and original programs produce will rarely be large. A user or developer can specify bounds on the acceptable difference. The analysis can then determine the conditions under which the transformed computation satisfies the probabilistic guarantees for those bounds.