Kleene Algebra With Tests for Weighted Programs

TL;DR

This paper extends Kleene algebra with tests to handle weighted programs, providing an algebraic framework for reasoning about program equivalence and optimization in probabilistic and mathematical models.

Contribution

It introduces Kleene algebra with weights and tests, extending existing algebraic formalism to reason about weighted programs and their equivalence.

Findings

Relational semantics for the extended language are developed.

The framework can reason about equivalence and optimal runs of weighted programs.

An example demonstrates the practical applicability of the algebraic approach.

Abstract

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.

Equations

$$\Big{(}\{\texttt{neq0}\}\big{(}\texttt{sub1}(\texttt{one}+\texttt{skis}\,\texttt{end})\big{)}\Big{)}^{*}\,\{\neg\texttt{neq0}\}\,.$$

$$\sum _{i\in I}(x\cdot x_i)=x\cdot \left(\sum _{i\in I}{x}_i\right)\sum _{i\in I}(x_i\cdot x)=\left(\sum _{i\in I}{x}_i\right)\cdot x$$

$$x⪯y⟺\exists z(x+z=y).$$

$$\mathbf{T}=({\mathbb{N}}^{\infty },\min ,+,0^{\mathbb{N}},\infty )$$

$$1+x{x}^{\ast }\le x^{\ast }1+x^{\ast }x\le x^{\ast }$$

$$y+xz\le z\to x^{\ast }y\le zy+zx\le y\to y{x}^{\ast }\le z$$

$$x{y}^{\ast }z=\sum _{n\ge 0}x{y}^{n}z.$$

$${\mathbf{Rel}}_X=(2^{X\times X},\cup ,\circ ,{}^{\ast },{\mathrm{id}}_X,\varnothing ),$$

$${\mathbf{Reg}}_{\Delta }=({\mathrm{Reg}}_{\Delta },\cup ,\cdot ,{}^{\ast },\{ϵ\},\varnothing ).$$

$$\mathbf{K}=(K,B,\cdot ,+,{}^{\ast },{}^{-},1,0)$$

$$A_0{p}_1{A}_1{p}_2{A}_2\dots p_k{A}_k$$

$$xA\diamond A^{\prime }y=\{\begin{array}{ll}xAy& \text{if }A=A^{\prime }\\ \text{undefined}& \text{otherwise}.\end{array}$$

$${\mathbf{G}}_{\mathsf{A},\mathsf{T}}=(2^{G{S}_{\mathsf{A},\mathsf{T}}},2^{1_{\mathsf{A}}},\cup ,\diamond ,{}^{\ast },{}^{-},1_{\mathsf{A}},\varnothing ),$$

$$\mathbf{K}=(K,B,S,\cdot ,+,{}^{\ast },{}^{-},1,0)$$

$${\mathbf{T}}^{\mathbf{G}}=(({\mathbb{N}}^{\infty }{)}^{GS},B,S,\cdot ,+,{}^{\ast },{}^{-},1,0)$$

$${\mathbf{S}}^{\mathbf{P}}=(S^G,B,W,\cdot ,+,{}^{\ast },{}^{-},1,0)$$

$$(W,\cdot ,+,1,0)\cong \mathbf{S}.$$

$$A_0{p}_1{A}_1\dots p_n{A}_n{\square }^m,$$

$$X⋓Y:=\{s(\min (U))\mid U=\{n\mid s(n)\in X\cup Y\}\}.$$

$$xA(n)\diamond A^{\prime }y(m)=\{\begin{array}{ll}xAy(n+m)& \text{if }A=A^{\prime }\\ \text{undefined}& \text{otherwise.}\end{array}$$

$$\mathbf{GT}=(K,B,S,\cdot ,⋓,{}^{\ast },{}^{-},1_{\mathsf{A}},\varnothing )$$

$$\begin{gathered}(\{\texttt{neq0}\}\,\texttt{sub1}\,\texttt{one})^{*}\\ \big{(}\{\texttt{neq0}\}\,\texttt{sub1}\,\texttt{skis}\,\texttt{end}\,(\{\texttt{neq0}\}\,\texttt{sub1}\,\texttt{one})^{*}\ \big{)}^{*}\\ \{\neg\texttt{neq0}\}\end{gathered}$$

$${\text{sub1}}^n\{\text{neq0}\}=0$$

$$\text{end}\{\text{neq0}\}=0$$

$$\begin{gathered}(\{\texttt{neq0}\}\,\texttt{sub1}\,\texttt{one})^{+n}\\ \big{(}\mathtt{1}+\{\texttt{neq0}\}\,\texttt{sub1}\,\texttt{skis}\,\texttt{end}\big{)}\{\neg\texttt{neq0}\}\end{gathered}$$

$$\displaystyle\{\neg\texttt{neq0}\}\big{(}0\big{)},\quad\{\texttt{neq0}\}\texttt{sub1}\{\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}y\big{)}\,,$$

$$\displaystyle\{\texttt{neq0}\}\texttt{sub1}\{\neg\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}y\big{)}\,,$$

$$\displaystyle\{\texttt{neq0}\}\texttt{sub1}\{\neg\texttt{neq0}\}\big{(}1\big{)}\,,$$

