一句话：提出加权编程范式及 Dijkstra 风格的 wp/wlp 演算，用以规约并推理超出概率分布的数学模型。
概率编程只能刻画以概率分布为取值范围的数学模型。本文提出更一般的「加权编程」范式：程序在通常的命令式语言之上增加两个特性——（1）非确定性分支，（2）对执行迹赋权，权既可以是数，也可以是字母表上的词、多项式、形式幂级数或基数等对象。作者据此发展了 Dijkstra 风格的 weakest-precondition 与 weakest-liberal-precondition 演算，用于对加权程序所规约的数学模型进行推理。文中给出若干案例研究，例如用加权程序不仅建模 ski rental 这一在线优化问题本身，还建模求解该问题的最优确定性在线算法，从而在源代码层面借助 wp 推理计算出该在线算法的竞争比。
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.
@article{paperbot1516,
title = {Weighted programming: a programming paradigm for specifying mathematical models},
author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527310}
}