Kleene Algebra of Weighted Programs with Domain

Weighted programs were recently introduced by Batz et al. (Proc. ACM Program. Lang. 2022) as a generalization of probabilistic programs which can also represent optimization problems and, in general, programs whose execution traces carry some sort of weight. Batz et al. show that a weighted version of Dijkstra’s weakest precondition operator can be used to reason about the competitive ratios of weighted programs. In this paper we study a propositional abstraction of weighted programs with three main contributions. First, we formulate a semantics for weighted programs with the weighted weakest precondition operator based on functions from multimonoids to quantales. Second, we show that the weighted weakest precondition operator corresponds to a generalization of the domain operator known from Kleene algebra with domain, and we study the properties of the generalized domain operator. Third, we formulate a weighted version of Kleene algebra with domain as a framework for reasoning about weighted programs with weakest precondition in an abstract setting.