$$\displaystyle\{\texttt{neq0}\}\texttt{sub1}\{\texttt{neq0}\}\texttt{sub1}\{\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}1+y\big{)}\,,$$

$$\displaystyle\{\texttt{neq0}\}\texttt{sub1}\{\texttt{neq0}\}\texttt{sub1}\{\neg\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}1+y\big{)}\,,$$

$$⋮$$

$$\displaystyle\Big{(}\{\texttt{neq0}\}\texttt{sub1}\Big{)}^{n}\{\neg\texttt{neq0}\}\big{(}n\big{)}\,,$$

$$\displaystyle\Big{(}\{\texttt{neq0}\}\texttt{sub1}\Big{)}^{n}\{\texttt{neq0}\}\texttt{sub1}\{\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}n+y\big{)}\,,$$

$$\displaystyle\Big{(}\{\texttt{neq0}\}\texttt{sub1}\Big{)}^{n}\{\texttt{neq0}\}\texttt{sub1}\{\neg\texttt{neq0}\}\texttt{end}\{\neg\texttt{neq0}\}\big{(}n+y\big{)}$$

$${\vartheta }_G(Y)=\{A(n)\mid \exists x(xA(n)\in Y\diamond G){\}}^{⋓}.$$

Full text

I Introduction

Weighted programs [3] add two features to standard while programs [1]: (i) nondeterministic branching, and (ii) the ability to weight the current execution trace. As such, they generalize probabilistic programs [2], in which execution can branch based on the outcome of a random coin flip.

Batz et al. [3] argue that, in addition to being an interesting generalization, weighted programs offer a useful programming paradigm for specifying and encoding mathematical models, such as optimization problems or probability distributions, by means of an algorithmic representation. They introduce structural operational semantics and a Dijkstra-style weakest precondition calculus for weighted programs, and they use this calculus to determine competitive ratios of weighted programs.

Kleene algebra with tests [10], KAT, is an extension of the algebraic theory of regular languages that provides a simple algebraic formalism for equational specification and verification of while programs, and for proving equivalence of programs. In this note we extend the language of KAT so that it is sufficient to formalize reasoning about a propositional abstraction of weighted programs where assignments are replaced by unstructured atomic actions. 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, or KAWT. We demonstrate by means of an example that KAWT offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.

The note is structured as follows. Section II introduces weighted regular programs, an expansion of regular programs with weights, and shows that weighted regular programs can express a propositional abstraction of weighted programs where assignments are replaced by unstructured atomic actions. Section III introduces a relational semantics for weighted regular programs using weighted transition systems where weights are elements of an arbitrary semiring. Section IV recalls the basics of Kleene algebra and Section V introduces an expansion of Kleene algebra with tests that generalizes the relational semantics of weighted regular programs. The expansion is called Kleene algebra with weights and tests, and it adds a semiring subalgebra (representing weights) to Kleene algebra with tests. Section VI demonstrates by means of an example how Kleene algebra with weights and tests can be used to reason about equivalence and optimal runs of regular while programs.

II Weighted programs

It is well-known that while programs can be represented using the syntax of regular programs [13, 5]. The latter contains nondeterministic branching (or choice) as one of the basic operations, so it is natural to extend regular programs with weights to capture weighted programs. For the sake of simplicity, we will work with a propositional abstraction of weighted programs where assignments $\mathtt{x}:=E$ are replaced by unstructured “atomic programs” in the style of [5, 10]. We will see that even in this simpler setting we are able to carry out a significant amount of reasoning about weighted programs.

Definition 1**.**

A signature is $\Sigma=(\mathsf{P},\mathsf{B},\mathsf{F})$, a triple of disjoint sets of variables, intuitively representing atomic programs, Boolean tests, and weighted tests, respectively. The set of weighted regular programs over $\Sigma$, $\mathsf{WRP}_{\Sigma}$, consists of expressions of the following sorts:

[TABLE]

(It is assumed that $\mathtt{b}\in\mathsf{B}$, $\mathtt{f}\in\mathsf{F}$, and $\mathtt{p}\in\mathsf{P}$.) We will sometimes write $\bar{b}$ instead of $\neg b$ and $pq$ instead of $p\cdot q$.

The language of weighted regular programs extends the language of Kleene algebra with tests [10] corresponding to regular programs by adding the sort of “weightings”, that is, semiring terms representing assignments of weights to computation paths. Weights are represented by elements of an abstract semiring [4, 12]. Recall how the language of KAT expresses standard control flow commands of while programs:

• •

skip $:=\mathtt{1}$ and abort $:=\mathtt{0}$

• •

sequential composition $p\,;\,q:=pq$

• •

if $b$ then $p$ else $q$ $:=(bp)+(\neg bq)$

• •

while $b$ do $p$ $:=(bp)^{*}\neg b$

Note that nondeterministic branching (choice) is represented in the language of regular programs by the $+$ operator.

Example 1**.**

Recall the “ski rental program”, the main motivating example of a weighted program in [3]:111The ski rental problem is an optimization problem regarding a situation where one goes for a skying trip for $n$ days and has the choice of renting a pair of skis for $1$ Euro per day vs. buying a pair of skis for $y$ Euros.

