# Weighted Programming

arXiv: https://arxiv.org/abs/2202.07577 · HTML: https://mlsanity.com/paper/2202.07577/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 77 references that are in the map.
- First posted on arXiv 15 Feb 2022.

## Builds on (most cited first, 7 of 7)

- [Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs](https://mlsanity.com/paper/1802.10467/) (2018)
- [Healthiness from Duality](https://mlsanity.com/paper/1605.00381/) (2016)
- [Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic](https://mlsanity.com/paper/1910.07910/) (2019)
- [Generalising KAT to verify weighted computations](https://mlsanity.com/paper/1911.01146/) (2019)
- [Tensors over Semirings for Latent-Variable Weighted Logic Programs](https://mlsanity.com/paper/2006.04232/) (2020)
- [Graded Hoare Logic and its Categorical Semantics](https://mlsanity.com/paper/2007.11235/) (2020)
- [Quantitative Strongest Post](https://mlsanity.com/paper/2202.06765/) (2022)

## Built on by (most cited first, 1 of 1)

- [SMT-Based Active Learning of Weighted Automata](https://mlsanity.com/paper/2605.07758/) (2026)

## Abstract (arXiv)

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.