面向加权程序的带测试 Kleene 代数

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