The operator $\oplus$ in line 4 expresses nondeterministic branching between computation sequences, one of which executes the “weighting” $\odot 1$, or “add one unit of weight” and returns to the beginning of the while loop, and the other executes $\odot y$, or “add $y$ units of weight”, then assigns $n:=0$, and then returns to the beginning of the loop, after which the Boolean test $n>0$ is evaluated as False and the computation halts.

The structure of the ski rental program can be represented by the following weighted regular program (for the sake of readability, we use descriptive variable names, bold font for weighting variables, and we enclose Boolean expressions in curly brackets):

[TABLE]

In this program, $\texttt{neq0}\in\mathsf{B}$ represents the test $n>0$, $\texttt{sub1}\in\mathsf{P}$ represents the instruction $n:=n-1$ to subtract $1$ from the value of $n$, $\texttt{end}\in\mathsf{P}$ represents the assignment $n:=0$ that ends the loop, and $\texttt{one},\texttt{skis}\in\mathsf{F}$ represent the weightings $\odot 1$ (adding one unit of weight) and $\odot y$ (adding the price of the skis), respectively.

III Relational semantics

In this section we introduce relational semantics for weighted regular programs, based on semiring-valued transition systems.

Definition 2**.**

A semiring is $\mathbf{S}=(S,+,\cdot,1,0)$ where

• •

$(S,+,0)$* is a commutative monoid;*

• •

$(S,\cdot,1)$* is a monoid;*

• •

$x\cdot(y+z)=(x\cdot y)+(x\cdot z)$* and $(x+y)\cdot z=(x\cdot z)+(y\cdot z)$;*

• •

$0\cdot x=0=x\cdot 0$.

A semiring is idempotent iff $x+x=x$ for all $x\in S$. A semiring is complete iff $(S,+,0)$ is a complete monoid and the following distributivity laws hold:

[TABLE]

(Complete idempotent semirings are also known as quantales.) We define the natural order $\preceq$ on a semiring as follows:

[TABLE]

We note that in idempotent semirings the natural order coincides with the semilattice order $\leq$ defined by $x\leq y\iff x+y=y$.

Example 2**.**

(1) An example of a complete idempotent semiring that is well known especially from shortest path algorithms is the tropical semiring over extended natural numbers

[TABLE]

where

• •

$\mathbb{N}^{\infty}=\mathbb{N}\cup\{\infty\}$, where $\infty\notin\mathbb{N}$;

• •

$\mathrm{min}$* is the minimum operation extended to $\mathbb{N}^{\infty}$ by defining $\mathrm{min}(n,\infty)=\mathrm{min}(\infty,n)=n$ for all $n$; $\mathrm{min}$ is seen as semiring addition (hence, $\infty$ is the minimal element in the ordering $\leq$ defined by $x\leq y$ iff $\mathrm{min}(x,y)=y$);*

• •

$+$, representing semiring multiplication, is addition on $\mathbb{N}$ and $n+\infty=\infty=\infty+n$ for all $n$ (hence, $\infty$ is the annihilator element);

• •

$0^{\mathbb{N}}$, the natural number zero, is the neutral element with respect to $+$.

(2) Another example well-known from the theory of fuzzy logic is the Łukasiewicz semiring $\textbf{{\L}}=([0,1],\mathrm{max},\otimes,1,0)$ where $[0,1]$ is the real unit interval and $\otimes$ is the Łukasiewicz t-norm $x\otimes y=\mathrm{max}\{0,x+y-1\}$.

Intuitively, semirings can be seen as representing a set of weights together with an operation of weight addition (semiring multiplication $\cdot$), a weight comparison relation $\preceq$ induced by semiring addition $+$, and two designated weights, namely, “no weight” $1$ and the “absolute” weight [math].

Definition 3**.**

Let $\mathbf{S}$ be a semiring. An $\mathbf{S}^{\Sigma}$-transition system is $(X,L)$ where $X\neq\emptyset$ and $L$ is a function such that

$L(\mathtt{p})\subseteq X\times X$*   $L(\mathtt{b})\subseteq X$  $L(\mathtt{f})\in\mathbf{S}\,.$*

Intuitively, $(s,t)\in L(\mathtt{p})$ means that the atomic program $\mathtt{p}$ may terminate in state $t$ when executed in state $s$; $s\in L(\mathtt{b})$ means that the atomic Boolean expression $\mathtt{b}$ is evaluated to True in $s$; and $L(\mathtt{f})\in\mathbf{S}$ is the weight assigned to the atomic weighting expression $\mathtt{f}$.

Equivalently, $L$ in an $\mathbf{S}^{\Sigma}$-transition system can be seen as a function from $\bigcup\Sigma$ to $\mathbf{S}^{X\times X}$ such that

• •

$L(\mathtt{p}),L(\mathtt{b})\in\{0,1\}^{X\times X}$;

• •

$L(\mathtt{b})(s,t)=0$ and $L(\mathtt{f})(s,t)=0$ if $s\neq t$;

• •

$L(\mathtt{f})(s,t)=L(\mathtt{f})(s^{\prime},t^{\prime})$ for all $s,s^{\prime},t,t^{\prime}\in X$.

(In effect, $L(\mathtt{b})$ and $L(\mathtt{f})$ are functions from the identity relation on $S$ which in turn represents $S$.)

