Weighted Programming

TL;DR

This paper introduces weighted programming as a flexible paradigm for modeling mathematical systems with nondeterminism and weights, extending probabilistic programming to broader mathematical contexts.

Contribution

It develops formal calculi for reasoning about weighted programs and demonstrates their application through case studies like the ski rental problem.

Findings

Weighted programming can specify diverse mathematical models beyond probability.

Weakest-precondition calculi enable formal reasoning about weighted programs.

Applied to the ski rental problem, the approach determines the competitive ratio of online algorithms.

Abstract

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 \`{a} 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.