论文标题
加权编程
Weighted Programming
论文作者
论文摘要
我们研究加权编程，这是一种用于指定数学模型的编程范例。更具体地说，我们研究的加权程序就像通常的命令式程序一样，具有两个其他功能：（1）非确定性分支和（2）加权执行跟踪。权重可以是数字，也可以是其他对象，例如字母，多项式，正式功率系列或基本数字的单词。我们认为，加权编程作为范例可用于指定超出概率分布的数学模型（如概率编程中所做的那样）。 我们开发了最弱的和最弱的自由主义 - 前提风格的计算，用于对加权程序指定的数学模型的推理。我们提出了一些案例研究。例如，我们使用加权编程来对滑雪租赁问题进行建模 - 优化问题。我们不仅对优化问题本身进行建模，而且对以加权程序解决此问题解决此问题的最佳确定性在线算法进行建模。通过最弱的前提式推理，我们可以确定源代码级别的在线算法的竞争比率。
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.