In a given $\mathbf{S}^{\Sigma}$-semiring, $L$ can be extended to a function $\mathsf{WRP}_{\Sigma}\to\mathbf{2}^{X\times X}$ specifying the interpretation of each weighted regular program by lifting the weighted regular program operations to the set of functions $X\times X\to\mathbf{S}$ :

Definition 4**.**

Let $\lambda,\lambda^{\prime}\in\mathbf{S}^{X\times X}$ and let $\theta\in\{0,1\}^{X\times X}$

• •

$\mathbf{1}=\mathrm{id}_{X}$* (the identity relation on $X$);*

• •

$\mathbf{0}(s,t)=0$;

• •

$(\lambda+\lambda^{\prime})(s,t)=\lambda(s,t)+\lambda^{\prime}(s,t)$;

• •

$(\lambda\cdot\lambda^{\prime})(s,t)=\sum\{\lambda(s,u)\cdot\lambda^{\prime}(u,t)\mid u\in X\}$;

• •

$(\neg\theta)(s,t)=\begin{cases}1&\text{if }s=t\text{ and }\theta(s,t)=0\\ 0&\text{otherwise;}\end{cases}$**

• •

$\lambda^{0}=\mathbf{1}$* and $\lambda^{n+1}=\lambda^{n}\cdot\lambda$.*

If $\mathbf{S}$ is a complete semiring, then we define:

• •

$\lambda^{*}=\sum_{n\geq 0}\lambda^{n}$.

It is easily checked that $(\mathbf{S}^{X\times X},\cdot,+,\mathbf{1},\mathbf{0})$ is a semiring; see Lemma 1 below. We denote $\{0,1\}^{X\times X}$ as $2^{X\times X}$.

IV Kleene algebra

Kleene algebras [8, 9] are structures that arise naturally in the study of regular languages, finite automata and shortest path algorithms, for instance. Kleene algebra offers an elegant framework for equational reasoning about regular programs [10]. In this section we recall the basic preliminaries on Kleene algebra.

Definition 5**.**

A Kleene algebra is an idempotent semiring with a unary operation ∗ that satisfies the following (quasi)equations:

[TABLE]

A Kleene algebra is **∗-continuous* iff it satisfies*

[TABLE]

Example 3**.**

(1) The Kleene algebra of binary relations on a non-empty set $X$ is

[TABLE]

where $\mathbf{2}^{X\times X}$ is the set of all binary relations on $X$, $\cup$ is union, $\circ$ is relational composition, $\,{}^{*}$ is reflexive transitive closure, and $\mathrm{id}_{X}$ is the identity relation on $X$.

(2) Take a finite set of symbols $\Delta$ and let $\Delta^{*}$ be the set of finite sequences over $\Delta$, including the empty sequence $\epsilon$. Let $\mathrm{Reg}_{\Delta}$ be the smallest subset of $\mathbf{2}^{\Delta^{*}}$ (i.e. the set of all languages over $\Delta$) that contains the empty set $\emptyset$, the set $\{\epsilon\}$, and $\{\mathtt{x}\}$ for all $\mathtt{x}\in\Delta$ that is closed under finite unions and the following operations:

• •

$X\cdot Y=\{xy\mid x\in X\And y\in Y\}$, i.e. the set of concatenations of strings from $X$ with strings from $Y$;

• •

$X^{*}=\bigcup_{n\geq 0}X^{n}$, where $X^{0}=\{\epsilon\}$ and $X^{n+1}=X^{n}\cdot X$, i.e. the set of all strings that can be parsed as concatenations of a finite number of strings in $X$ (Kleene iteration).

The set $\mathrm{Reg}_{\Delta}$ is called the set of regular languages over $\Delta$. The Kleene algebra of regular languages over $\Delta$ is

[TABLE]

Definition 6**.**

A Kleene algebra with tests [10] is a structure of the form

[TABLE]

where

• •

$(K,\cdot,+,\,^{*},1,0)$* is a Kleene algebra;*

• •

$B\subseteq K$, and $(B,\cdot,+,\,^{-},1,0)$ is a Boolean algebra.

A Kleene algebra with tests is ∗-continuous iff its underlying Kleene algebra is ∗-continuous.

In a Kleene algebra with tests, elements of $B$ are seen as “tests” of statements formulated in a Boolean language, while elements of $K$ in general represent “structured actions”.

Example 4**.**

(1) Every Kleene algebra is a Kleene algebra with tests. Take $B=\{1,0\}$ and define $\,{}^{-}$ as Boolean complementation on $B$.

(2) A relational Kleene algebra with tests over some set $X$ is the expansion of $\mathbf{Rel}_{X}$ with the set of subsets of $\mathrm{id}_{X}$ (seen as $B$), and the complementation operation on the set of subsets of $\mathrm{id}_{X}$ (seen as $\,{}^{-}$).

(3) Take two finite sets $\mathsf{A}$ and $\mathsf{T}$ of program and Boolean variables, respectively. We assume that $\mathsf{A}=\{\mathtt{b}_{1},\ldots,\mathtt{b}_{n}\}$ is ordered in some fixed but arbitrary way. An atom over $\mathsf{A}$ is a sequence $\mathtt{b}_{1}^{\pm}\ldots\mathtt{b}_{n}^{\pm}$, where $\mathtt{b}_{i}^{\pm}\in\{\mathtt{b}_{i},\bar{\mathtt{b}}_{i}\}$. Let $1_{\mathsf{A}}$ be the set of all atoms over $\mathsf{A}$. A guarded string over $\mathsf{A},\mathsf{T}$ is any sequence of the form (for $k\geq 0$)

