Weighted Programming
This work addresses the need for a more general programming paradigm to model diverse mathematical structures, such as optimization problems, for researchers and practitioners in formal methods and theoretical computer science, though it appears incremental as it builds on existing weakest-precondition calculi.
The paper tackles the problem of specifying mathematical models beyond probability distributions by introducing weighted programming, a paradigm that extends imperative programs with nondeterministic branching and weighted execution traces, and develops weakest-precondition-style calculi for reasoning about such models, as demonstrated in case studies like modeling the ski rental problem and its online algorithm to determine competitive ratios at the source code level.
We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2) weighting execution traces. Weights can be numbers but also other objects like words from an alphabet, polynomials, formal power series, or cardinal numbers. We argue that weighted programming as a paradigm can be used to specify mathematical models beyond probability distributions (as is done in probabilistic programming). We develop weakest-precondition- and weakest-liberal-precondition-style calculi à la Dijkstra for reasoning about mathematical models specified by weighted programs. We present several case studies. For instance, we use weighted programming to model the ski rental problem - an optimization problem. We model not only the optimization problem itself, but also the best deterministic online algorithm for solving this problem as weighted programs. By means of weakest-precondition-style reasoning, we can determine the competitive ratio of the online algorithm on source code level.