Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.

翻译：加权程序是对概率程序的一般化，提供了一种通过算法表示来指定和编码数学模型的框架。带有测试的Kleene代数是一种基于正则表达式的代数形式化方法，在证明程序等价性方面具有应用。我们扩展了带有测试的Kleene代数的语言，使其足以形式化关于简化版加权程序的推理。我们为扩展语言引入了关系语义，并将关系语义推广到带有测试的Kleene代数的适当扩展，称为带有权重和测试的Kleene代数。通过一个示例，我们展示了带有权重和测试的Kleene代数提供了一个简单的代数框架，用于推理加权程序的等价性和最优运行。