[TABLE]

where each $A_{i}$ is an atom over $\mathsf{A}$ and each $p_{i}\in\mathsf{T}$. Guarded strings can be seen as representations of execution traces of programs (abstract states are replaced by atoms). Let $2^{GS_{\mathsf{A},\mathsf{T}}}$ be the set of all sets of guarded strings over $\mathsf{A},\mathsf{T}$. Obviously $1_{\mathsf{A}}\subseteq 2^{GS_{\mathsf{A},\mathsf{T}}}$. The coalesced product operation $\diamond$ is a partial binary function on $GS_{\mathsf{A},\mathsf{T}}$ defined as follows:

[TABLE]

The coalesced product operation is lifted to sets of guarded strings in an obvious way. Note that the coalesced product operation on sets of guarded strings is a total function. The algebra of guarded languages over $\mathsf{A},\mathsf{T}$ [11],

[TABLE]

is a ∗-continuous Kleene algebra with tests ($X^{*}=\bigcup_{n\geq 0}X^{n}$, where exponentiation is defined using $\diamond$).

Lemma 1**.**

Let $X$ be a non-empty set and $\mathbf{S}$ a semiring. Then

$\mathbf{S}(X)=(\mathbf{S}^{X\times X},\cdot,+,\mathbf{1},\mathbf{0})$* is a semiring;* 2. 2.

if $\mathbf{S}$ is idempotent (complete), then $\mathbf{S}(X)$ is idempotent (complete); 3. 3.

if $\mathbf{S}$ is idempotent and complete, then $\mathbf{S^{*}}(X)=(\mathbf{S}(X),\,^{*})$ is a ∗-continuous Kleene algebra; 4. 4.

if $\mathbf{S}$ is idempotent and complete, then $\mathbf{S^{*}_{2}}(X)=(\mathbf{S^{*}}(X),\mathbf{2}^{\mathrm{id}_{X}},\neg)$ is a ∗-continuous Kleene algebra with tests.

(We note that $\mathbf{S^{*}_{2}}(X)$ provides a natural example of a Kleene algebra with tests where the set of tests, that is $\mathbf{2}^{\mathrm{id}_{X}}$, is not identical to the set of elements under $\mathbf{1}=\mathrm{id}_{X}$, where $\lambda\leq\lambda^{\prime}$ iff $\lambda(s,t)\leq\lambda^{\prime}(s,t)$ for all $s,t\in X\times X$.)

Lemma 2**.**

The subalgebra of $\mathbf{S}(X)$ consisting of all constant functions is isomorphic to $\mathbf{S}$.

V Kleene algebra with weights and tests

Given the applications of Kleene algebra in reasoning about regular and while programs, it is natural to consider a Kleene-algebraic perspective on weighted programs. Gomes et al. [6] formulate a generalization of KAT called graded KAT (or GKAT) where the Boolean algebra of tests is replaced by a more general algebraic structure. Batz et al. [3] point out that a deeper study of the applicability of GKAT to reasoning about weighted programs is an interesting problem to look at. Weighted programs in the sense of [3] combine Boolean tests and weightings (weighted tests), and so it seems natural to consider a generalization of the GKAT approach.

Definition 7**.**

A Kleene algebra with weights and tests is a structure

[TABLE]

where

• •

$(K,\cdot,+,\,^{*},1,0)$* is a Kleene algebra;*

• •

$B\subseteq K$* and $S\subseteq K$;*

• •

$(B,\cdot,+,\,^{-},1,0)$* is a Boolean algebra;*

• •

$(S,\cdot,+,1,0)$* is a semiring.*

A valuation in $\mathbf{K}$ is any homomorphism $v$ from $\mathsf{WRP}_{\Sigma}$ to $\mathbf{K}$ such that $v(\mathtt{b})\in B$ and $v(\mathtt{f})\in S$. Two programs $p,q\in\mathsf{WRP}_{\Sigma}$ are equivalent in a class $\mathcal{K}$ of Kleene algebras with weights and tests iff $v(p)=v(q)$ for all valuations $v$ in all $\mathbf{K}\in\mathcal{K}$ .

Clearly each KAT is a KAWT; just take any subuniverse $S$ of $K$. However, there are more interesting examples.

Example 5**.**

(1) Our first example combines a Kleene algebra of guarded languages with the tropical semiring. Take the set of guarded strings over some fixed $\mathsf{A}$ and $\mathsf{T}$, and denote it as $GS$. A function $\lambda:GS\to\mathbb{N}^{\infty}$, assigning a weight to each guarded string, can be seen as specifying the weights of execution traces of a program (if $\lambda(s)=\infty$, then either $s$ is not a trace that can be generated by the program corresponding to $\lambda$ or the trace carries an “absolute weight”). Note that functions $\lambda:GS\to\mathbb{N}^{\infty}$ generalize sets of guarded strings ($GS\to\{0^{\mathbb{N}},\infty\}$), i.e. elements of the Kleene algebra $\mathbf{G}$. Take

[TABLE]

where $(\mathbb{N}^{\infty})^{GS}$ is the set of all functions from $GS$ to $\mathbb{N}^{\infty}$ and

• •

$1(s)=\begin{cases}0^{\mathbb{N}}&\text{if }s\in 1_{\mathsf{A}}\\ \infty&\text{otherwise;}\end{cases}$**

• •

$0(s)=\infty$* for all $s$;*

• •

$\lambda\in B$* iff $\lambda(s)\in\{0^{\mathbb{N}},\infty\}$ for all $s\in GT$ and $\lambda(s)=0^{\mathbb{N}}$ only if $s\in 1_{\mathsf{A}}$;*

• •

$S=\{\lambda\mid\lambda(s)=\infty$* if $s\not\in 1_{\mathsf{A}}$ and $\lambda(A_{i})=\lambda(A_{j})$ for all $A_{i},A_{j}\in 1_{\mathsf{A}}\}$;*

• •

$(\lambda\cdot\lambda^{\prime})(s)=\mathrm{min}\{\lambda(t)+^{\mathbb{N}^{\infty}}\lambda^{\prime}(u)\mid s=t\diamond u\}$;

• •

$(\lambda+\lambda^{\prime})(s)=\mathrm{min}\{\lambda(s),\lambda^{\prime}(s)\}$;

• •

(\lambda^{*})(s)=\mathrm{min}_{n\geq 0}\big{(}\lambda^{n}(s)\big{)}* where $\lambda^{n}$ is defined using $\cdot\,;$*

• •

$\,{}^{-}:B\to B$* such that $(\bar{\lambda})(s)=\infty$ iff $\lambda(s)\neq\infty$.*

It can be shown that $\mathbf{T^{G}}$ is a (∗-continuous) Kleene algebra with weights and tests where $(S,\cdot,+,1,0)\cong\mathbf{T}$. $\mathbf{T^{G}}$ also contains a (proper) subalgebra isomorphic to $\mathbf{G}$, namely, $(\{0^{\mathbb{N}},\infty\}^{G},B,\cdot,+,\,^{*},\,^{-},1,0)$.

(2) A similar construction can be carried out using $\mathbf{T}$ and $\mathbf{Rel}_{X}$. We leave the details to the reader, noting just that the coalesced product operation $\diamond$ can be defined on $X\times X$ by stipulating that $(s,t)\diamond(u,v)$ is $(s,v)$ if $t=u$ and is undefined otherwise.

The construction encountered in the previous example can obviously be carried out in a more general setting. In fact, we can use a slight generalization of the well known notion of formal power series coming up for instance in the study of weighted automata [4, 12]. Formal power series are functions from a monoid to a semiring; we will build on functions from certain partial semigroups.

Definition 8**.**

A partial semigroup with identity is $(G,D,\diamond,I)$ where $G\neq\emptyset$, $D$ is a binary relation on $G$, $\diamond:D\to G$, and $I\subseteq G$ such that

• •

$D(x,y)\And D(x\diamond y,z)$* iff $D(y,z)\And D(x,y\diamond z)$;*

• •

$D(x,y)\And D(x\diamond y,z)$* only if $(x\diamond y)\diamond z=x\diamond(y\diamond z)$;*

• •

for all $x$ there is $y$: $I(y)$ and $D(x,y)$;

• •

for all $x$ there is $y$: $I(y)$ and $D(y,x)$;

• •

$D(x,y)$* and $I(y)$ only if $x=x\diamond y$;*

• •

$D(y,x)$* and $I(y)$ only if $x=y\diamond x$.*

We note that the first two conditions above are stronger than the standard definition of a partial semigroup [7]. We’ll often write $xy$ instead of $x\diamond y$.

Example 6**.**

(1) An example of a partial semigroup with identity is $\mathbf{Cart}_{X}=(X\times X,D,\diamond,\mathrm{id}_{X})$ where $X\times X$ is the Cartesian product on a non-empty set $X$, $((x_{1},y_{1}),(x_{2},y_{2}))\in D$ iff $y_{1}=x_{2}$, $(x,y)\diamond(y,z)=(x,z)$, and $\mathrm{id}_{X}=\{(x,x)\mid x\in X\}$ is the identity relation on $X$.

(2) $\mathbf{Gu}_{\mathsf{A,T}}=(GS,D,\diamond,1_{\mathsf{A}})$ where $GS$ is the set of guarded strings over some $\mathsf{A}$ and $\mathsf{T}$, $\diamond$ is the coalesced product operation, $D$ is the set of pairs $(s,t)$ such that $s\diamond t$ is defined, and $1_{\mathsf{A}}$ is the set of atoms over $\mathsf{A}$.

(3) $\mathbf{Str}_{\Delta}=(\Delta^{*},D,\,^{\frown},\epsilon)$ where $\Delta^{*}$ is the set of finite sequences (strings) over a finite alphabet $\Delta$ (including the empty string $\epsilon$), $D$ is the universal relation on $\Delta^{*}$ and $\,{}^{\frown}$ is the concatenation operation (which is actually a total operation on $\Delta^{*}$).

Many well-known examples of Kleene algebras (with tests) are in fact algebras of functions from specific (regular) partial semigroups to the two-element Boolean semiring $\mathbf{Bo}=(\{1,0\},\land,\lor,1,0)$; the reader can easily verify this by considering some of the previous examples.

Definition 9**.**

Let $\mathbf{P}=(G,D,\diamond,I)$ be a partial semigroup with identity, and let $\mathbf{S}=(S,\cdot^{\mathbf{S}},+^{\mathbf{S}},1^{\mathbf{S}},0^{\mathbf{S}})$ be a complete idempotent semiring. We define

[TABLE]

where $S^{G}$ is the set of all functions form $G$ to $S$ and

• •

$1(x)=\begin{cases}1^{\mathbf{S}}&\text{if }x\in I\\ 0^{\mathbf{S}}&\text{otherwise;}\end{cases}$**

• •

$0(x)=0^{\mathbf{S}}$* for all $s$;*

• •

$\lambda\in B$* iff $\lambda(x)\in\{1^{\mathbf{S}},0^{\mathbf{S}}\}$ for all $x\in G$ and $\lambda(x)=1^{\mathbf{S}}$ only if $x\in I$;*

• •

$W=\{\lambda\mid\lambda(x)=0^{\mathbf{S}}$* if $x\not\in I$ and $\lambda(y)=\lambda(z)$ for all $y,z\in I\}$;*

• •

$(\lambda\cdot\lambda^{\prime})(x)=\sum\{\lambda(y)\cdot^{\mathbf{S}}\lambda^{\prime}(z)\mid(y,z)\in D\And y\diamond z=x\}$* (the sum uses $+^{\mathbf{S}}$);*

• •

$(\lambda+\lambda^{\prime})(x)=\lambda(x)+^{\mathbf{S}}\lambda^{\prime}(x)$;

• •

(\lambda^{*})(x)=\sum_{n\geq 0}\big{(}\lambda^{n}(x)\big{)}* where $\lambda^{n}$ is defined using $\cdot\,;$*

• •

$\,{}^{-}:B\to B$* such that $(\bar{\lambda})(x)=1^{\mathbf{S}}$ iff $\lambda(x)\neq 1^{\mathbf{S}}$.*

Theorem 1**.**

If $\mathbf{P}$ is a partial semigroup with identity and $\mathbf{S}$ is a complete idempotent semiring, then $\mathbf{S^{P}}$ is a ∗-continuous Kleene algebra with weights and tests where

[TABLE]

Given the relation of Kleene algebra to the algebra of regular languages [9], and the relation of Kleene algebra with tests to the algebra of regular guarded languages [11], it is natural to ask if, for any given class of semirings $\mathcal{S}$ (closed under isomorphisms) there is a Kleene algebra with weights and tests whose elements are sets of strings over some alphabet (a “language-theoretic” algebra, to use the terminology of [11]) which is free in the class of Kleene algebras with weights and tests whose semiring of weights belongs to $\mathcal{S}$. (That is, if the equational theory of the given class of Kleene algebras with weights and tests is complete with respect to a class language-theoretic algebras.)

We will not answer this question here, but we will note that $\mathbf{T^{G}}$ over any $\mathsf{A},\mathsf{T}$ (the algebra of functions from guarded strings over $\mathsf{A},\mathsf{T}$ to extended natural numbers) is isomorphic to a language-theoretic algebra.

Let $\Phi=(\mathsf{A},\mathsf{T})$ where $\mathsf{A}\subseteq\mathsf{B}$ is a finite set of Boolean variables and $\mathsf{T}\subseteq\mathsf{P}$ is a finite set of program variables. We assume that $\mathsf{A}=\{\mathtt{b}_{1},\ldots,\mathtt{b}_{n}\}$ is ordered in some fixed but arbitrary way. Let $\Box$ be a new symbol (i.e. $\Box\notin\bigcup\Sigma$). A weighted guarded string over $\Phi$ is a string of the form

[TABLE]

where all $A_{i}$ are atoms over $\mathsf{A}$ and all $p_{i}\in\mathsf{T}$. That is, weighted guarded strings over $\Phi$ are a guarded strings over $\Phi$ followed by a string of $m$ copies of $\Box$. We’ll write just $s(m)$, where $s\in GS$ and $m\in\mathbb{N}$. A weighted atom is $s(m)$ where $s\in 1_{\mathsf{A}}$.

Intuitively, a guarded string represents an execution trace of a program and the weight $\Box^{m}$ represents the weight of the trace. Hence, (some) sets of weighted guarded strings can be seen as representing the possible execution traces of weighted regular programs. If a set $X$ represents a program and $s(m)\notin X$ for all $m$, then $s$ is not a possible execution trace of the program, i.e. it has “infinite weight”.

A set $X$ of weighted guarded strings is unambiguous iff $s(n)\in X$ and $s(m)\in X$ only if $n=m$; moreover, $X$ is crisp iff $s(m)\in X$ only if $m=0$, and $X$ is uniform only if $s(n),t(m)\in X$ only if $n=m$. A set $X$ of weighted atoms is universal iff for all $A$ there is $n$ such that $A(n)\in X$. Note that a crisp set of weighted guarded strings is just a set of guarded strings, and that uniform sets are unambiguous.

The unambiguous union of two sets of weighted guarded strings $X,Y$ is

[TABLE]

Note that $\Cup$ is not necessarily idempotent, but it is a semilattice join operation on the set of all unambiguous sets of weighted guarded strings. We denote $X\Cup X$ as $X^{\Cup}$.

Coalesced product of weighted guarded strings is defined as follows:

[TABLE]

Definition 10**.**

Fix a $\Phi$. Let

[TABLE]

be an algebra such that:

• •

$K$* is the set of all unambiguous sets of weighted guarded strings over $\Phi$;*

• •

$B$* is the set of crisp sets of weighted atoms (i.e. the set of all sets of atoms);*

• •

$S$* is the set of uniform universal sets of weighted atoms;*

• •

$X\cdot Y=(X\diamond Y)^{\Cup}$;

• •

X^{*}=\text{\Large{\Cup}}_{n\geq 0}X^{n}* (where $X^{n}$ is defined using $\cdot$);*

• •

$\,{}^{-}$* is complementation on $1_{\mathsf{A}}$.*

(The ordinary lifting of $\diamond$ to sets of weighted guarded strings is not necessarily an unambiguous set.)

Theorem 2**.**

$\mathbf{T^{G}}\cong\mathbf{GT}$.

Definition 11**.**

A valuation in $\mathbf{GT}$ is called canonical iff

• •

if $\mathtt{p}\in\mathsf{T}$, then $v(\mathtt{p})=\{A\mathtt{\,p\,}B\mid A,B\in 1_{\mathsf{A}}\}$;

• •

if $\mathtt{b}\in\mathsf{A}$, then $v(\mathtt{b})=\{A\mid\neg\mathtt{b}\text{ does not occur in }A\}$.

VI Using Kleene algebra to reason about weighted programs

Using the (quasi)equational theory of Kleene algebra with weights and tests, we can reason about equivalence of weighted programs in a simple algebraic setting.

Example 7**.**

Recall the ski rental program and Example 1. Using Kleene algebra (see [9], Proposition 2.7), we can show that (1) is equivalent to

[TABLE]

Now consider the following equations:

[TABLE]

Both correspond to reasonable assumptions in the version of the ski rental scenario where the length of the trip in $n$ days, given the intended interpretation of the variables occurring in the equations: if you do subtract $1$ from $n$ $n$-times, then the test $n>0$ evaluates to False (3); and if you assign $n:=0$, then then the test $n>0$ evaluates to False (4).

Let us define $\gamma^{+n}:=1+\gamma+\gamma^{2}+\ldots+\gamma^{n}$. It is possible to show that, in each ∗-continuous KAWT where (3) and (4) hold, and where $1$ is the top element of $S$ (such as algebras where $S$ is isomorphic to the tropical semiring, for example), the program (2) is equivalent to

[TABLE]

Hence, it is possible to show using Kleene algebra with weights and tests that, on each input $n$, the program (2) is equivalent to a simpler program (5) that does not involve ∗. Hence, in a sense, (5) is finite.

Example 8**.**

Take $\mathbf{GT}$ over $\Phi=(\mathsf{A},\mathsf{T})$ where $\mathsf{A}=\{\{\texttt{neq0}\},\{\neg\texttt{neq0}\}\}$ and $\mathsf{T}=\{\texttt{sub1},\texttt{end}\}$. Take any canonical valuation where $v(\texttt{one})=\{A(1)\mid A\in 1_{\mathsf{A}}\}=\{\{\texttt{neq0}\}\Box,\{\neg\texttt{neq0}\}\Box\}$ and $v(\texttt{skis})=\{A(y)\mid A\in 1_{\mathsf{A}}\}=\{\{\texttt{neq0}\}\Box^{y},\{\neg\texttt{neq0}\}\Box^{y}\}\}$. Then $v$ maps the program (5) to the set $X$ of weighted guarded strings containing:

[TABLE]

Every set $G$ of weighted guarded strings in $\mathbf{GT}$ gives a function $\vartheta_{G}$ from $1_{\mathsf{A}}$ to the set of sets of weighted atoms defined by

[TABLE]

Hence, $\vartheta_{G}(Y)$ is the set weighted atoms representing the optimal execution traces from $G$ starting in an atom in $Y$. If $G$ is finite, then $\vartheta_{G}$ is obviously computable.

For example, $\vartheta_{X}(\{\neg\texttt{neq0}\})=\{\{\neg\texttt{neq0}\}\}$ (if the ski rental program is run in a state where $n=0$, then it halts immediately without accumulating any weight), and

[TABLE]

That is, an optimal run of (5) from a state where $n\neq 0$ will have weight $\mathrm{min}(n,y)$. This result agrees with intuition and the calculation in [3] using the weakest preweighting operator.

VII Conclusion

We introduced Kleene algebra with weights and tests, an expansion of Kleene algebra with tests suitable for formalizing reasoning about a simplified version of weighted programs discussed in [3]. We described constructions of some “concrete” KAWT, and we demonstrated by means of an example that KAWT can be used for reasoning about equivalence and optimal runs of weighted programs.

Many interesting topics need to be left to future research, including a study of free Kleene algebras with weights and tests, questions of decidability and computational complexity, and a systematic accommodation of the weakest preweighting operator of [3] into our framework.