Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time

TL;DR

This paper introduces Guarded Kleene Algebra with Tests (GKAT), a simplified algebraic framework that enables nearly linear time verification of certain programs, contrasting with the more complex KAT.

Contribution

It develops the algebraic theory of GKAT, proves its near-linear time decidability, and establishes a Kleene theorem and completeness results.

Findings

GKAT's equational theory is almost linear time decidable.

A full Kleene theorem for GKAT is established.

Completeness of GKAT's axiomatization is proved.

Abstract

Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa's axiomatization of Kleene Algebra.

Equations

$$\begin{array}[t]{r@{\;\;}l@{\qquad}l}\lx@intercol b,c,d\in\mathsf{BExp}::=\hfil\lx@intercol\\[1.99997pt] \quad\mid&0&\boldsymbol{\mathsf{false}}\\[-0.85358pt] \mid&1&\boldsymbol{\mathsf{true}}\\[-0.85358pt] \mid&t\in T&t\\[-0.85358pt] \mid&b\cdot c&b~{}\boldsymbol{\mathsf{and}}~{}c\\[-0.85358pt] \mid&b+c&b~{}\boldsymbol{\mathsf{or}}~{}c\\[-0.85358pt] \mid&\overline{b}&\boldsymbol{\mathsf{not}}~{}b\end{array}\qquad\qquad\qquad\begin{array}[t]{r@{\;\,}l@{\qquad}l}\lx@intercol e,f,g\in\mathop{\mathsf{Exp}}::=\hfil\lx@intercol\\[1.99997pt] \quad\mid&p\in\Sigma&\boldsymbol{\mathsf{do}}~{}p\\[-0.85358pt] \mid&b\in\mathsf{BExp}&\boldsymbol{\mathsf{assert}}~{}b\\[-0.85358pt] \mid&e\cdot f&e\boldsymbol{\mathsf{;}}\,f\\[-0.85358pt] \mid&e+_{b}f&\boldsymbol{\mathsf{if}}~{}b~{}\boldsymbol{\mathsf{then}}~{}e~{}\boldsymbol{\mathsf{else}}~{}f\\[0.85358pt] \mid&e^{(b)}&\boldsymbol{\mathsf{while}}~{}b~{}\boldsymbol{\mathsf{do}}~{}e\end{array}$$

$$x\alpha \diamond \beta y:=\{\begin{array}{ll}x\alpha y& \text{if }\alpha =\beta \\ \text{undefined}& \text{otherwise.}\end{array}$$

$$L\diamond K:=\{x\diamond y\mid x\in L,y\in K\}.$$

$$L^0:=\mathsf{At}\text{penalty}50plus0.5filminus5.0pt{L}^{n+1}:=L^n\diamond L$$

$$L{+}_{B}K:=(B\diamond L)\cup (\overline{B}\diamond K)\text{penalty}50plus0.5filminus5.0pt{L}^{(B)}:=\bigcup _{n\ge 0}{(B\diamond L)}^n\diamond \overline{B}$$

$$\begin{array}{rl}[[p]]& :=\{\alpha p\beta \mid \alpha ,\beta \in \mathsf{At}\}\\ [[b]]& :=\{\alpha \in \mathsf{At}\mid \alpha \le b\}\end{array}\begin{array}{rl}[[e\cdot f]]& :=[[e]]\diamond [[f]]\\ [[e{+}_{b}f]]& :=[[e]]{+}_{[[b]]}[[f]]\end{array}\begin{array}{rl}[[e^{(b)}]]& :=[[e{]]}^{([[b]])}\end{array}$$

$$e{+}_{b}f\mapsto be+\overline{b}f\text{penalty}50plus0.5filminus5.0pt{e}^{(b)}\mapsto {(be)}^{\ast }\overline{b}$$

$$\frac{\text{vbox}(\sigma ,{\sigma }^{\prime })\in \mathrm{eval}(p)\text{vbox}}{\text{vbox}\text{vbox}(\sigma ,{\sigma }^{\prime })\in {\mathcal{R}}_i[[p]]}$$

$$[[e]]=[[f]]⟺\forall i.{\mathcal{R}}_i[[e]]={\mathcal{R}}_i[[f]]$$

$$\begin{array}[]{r@{\quad}r@{~~}c@{~~}l}\textit{arithmetic expressions}&a\in\mathcal{A}~{}~{}&::=\hfil~{}~{}&x\in\mathsf{Var}\mid n\in\mathbb{Z}\mid a_{1}+a_{2}\mid a_{1}-a_{2}\mid a_{1}\times a_{2}\\ \textit{boolean expressions}&b\in\mathcal{B}~{}~{}&::=\hfil~{}~{}&\boldsymbol{\mathsf{false}}\mid\boldsymbol{\mathsf{true}}\mid a_{1}<a_{2}\mid\boldsymbol{\mathsf{not}}~{}b\mid b_{1}~{}\boldsymbol{\mathsf{and}}~{}b_{2}\mid b_{1}~{}\boldsymbol{\mathsf{or}}~{}b_{2}\\ \textit{commands}&c\in\mathcal{C}~{}~{}&::=\hfil~{}~{}&\boldsymbol{\mathsf{skip}}\mid x\coloneqq a\mid c_{1};c_{2}\mid\boldsymbol{\mathsf{if}}~{}b~{}\boldsymbol{\mathsf{then}}~{}c_{1}~{}\boldsymbol{\mathsf{else}}~{}c_{2}\mid\boldsymbol{\mathsf{while}}~{}b~{}\boldsymbol{\mathsf{do}}~{}c\end{array}$$

$$\Sigma =\{x:-a\mid x\in \mathsf{Var},a\in \mathcal{A}\}\text{penalty}50plus0.5filminus5.0ptT=\{a_1<a_2\mid a_1,a_2\in \mathcal{A}\}$$

$$\mathrm{eval}(x:-a)$$

$$\sigma [x:=n]$$

$$\mathrm{sat}(a_1<a_2)$$

$$\mathsf{if}x<0\mathsf{then}(x:=0-x;x:=2\times x)\mathsf{else}(x:=2\times x)$$

$$⇝$$

$${\mathcal{P}}_i[[p]]$$

$${\mathcal{P}}_i[[e\cdot f]](\sigma )({\sigma }^{\prime })$$

$${\mathcal{P}}_i[[e{+}_{b}f]](\sigma )$$

$${\mathcal{P}}_i[[e^{(b)}]](\sigma )({\sigma }^{\prime })$$

$$[[e]]=[[f]]⟺\forall i.{\mathcal{P}}_i[[e]]={\mathcal{P}}_i[[f]]$$

$${\kappa }_i(\alpha )(\sigma )$$

$${\kappa }_i(\alpha pw)(\sigma )({\sigma }^{\prime })$$

$$\mathrm{eval}(p)(w):=\mathrm{Unif}(\{wp\alpha \mid \alpha \in \mathsf{At}\})\text{penalty}50plus0.5filminus5.0pt\mathrm{sat}(t):=\{x\alpha \in \mathsf{GS}\mid \alpha \le t\}$$

$$[[e]]=\{\alpha x\in \mathsf{GS}\mid {\mathcal{P}}_i[[e]](\alpha )(\alpha x)\ne 0\}.\text{qed}$$

$$c::=\dots \mid x\sim \mu \text{penalty}50plus0.5filminus5.0pt\Sigma =\dots \cup \{x\sim \mu \mid x\in \mathsf{Var},\mu \in D(\mathbb{Z})\}$$

$$\mathrm{eval}(x:=n)(\sigma ):={\delta }_{\sigma [x:=n]}\text{penalty}50plus0.5filminus5.0pt\mathrm{eval}(x\sim \mu )(\sigma ):=\sum _{n\in \mathbb{Z}}\mu (n)\cdot {\delta }_{\sigma [x:=n]}$$

$$E(b):=b\text{penalty}50plus0.5filminus5.0ptE(p):=0\text{penalty}50plus0.5filminus5.0ptE(e{+}_{b}f):=b\cdot E(e)+\overline{b}\cdot E(f)\text{penalty}50plus0.5filminus5.0ptE(e\cdot f):=E(e)\cdot E(f)\text{penalty}50plus0.5filminus5.0ptE(e^{(b)}):=\overline{b}$$

$$e\equiv f⟹[[e]]=[[f]].$$

$$\alpha py\in [[g]]$$

$$⟺\alpha py\in [[eg{+}_{b}f]]$$

$$⟺\alpha py\in [[eg]]\wedge \alpha \le b\text{or}\alpha py\in [[f]]\wedge \alpha \le \overline{b}$$

$$E(e)=0$$

$$⟺\exists y,\beta .y=y_1\beta y_2\wedge \alpha p{y}_1\beta \in [[e]]\wedge \beta y_2\in [[e^{(b)}f]]\wedge \alpha \le b\text{or}\alpha py\in [[f]]\wedge \alpha \le \overline{b}$$

$$E(e)=0$$

$$⟺\alpha py\in [[e{e}^{(b)}f{+}_{b}f]]=[[e^{(b)}f]]$$

$$D_{\alpha }(b)=\{\begin{array}{ll}1& \alpha \le b\\ 0& \alpha \nleqq b\end{array}\text{penalty}50plus0.5filminus5.0pt{D}_{\alpha }(p)=(p,1)\text{penalty}50plus0.5filminus5.0pt{D}_{\alpha }(e{+}_{b}f)=\{\begin{array}{ll}{D}_{\alpha }(e)& \alpha \le b\\ D_{\alpha }(f)& \alpha \le \overline{b}\end{array}\text{penalty}50plus0.5filminus5.0pt{D}_{\alpha }(e\cdot f)=\{\begin{array}{ll}(p,e^{\prime }\cdot f)& D_{\alpha }(e)=(p,e^{\prime })\\ 0& D_{\alpha }(e)=0\\ D_{\alpha }(f)& D_{\alpha }(e)=1\end{array}\text{penalty}50plus0.5filminus5.0pt{D}_{\alpha }(e^{(b)})=\{\begin{array}{ll}(p,e^{\prime }\cdot e^{(b)})& \alpha \le b\wedge D_{\alpha }(e)=(p,e^{\prime })\\ 0& \alpha \le b\wedge D_{\alpha }(e)\in 2\\ 1& \alpha \le \overline{b}\end{array}$$

Full text

uninterpreted programs, program equivalence, program schemes, guarded automata, coalgebra, Kleene algebra with Tests

††copyright: acmlicensed††doi: 10.1145/3371129††journalyear: 2020††journal: PACMPL††journalvolume: 4††journalnumber: POPL††publicationmonth: 1††ccs: Theory of computation Program schemes††ccs: Theory of computation Program reasoning

This paper is dedicated to Laurie J. Hendren (1958–2019), whose passion for teaching and research inspired us and many others. Laurie’s early work on McCAT (Erosa and Hendren, 1994) helped us understand the limits of Guarded Kleene Algebra with Tests and devise a suitable definition of well-nestedness that underpins our main results.

1. Introduction

Computer scientists have long explored the connections between families of programming languages and abstract machines. This dual perspective has furnished deep theoretical insights as well as practical tools. As an example, Kleene’s classic result establishing the equivalence of regular expressions and finite automata (Kleene, 1956) inspired decades of work across a variety of areas including programming language design, mathematical semantics, and formal verification.

Kleene Algebra with Tests (KAT) (Kozen, 1996), which combines Kleene Algebra (KA) with Boolean Algebra (BA), is a modern example of this approach. Viewed from the program-centric perspective, a KAT models the fundamental constructs that arise in programs: sequencing, branching, iteration, etc. The equational theory of KAT enables algebraic reasoning and can be finitely axiomatized (Kozen and Smith, 1996). Viewed from the machine-centric perspective, a KAT describes a kind of automaton that generates a regular language of traces. This shift in perspective admits techniques from coalgebra for reasoning about program behavior. In particular, there are efficient algorithms for checking bisimulation, which can be optimized using properties of bisimulations (Hopcroft and Karp, 1971; Bonchi and Pous, 2013) or symbolic automata representations (Pous, 2015).

KAT has been used to model computation across a wide variety of areas including program transformations (Angus and Kozen, 2001; Kozen, 1997), concurrency control (Cohen, 1994b), compiler optimizations (Kozen and Patron, 2000), cache control (Barth and Kozen, 2002; Cohen, 1994a), and more (Cohen, 1994a). A prominent recent application is NetKAT (Anderson et al., 2014), a language for reasoning about the packet-forwarding behavior of software-defined networks. NetKAT has a sound and complete equational theory, and a coalgebraic decision procedure that can be used to automatically verify many important networking properties including reachability, loop-freedom, and isolation (Foster et al., 2015). However, while NetKAT’s implementation scales well in practice, deciding equivalence for NetKAT is PSPACE-complete in the worst case (Anderson et al., 2014).

A natural question to ask is whether there is an efficient fragment of KAT that is reasonably expressive, while retaining a solid foundation. We answer this question positively with a comprehensive study of Guarded Kleene Algebra with Tests (GKAT), the guarded fragment of KAT. GKAT is a propositional abstraction of imperative while programs. We establish the fundamental properties of GKAT and develop its algebraic and coalgebraic theory. GKAT replaces the union $(e+f)$ and iteration $(e^{*})$ constructs in KAT with guarded versions: conditionals $(e+_{b}f)$ and loops $(e^{(b)})$ guarded by Boolean predicates $b$. The resulting language is a restriction of full KAT, but sufficiently expressive to model typical, imperative programs—e.g., essentially all NetKAT programs needed to solve practical verification problems can be expressed as guarded programs.

In exchange for a modest sacrifice in expressiveness, GKAT offers two significant advantages. First, program equivalence (for a fixed Boolean algebra) is decidable in nearly linear time—a substantial improvement over the PSPACE complexity for KAT (Cohen et al., 1996). Specifically, any GKAT expression $e$ can be represented as a deterministic automaton of size $\mathcal{O}(|e|)$, while KAT expressions can require as many as $\mathcal{O}(2^{|e|})$ states. As a consequence, any language property that is efficiently decidable for deterministic automata is also efficiently decidable for GKAT. Second, we believe that GKAT is a better foundation for probabilistic languages due to well-known issues that arise when combining non-determinism—which is native to KAT—with probabilistic choice (Varacca and Winskel, 2006; Mislove, 2006). For example, ProbNetKAT (Foster et al., 2016), a probabilistic extension of NetKAT, does not satisfy the KAT axioms, but its guarded restriction forms a proper GKAT.

Although GKAT is a simple restriction of KAT at the syntactic level, its semantics is surprisingly subtle. In particular, the “obvious” notion of GKAT automata can encode behaviors that would require non-local control-flow operators (e.g, $\boldsymbol{\mathsf{goto}}$ or multi-level $\boldsymbol{\mathsf{break}}$ statements) (Kozen and Tseng, 2008). In contrast, GKAT models programs whose control-flow always follows a lexical, nested structure. To overcome this discrepancy, we identify restrictions on automata to enable an analogue of Kleene’s theorem—every GKAT automaton satisfying our restrictions can be converted to a program, and vice versa. Besides the theoretical interest in this result, we believe it may also have practical applications, such as reasoning about optimizations in a compiler (Hendren et al., 1992). We also develop an equational axiomatization for GKAT and prove that it is sound and complete over a coequationally-defined language model. The main challenge is that without $+$, the natural order on KAT programs can no longer be used to axiomatize a least fixpoint. We instead axiomatize a unique fixed point, in the style of Salomaa’s work on Kleene Algebra (Salomaa, 1966).

Outline.

We make the following contributions in this paper.

• •

We initiate a comprehensive study of GKAT, a guarded version of KAT, and show how GKAT models relational and probabilistic programming languages (§ 2).

• •

We give a new construction of linear-size automata from GKAT programs (§ 4). As a consequence, the equational theory of GKAT (over a fixed Boolean algebra) is decidable in nearly linear time (§ 5).

• •

We identify a class of automata representable as GKAT expressions (§ 4) that contains all automata produced by the previous construction, yielding a Kleene theorem.

• •

We present axioms for GKAT (§ 3) and prove that our axiomatization is complete for equivalence with respect to a coequationally-defined language model (§ 6).

Omitted proofs appear in the appendix.

2. Overview: An Abstract Programming Language

This section introduces the syntax and semantics of GKAT, an abstract programming language with uninterpreted actions. Using examples, we show how GKAT can model relational and probabilistic programming languages—i.e., by giving actions a concrete interpretation. An equivalence between abstract GKAT programs thus implies a corresponding equivalence between concrete programs.

2.1. Syntax

The syntax of GKAT is parameterized by abstract sets of actions $\Sigma$ and primitive tests $T$, where $\Sigma$ and $T$ are assumed to be disjoint and nonempty, and $T$ is assumed to be finite. We reserve $p$ and $q$ to range over actions, and $t$ to range over primitive tests. The language consists of Boolean expressions, $\mathsf{BExp}$, and GKAT expressions, $\mathop{\mathsf{Exp}}$, as defined by the following grammar:

[TABLE]

The algebraic notation on the left is more convenient when manipulating terms, while the notation on the right may be more intuitive when writing programs. We often abbreviate $e\cdot f$ by $ef$, and omit parentheses following standard conventions, e.g., writing $bc+d$ instead of $(bc)+d$ and $ef^{(b)}$ instead of $e(f^{(b)})$.

2.2. Semantics: Language Model

Intuitively, we interpret a GKAT expression as the set of “legal” execution traces it induces, where a trace is legal if no assertion fails. To make this formal, let $b\equiv_{\text{BA}}c$ denote Boolean equivalence. Entailment is a preorder on the set of Boolean expressions, $\mathsf{BExp}$, and can be characterized in terms of equivalence as follows: $b\leq c\iff b+c\equiv_{\text{BA}}c$. In the quotient set $\mathsf{BExp}/\equiv_{\text{BA}}$ (the free Boolean algebra on generators $T=\{t_{1},\dots,t_{n}\}$), entailment is a partial order ${[b]}_{\equiv_{\text{BA}}}\leq{[c]}_{\equiv_{\text{BA}}}~{}\mathrel{\vcentcolon\Longleftrightarrow}~{}b+c\equiv_{\text{BA}}c$, with minimum and maximum elements given by the equivalence classes of [math] and $1$, respectively. The minimal nonzero elements of this order are called atoms. We let $\mathsf{At}$ denote the set of atoms and use lowercase Greek letters $\alpha,\beta,\dots$ to denote individual atoms. Each atom is the equivalence class of an expression of the form $c_{1}\cdot c_{2}\cdots c_{n}\in\mathsf{BExp}$ with $c_{i}\in\{t_{i},\overline{t_{i}}\}$. Thus we can think of each atom as representing a truth assignment on $T$, e.g., if $c_{i}=t_{i}$ then $t_{i}$ is set to true, otherwise if $c_{i}=\overline{t_{i}}$ then $t_{i}$ is set to false. Likewise, the set $\{\alpha\in\mathsf{At}\mid\alpha\leq b\}$ can be thought of as the set of truth assignments where $b$ evaluates to true; $\equiv_{\text{BA}}$ is complete with respect to this interpretation in that two Boolean expressions are related by $\equiv_{\text{BA}}$ if and only if their atoms coincide (Birkhoff and Bartee, 1970).

A guarded string is an element of the regular set $\mathsf{GS}\coloneqq\mathsf{At}\cdot{(\Sigma\cdot\mathsf{At})}^{*}$. Intuitively, a non-empty string $\alpha_{0}p_{1}\alpha_{1}\cdots p_{n}\alpha_{n}\in\mathsf{GS}$ describes a trace of an abstract program: the atoms $\alpha_{i}$ describe the state of the system at various points in time, starting from an initial state $\alpha_{0}$ and ending in a final state $\alpha_{n}$, while the actions $p_{i}\in\Sigma$ are the transitions triggered between the various states. Given two traces, we can combine them sequentially by running one after the other. Formally, guarded strings compose via a partial fusion product $\diamond\colon\mathsf{GS}\times\mathsf{GS}\rightharpoonup\mathsf{GS}$, defined for $x,y\in{(\mathsf{At}\cup\Sigma)}^{*}$ as

[TABLE]

This product lifts to a total function on languages $L,K\subseteq\mathsf{GS}$ of guarded strings, given by

[TABLE]

We need a few more constructions before we can interpret GKAT expressions as languages representing their possible traces. First, $2^{\mathsf{GS}}$ with the fusion product forms a monoid with identity $\mathsf{At}$ and so we can define the $n$-th power $L^{n}$ of a language $L$ inductively in the usual way:

[TABLE]

Second, in the special case where $B\subseteq\mathsf{At}$, we write $\overline{B}$ for $\mathsf{At}-B$ and define:

[TABLE]

We are now ready to interpret GKAT expressions as languages of guarded strings via the semantic map $\llbracket-\rrbracket~{}\colon~{}\mathop{\mathsf{Exp}}\to 2^{\mathsf{GS}}$ as follows:

[TABLE]

We call this the language model of GKAT. Since we make no assumptions about the semantics of actions, we interpret them as sets of traces beginning and ending in arbitrary states; this soundly overapproximates the behavior of any instantiation. A test is interpreted as the set of states satisfying the test. The traces of $e\cdot f$ are obtained by composing traces from $e$ with traces from $f$ in all possible ways that make the final state of an $e$-trace match up with the initial state of an $f$-trace. The traces of $e+_{b}f$ collect traces of $e$ and $f$, restricting to $e$-traces whose initial state satisfies $b$ and $f$-traces whose initial state satisfies $\overline{b}$. The traces of $e^{(b)}$ are obtained by sequentially composing zero or more $be$-traces and selecting traces ending in a state satisfying $\overline{b}$.

Remark 2.1 (Connection to KAT).

The expressions for KAT, denoted $\mathsf{KExp}$, are generated by the same grammar as for GKAT, except that KAT’s union ($+$) replaces GKAT’s guarded union ($+_{b}$) and KAT’s iteration ($e^{*}$) replaces GKAT’s guarded iteration ($e^{(b)}$). GKAT’s guarded operators can be encoded in KAT; this encoding, which goes back to early work on Propositional Dynamic Logic (Fischer and Ladner, 1979), is the standard method to model conditionals and while loops:

[TABLE]

Thus, there is a homomorphism $\varphi\colon\mathop{\mathsf{Exp}}\to\mathsf{KExp}$ from GKAT to KAT expressions. We inherit KAT’s language model (Kozen and Smith, 1996), $\mathcal{K}\llbracket-\rrbracket\colon\mathsf{KExp}\to 2^{\mathsf{GS}}$, in the sense that $\llbracket-\rrbracket=\mathcal{K}\llbracket-\rrbracket\circ\varphi$.

The languages denoted by GKAT programs satisfy an important property:

Definition 2.2 (Determinacy property).

A language of guarded strings $L\subseteq\mathsf{GS}$ satisfies the determinacy property if, whenever string $x,y\in L$ agree on their first $n$ atoms, then they agree on their first $n$ actions (or lack thereof). For example, $\{\alpha p\gamma,\alpha p\delta,\beta q\delta\}$ and $\{\alpha p\gamma,\beta\}$ for $\alpha\neq\beta$ satisfy the determinacy property, while $\{\alpha p\beta,\alpha\}$ and $\{\alpha p\beta,\alpha q\delta\}$ for $p\neq q$ do not.

We say that two expressions $e$ and $f$ are equivalent if they have the same semantics—i.e., if $\llbracket e\rrbracket=\llbracket f\rrbracket$. In the following sections, we show that this notion of equivalence

• •

is sound and complete for relational and probabilistic interpretations (§ 2.3 and 2.4),

• •

can be finitely and equationally axiomatized in a sound (§ 3) and complete (§ 6) way, and

• •

is efficiently decidable in time nearly linear in the sizes of the expressions (§ 4 and 5).

2.3. Relational Model

This subsection gives an interpretation of GKAT expressions as binary relations, a common model of input-output behavior for many programming languages. We show that the language model is sound and complete for this interpretation. Thus GKAT equivalence implies program equivalence for any programming language with a suitable relational semantics.

Definition 2.3 (Relational Interpretation).

Let $i=(\mathsf{State},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ be a triple consisting of

• •

a set of states $\mathsf{State}$,

• •

for each action $p\in\Sigma$, a binary relation $\operatorname{\mathsf{eval}}(p)\subseteq\mathsf{State}\times\mathsf{State}$, and

• •

for each primitive test $t\in T$, a set of states $\operatorname{\mathsf{sat}}(t)\subseteq\mathsf{State}$.

Then the relational interpretation of an expression $e$ with respect to $i$ is the smallest binary relation $\mathcal{R}_{i}\llbracket e\rrbracket\subseteq\mathsf{State}\times\mathsf{State}$ satisfying the following rules,

[TABLE]

where $\operatorname{\mathsf{sat}}^{\dagger}:\mathsf{BExp}\to 2^{\mathsf{State}}$ is the usual lifting of $\operatorname{\mathsf{sat}}:T\to 2^{\mathsf{State}}$ to Boolean expression over $T$.

The rules defining $\mathcal{R}_{i}\llbracket e\rrbracket$ are reminiscent of the big-step semantics of imperative languages, which arise as instances of the model for various choices of $i$. The following result says that the language model from the previous section abstracts the various relational interpretations in a sound and complete way. It was first proved for KAT by Kozen and Smith (1996).

Theorem 2.4.

The language model is sound and complete for the relational model:

[TABLE]

It is worth noting that Theorem 2.4 also holds for refinement (i.e., with $\subseteq$ instead of $=$).

Example 2.5 (IMP).

Consider a simple imperative programming language IMP with variable assignments and arithmetic and boolean expressions:

[TABLE]

IMP can be modeled in GKAT using actions for assignments and primitive tests for comparisons,111Technically, we can only reserve a test for a finite subset of comparisons, as $T$ is finite. However, for reasoning about pairwise equivalences of programs, which only contain a finite number of comparisons, this restriction is not essential.

[TABLE]

and interpreting GKAT expressions over the state space of variable assignments $\mathsf{State}\coloneq\mathsf{Var}\to\mathbb{Z}$:

[TABLE]

where $\mathcal{A}\llbracket a\rrbracket:\mathsf{State}\to\mathbb{Z}$ denotes arithmetic evaluation. Sequential composition, conditionals, and while loops in IMP are modeled by their GKAT counterparts; $\boldsymbol{\mathsf{skip}}$ is modeled by $1$. Thus, IMP equivalence refines GKAT equivalence (Theorem 2.4). For example, the program transformation

[TABLE]

is sound by the equivalence $pq+_{b}q\equiv(p+_{b}1)\cdot q$. We study such equivalences further in Section 3.

2.4. Probabilistic Model

In this subsection, we give a third interpretation of GKAT expressions in terms of sub-Markov kernels, a common model for probabilistic programming languages (PPLs). We show that the language model is sound and complete for this model as well.

We briefly review some basic primitives commonly used in the denotational semantics of PPLs. For a countable set222We restrict to countable state spaces (i.e., discrete distributions) for ease of presentation, but this assumption is not essential. Appendix D for a more general version using measure theory and Lebesgue integration. $X$, we let $\operatorname{\mathcal{D}}(X)$ denote the set of subdistributions over $X$, i.e., the set of probability assignments $f:X\to[0,1]$ summing up to at most $1$—i.e., $\sum_{x\in X}f(x)\leq 1$. A common distribution is the Dirac distribution or point mass on $x\in X$, denoted $\delta_{x}\in\operatorname{\mathcal{D}}(X)$; it is the map $y\mapsto[y=x]$ assigning probability $1$ to x, and probability [math] to $y\neq x$. (The Iverson bracket $[\varphi]$ is defined to be $1$ if the statement $\varphi$ is true, and [math] otherwise.) Denotational models of PPLs typically interpret programs as Markov kernels, maps of type $X\to\operatorname{\mathcal{D}}(X)$. Such kernels can be composed in sequence using Kleisli composition, since $\operatorname{\mathcal{D}}(-)$ is a monad (Giry, 1982).

Definition 2.6 (Probabilistic Interpretation).

Let $i=(\mathsf{State},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ be a triple consisting of

• •

a countable set of states $\mathsf{State}$;

• •

for each action $p\in\Sigma$, a sub-Markov kernel $\operatorname{\mathsf{eval}}(p)\colon\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$; and

• •

for each primitive test $t\in T$, a set of states $\operatorname{\mathsf{sat}}(t)\subseteq\mathsf{State}$.

Then the probabilistic interpretation of an expression $e$ with respect to $i$ is the sub-Markov kernel $\mathcal{P}_{i}\llbracket e\rrbracket\colon\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ defined as follows:

[TABLE]

The proofs that the limit exists and that $\mathcal{P}_{i}\llbracket e\rrbracket$ is sub-Markov for all $e$ can be found in Lemma A.1.

Theorem 2.7.

The language model is sound and complete for the probabilistic model:

[TABLE]

Proof Sketch.

By mutual implication.

• $\Rightarrow$:

For soundness, we define a map $\kappa_{i}\colon\mathsf{GS}\to\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ from guarded strings to sub-Markov kernels:

[TABLE]

We then lift $\kappa_{i}$ to languages via pointwise summation, $\kappa_{i}(L)\coloneqq\sum_{w\in L}\kappa_{i}(w)$, and establish that any probabilistic interpretation factors through the language model via $\kappa_{i}$: $\mathcal{P}_{i}\llbracket-\rrbracket=\kappa_{i}\circ\llbracket-\rrbracket$.

• $\Leftarrow$:

For completeness, we construct an interpretation $i\coloneqq(\mathsf{GS},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ over $\mathsf{GS}$ as follows,

[TABLE]

and show that $\llbracket e\rrbracket$ is fully determined by $\mathcal{P}_{i}\llbracket e\rrbracket$:

[TABLE]

As for Theorem 2.4, Theorem 2.7 can also be shown for refinement (i.e., with $\subseteq$ and $\leq$ instead of $=$).

Example 2.8 (Probabilistic IMP).

We can extend IMP from Example 2.5 with a probabilistic assignment command $x\sim\mu$, where $\mu$ ranges over sub-distributions on $\mathbb{Z}$, as follows:

[TABLE]

The interpretation $i=(\mathsf{Var}\to\mathbb{Z},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ is as before, except we now restrict to a finite set of variables to guarantee that the state space is countable, and interpret actions as sub-Markov kernels:

[TABLE]

A concrete example of a PPL based on GKAT is McNetKAT (Smolka et al., 2019), a recent language and verification tool for reasoning about the packet-forwarding behavior in networks.

3. Axiomatization

In most programming languages, the same behavior can be realized using different programs. For example, we expect the programs $\boldsymbol{\mathsf{if}}~{}b~{}\boldsymbol{\mathsf{then}}~{}e~{}\boldsymbol{\mathsf{else}}~{}f$ and $\boldsymbol{\mathsf{if}}~{}(\boldsymbol{\mathsf{not}}~{}b)~{}\boldsymbol{\mathsf{then}}~{}f~{}\boldsymbol{\mathsf{else}}~{}e$ to encode the same behavior. Likewise, different expressions in GKAT can denote the same language of guarded strings. For instance, the previous example is reflected in GKAT by the fact that the language semantics of $e+_{b}f$ and $f+_{\overline{b}}e$ coincide. This raises the questions: what other equivalences hold between GKAT expressions? And, can all equivalences be captured by a finite number of equations? In this section, we give some initial answers to these questions, by proposing a set of axioms for GKAT and showing that they can be used to prove a large class of equivalences.

3.1. Some Simple Axioms

As an initial answer to the first question, we propose the following.

Definition 3.1.

We define $\equiv$ as the smallest congruence (with respect to all operators) on $\mathop{\mathsf{Exp}}$ that satisfies the axioms given in Figure 1 (for all $e,f,g\in\mathop{\mathsf{Exp}}$ and $b,c,d\in\mathsf{BExp}$) and subsumes Boolean equivalence in the sense that $b\equiv_{\text{BA}}c$ implies $b\equiv c$.

The guarded union axioms (LABEL:ax:idemp-LABEL:ax:rightdistr) can be understood intuitively in terms of conditionals. For instance, we have the law $e+_{b}f\equiv f+_{\overline{b}}e$ discussed before, but also $eg+_{b}fg\equiv(e+_{b}f)\cdot g$, which says that $g$ can be “factored out” of branches of a guarded union. Equivalences for sequential composition are also intuitive. For instance, $0\cdot e\equiv 0$ encodes that any instruction after failure is irrelevant, because the program has failed. The axioms for loops (LABEL:ax:unroll–LABEL:ax:fixpoint) are more subtle. The axiom $e^{(b)}\equiv ee^{(b)}+_{b}1$ (LABEL:ax:unroll) says that we can think of a guarded loop as equivalent to its unrolling—i.e., the program $\boldsymbol{\mathsf{while}}\ b\ \boldsymbol{\mathsf{do}}\ e$ has the same behavior as the program $\boldsymbol{\mathsf{if}}\ b\ \boldsymbol{\mathsf{then}}\ (e;\ \boldsymbol{\mathsf{while}}\ b\ \boldsymbol{\mathsf{do}}\ e)\ \boldsymbol{\mathsf{else}}\ \boldsymbol{\mathsf{skip}}$. The axiom ${(e+_{c}1)}^{(b)}\equiv{(ce)}^{(b)}$ (LABEL:ax:tighten) states that if part of a loop body does not have an effect (i.e., is equivalent to $\boldsymbol{\mathsf{skip}}$), it can be omitted; we refer to this transformation as loop tightening.

To explain the fixpoint axiom (LABEL:ax:fixpoint), disregard the side-condition for a moment. In a sense, this rule states that if $g$ tests (using $b$) whether to execute $e$ and loop again or execute $f$ (i.e., if $g\equiv eg+_{b}f$) then $g$ is a $b$-guarded loop followed by $f$ (i.e., $g\equiv e^{(b)}f$). However, such a rule is not sound in general. For instance, suppose $e,f,g,b=1$; in that case, $1\equiv 1\cdot 1+_{1}1$ can be proved using the other axioms, but applying the rule would allow us to conclude that $1\equiv 1^{(1)}\cdot 1$, even though $\llbracket 1\rrbracket=\mathsf{At}$ and $\llbracket 1^{(1)}\cdot 1\rrbracket=\varnothing$! The problem here is that, while $g$ is tail-recursive as required by the premise, this self-similarity is trivial because $e$ does not represent a productive program. We thus need to restrict the application of the inference rule to cases where the loop body is strictly productive—i.e., where $e$ is guaranteed to execute some action. To this end, we define the function $E$ as follows.

Definition 3.2.

The function $E:\mathop{\mathsf{Exp}}\to\mathsf{BExp}$ is defined inductively as follows:

[TABLE]

Intuitively, $E(e)$ is the weakest test that guarantees that $e$ terminates successfully, but does not perform any action. For instance, $E(p)$ is [math]—the program $p$ is guaranteed to perform the action $p$. Using $E$, we can now restrict the application of the fixpoint rule to the cases where $E(e)\equiv 0$, i.e., where $e$ performs an action under any circumstance.

Theorem 3.3 (Soundness).

The GKAT axioms are sound for the language model: for all $e,f\in\mathop{\mathsf{Exp}}$,

[TABLE]

Proof Sketch.

By induction on the length of derivation of the congruence $\equiv$. We provide the full proof in the appendix and show just the proof for the fixpoint rule. Here, we should argue that if $E(e)\equiv 0$ and $\llbracket g\rrbracket=\llbracket eg+_{b}f\rrbracket$, then also $\llbracket g\rrbracket=\llbracket e^{(b)}f\rrbracket$. We note that, using soundness of (LABEL:ax:unroll) and (LABEL:ax:rightdistr), we can derive that $\llbracket e^{(b)}f\rrbracket=\llbracket(ee^{(b)}+_{b}1)f\rrbracket=\llbracket ee^{(b)}f+_{b}f\rrbracket$.

We reason by induction on the length of guarded strings. In the base case, we know that $\alpha\in\llbracket g\rrbracket$ if and only if $\alpha\in\llbracket eg+_{b}f\rrbracket$; since $E(e)\equiv 0$, the latter holds precisely when $\alpha\in\llbracket f\rrbracket$ and $\alpha\leq\overline{b}$, which is equivalent to $\alpha\in\llbracket e^{(b)}f\rrbracket$. For the inductive step, suppose the claim holds for $y$; then

[TABLE]

3.2. A Fundamental Theorem

The side condition on (LABEL:ax:fixpoint) is inconvenient when proving facts about loops. However, it turns out that we can transform any loop into an equivalent, productive loop—i.e., one with a loop body $e$ such that $E(e)\equiv 0$. To this end, we need a way of decomposing a GKAT expression into a guarded sum of an expression that describes termination, and another (strictly productive) expression that describes the next steps that the program may undertake. As a matter of fact, we already have a handle on the former term: $E(e)$ is a Boolean term that captures the atoms for which $e$ may halt immediately. It therefore remains to describe the next steps of a program.

Definition 3.4 (Derivatives).

For $\alpha\in\mathsf{At}$ we define $D_{\alpha}\colon\mathop{\mathsf{Exp}}\to 2+\Sigma\times\mathop{\mathsf{Exp}}$ inductively as follows, where $2=\{0,1\}$ is the two-element set:

[TABLE]

We will use a general type of guarded union to sum over an atom-indexed set of expressions.

Definition 3.5.

Let $\Phi\subseteq\mathsf{At}$, and let ${\{e_{\alpha}\}}_{\alpha\in\Phi}$ be a set of expressions indexed by $\Phi$. We write

[TABLE]

Like other operators on indexed sets, we may abuse notation and replace $\Phi$ by a predicate over some atom $\alpha$, with $e_{\alpha}$ a function of $\alpha$; for instance, we could write \operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}}_{\alpha\leq 1}\alpha\equiv 1.

Remark 3.6.

The definition above is ambiguous in the choice of $\beta$. However, because of skew-commutativity (LABEL:ax:skewcomm) and skew-associativity (LABEL:ax:skewassoc), that does not change the meaning of the expression as far as $\equiv$ is concerned. For the details, see Appendix B.

We are now ready to state the desired decomposition of terms. Following (Rutten, 2000; Silva, 2010), we call this the fundamental theorem of GKAT, in reference to the strong analogy with the fundamental theorem of calculus, as explained in (Rutten, 2000; Silva, 2010). The proof is included in Appendix A.

Theorem 3.7 (Fundamental Theorem).

For all GKAT programs $e$, the following equality holds:

[TABLE]

The following observations about $D$ and $E$ are also useful.

Lemma 3.8.

Let $e\in\mathop{\mathsf{Exp}}$; its components $E(e)$ and $D(e)$ satisfy the following identities:

[TABLE]

Using the fundamental theorem and the above, we can now show how to syntactically transform any loop into an equivalent loop whose body $e$ is strictly productive.

Lemma 3.9 (Productive Loop).

Let $e\in\mathop{\mathsf{Exp}}$ and $b\in\mathsf{BExp}$. We have $e^{(b)}\equiv{D(e)}^{(b)}$.

Proof.

Using Lemma 3.8, we derive as follows:

[TABLE]

3.3. Derivable Facts

The GKAT axioms can be used to derive other natural equivalences of programs, such as the ones in Figure 2. For instance, $e^{(b)}\equiv e^{(b)}\overline{b}$, labelled (LABEL:fact:guard-loop-out), says that $b$ must be false when $e^{(b)}$ ends.

Lemma 3.10.

The facts in Figure 2 are derivable from the axioms.

Proof Sketch.

Let us start by showing (LABEL:fact:neutrright2).

[TABLE]

The remaining proofs appear in the appendix. ∎

We conclude our presentation of derivable facts by showing one more interesting fact. Unlike the derived facts above, this one is an implication: if the test $c$ is invariant for the program $e$ given that a test $b$ succeeds, then $c$ is preserved by a $b$-loop on $e$.

Lemma 3.11 (Invariance).

Let $e\in\mathop{\mathsf{Exp}}$ and $b,c\in\mathsf{BExp}$. If $cbe\equiv cbec$, then $ce^{(b)}\equiv{(ce)}^{(b)}c$.

Proof.

We first derive a useful equivalence, as follows:

[TABLE]

This completes the proof. ∎

3.4. A Limited Form of Completeness

Above, we considered a number of axioms that were proven sound with respect to the language model. Ultimately, we would like to show the converse, i.e., that these axioms are sufficient to prove all equivalences between programs, meaning that whenever $\llbracket e\rrbracket=\llbracket f\rrbracket$, it also holds that $e\equiv f$.

We return to this general form of completeness in Section 6, when we can rely on the coalgebraic theory of GKAT developed in Sections 4 and 5. At this point, however, we can already prove a special case of completeness related to Hoare triples. Suppose $e$ is a GKAT program, and $b$ and $c$ are Boolean expressions encoding pre- and postconditions. The equation $\llbracket be\rrbracket=\llbracket bec\rrbracket$ states that every finite, terminating run of $e$ starting from a state satisfying $b$ concludes in a state satisfying $c$. The following states that all valid Hoare triples of this kind can be established axiomatically:

Theorem 3.12 (Hoare completeness).

Let $e\in\mathop{\mathsf{Exp}}$, $b,c\in\mathsf{BExp}$. If $\llbracket bec\rrbracket=\llbracket be\rrbracket$, then $bec\equiv be$.

Proof Sketch.

By induction on $e$. We show only the case for while loops and defer the full proof to Appendix A.

If $e=e_{0}^{(d)}$, first note that if $b\equiv 0$, then the claim follows trivially. For $b\not\equiv 0$, let

[TABLE]

We make the following observations.

1. (i)

Since $b\not\equiv 0$, we have that $\llbracket b\rrbracket\diamond\llbracket{de_{0}}\rrbracket^{0}\diamond\llbracket b\rrbracket=\llbracket b\rrbracket\neq\varnothing$, and thus $b\leq h$. 2. (ii)

If $\alpha\leq h\overline{d}$, then in particular $\gamma{}w\alpha\in\llbracket b\rrbracket\diamond\llbracket de_{0}\rrbracket^{n}\diamond\llbracket\alpha\rrbracket$ for some $n$ and $\gamma{}w$. Since $\alpha\leq\overline{d}$, it follows that $\gamma{}w\alpha\in\llbracket be_{0}^{(d)}\rrbracket=\llbracket be_{0}^{(d)}c\rrbracket$, and thus $\alpha\leq c$. Consequently, $h\overline{d}\leq c$. 3. (iii)

If $\alpha{}w\beta\in\llbracket dhe_{0}\rrbracket$, then $\alpha\leq h$ and hence there exists an $n$ such that $\gamma{}x\alpha\in\llbracket b\rrbracket\diamond\llbracket de_{0}\rrbracket^{n}\diamond\llbracket\beta\rrbracket$. But then $\gamma{}x\alpha{}w\beta\in\llbracket b\rrbracket\ \diamond\llbracket de_{0}\rrbracket^{n+1}\diamond\llbracket\beta\rrbracket$, and therefore $\beta\leq h$. We can conclude that $\llbracket dhe_{0}\rrbracket=\llbracket dhe_{0}h\rrbracket$; by induction, it follows that $dhe_{0}h\equiv dhe_{0}$.

Using these observations and the invariance lemma (Lemma 3.11), we derive

[TABLE]

This completes the proof. ∎

As a special case, the fact that a program has no traces at all can be shown axiomatically.

Corollary 3.13 (Partial Completeness).

If $\llbracket e\rrbracket=\varnothing$, then $e\equiv 0$.

Proof.

We have $\llbracket 1\cdot e\rrbracket=\llbracket e\rrbracket=\varnothing=\llbracket 1\cdot e\cdot 0\rrbracket$, and thus $e\equiv 1\cdot e\equiv 1\cdot e\cdot 0\equiv 0$ by Theorem 3.12. ∎

We will return to deriving a general completeness result in Section 6. This will rely on the coalgebraic theory of GKAT, which we develop next (Sections 4 and 5).

4. Automaton Model and Kleene Theorem

In this section, we present an automaton model that accepts traces (i.e., guarded strings) of GKAT programs. We then present language-preserving constructions from GKAT expressions to automata, and conversely, from automata to expressions. Our automaton model is rich enough to express programs that go beyond GKAT; in particular, it can encode traces of programs with goto statements that have no equivalent GKAT program (Kozen and Tseng, 2008). In order to obtain a Kleene Theorem for GKAT, that is, a correspondence between automata and GKAT programs, we identify conditions ensuring that the language accepted by an automaton corresponds to a valid GKAT program.

4.1. Automata and Languages

Let $G$ be the functor $GX={(2+\Sigma\times X)}^{\mathsf{At}}$, where $2=\{0,1\}$ is the two-element set. A $G$-coalgebra is a pair $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ with state space $X$ and transition map $\delta^{\mathcal{X}}\colon X\to GX$. The outcomes $1$ and [math] model immediate acceptance and rejection, respectively. From each state $s\in X$, given an input $\alpha\in\mathsf{At}$, the coalgebra performs exactly one of three possible actions: it either produces an output $p\in\Sigma$ and moves to a new state $t$, halts and accepts, or halts and rejects; that is, either $\delta^{\mathcal{X}}(s)(\alpha)=(p,t)$, or $\delta^{\mathcal{X}}(s)(\alpha)=1$, or $\delta^{\mathcal{X}}(s)(\alpha)=0$.

A $G$-automaton is a $G$-coalgebra with a designated start state $\iota$, commonly denoted as a triple $\mathcal{X}=\langle X,\delta^{\mathcal{X}},\iota\rangle$. We can represent $G$-coalgebras graphically as in Figure 3.

A $G$-coalgebra $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ can be viewed both as an acceptor of finite guarded strings $\mathsf{GS}=\mathsf{At}\cdot{(\Sigma\cdot\mathsf{At})}^{*}$, or as an acceptor of finite and infinite guarded strings $\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$, where $\omega\mathchar 45\relax\mathsf{GS}\coloneqq{(\mathsf{At}\cdot\Sigma)}^{\omega}$. Acceptance for a state $s$ is captured by the following equivalences:

[TABLE]

The language of finite guarded strings $\ell^{\mathcal{X}}(s)\subseteq GS$ accepted from state $s\in X$ is the least fixpoint solution of the above system; in other words, we interpret (2) inductively. The language of finite and infinite guarded strings $L^{\mathcal{X}}(s)\subseteq\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ accepted from state $s$ is the greatest fixpoint solution of the above system; in other words, we interpret (2) coinductively.333The set $\mathcal{F}$ of maps $F\colon X\to 2^{\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}}$ ordered pointwise by subset inclusion forms a complete lattice. The monotone map

$\displaystyle\tau\colon\mathcal{F}\to\mathcal{F},\,\tau(F)=\lambda s\in X\kern 1.0pt.\kern 1.0pt\{\alpha\in\mathsf{At}\mid\delta^{\mathcal{X}}(s)(\alpha)=1\}\cup\{apx\mid\exists t.\;\delta^{\mathcal{X}}(s)(\alpha)=(p,t)\land x\in F(t)\}$

arising from (2) has least and greatest fixpoints, $\ell^{\mathcal{X}}$ and $L^{\mathcal{X}}$, by the Knaster-Tarksi theorem.

The two languages are related by the equation $\ell^{\mathcal{X}}(s)=L^{\mathcal{X}}(s)\cap\mathsf{GS}$. Our focus will mostly be on the finite-string semantics, $\ell^{\mathcal{X}}(-)\colon X\to 2^{\mathsf{GS}}$, since GKAT expressions denote finite-string languages, $\llbracket-\rrbracket\colon\mathop{\mathsf{Exp}}\to 2^{\mathsf{GS}}$.

The language accepted by a $G$-automaton $\mathcal{X}=\langle X,\delta^{X},\iota\rangle$ is the language accepted by its initial state $\iota$. Just like the language model for GKAT programs, the language semantics of a $G$-automaton satisfies the determinacy property (see Definition 2.2). In fact, every language that satisfies the determinacy property can be recognized by a $G$-automaton, possibly with infinitely many states. (We will prove this formally in Theorem 5.8.)

4.2. Expressions to Automata: a Thompson Construction

We translate expressions to $G$-coalgebras using a construction reminiscent of Thompson’s construction for regular expressions (Thompson, 1968), where automata are formed by induction on the structure of the expressions and combined to reflect the various GKAT operations.

We first set some notation. A pseudostate is an element $h\in GX$. We let $\mathbf{1}\in GX$ denote the pseudostate $\mathbf{1}(\alpha)=1$, i.e., the constant function returning $1$. Let $\mathcal{X}=\langle X,\delta\rangle$ be a $G$-coalgebra. The uniform continuation of $Y\subseteq X$ by $h\in GX$ (in $\mathcal{X}$) is the coalgebra $\mathcal{X}[Y,h]\coloneqq\langle X,\delta[Y,h]\rangle$, where

[TABLE]

Intuitively, uniform continuation replaces termination of states in a region $Y$ of $\mathcal{X}$ by a transition described by $h\in GX$; this construction will be useful for modeling operations that perform some kind of sequencing. Figure 5 schematically describes the uniform continuation operation, illustrating different changes to the automaton that can occur as a result; observe that since $h$ may have transitions into $Y$, uniform continuation can introduce loops.

We will also need coproducts to combine coalgebras. Intuitively, the coproduct of two coalgebras is just the juxtaposition of both coalgebras. Formally, for $\mathcal{X}=\langle X,\delta_{1}\rangle$ and $\mathcal{Y}=\langle Y,\delta_{2}\rangle$, we write the coproduct as $\mathcal{X}+\mathcal{Y}=\langle X+Y,\delta_{1}+\delta_{2}\rangle$, where $X+Y$ is the disjoint union of $X$ and $Y$, and $\delta_{1}+\delta_{2}\colon X+Y\to G(X+Y)$ is the map that applies $\delta_{1}$ to states in $X$ and $\delta_{2}$ to states in $Y$.

Figure 4 presents our translation from expressions $e$ to coalgebras $\mathcal{X}_{e}$ using coproducts and uniform continuations, and Figure 6 sketches the transformations used to construct the automaton of a term from its subterms. We model initial states as pseudostates, rather than proper states. This trick avoids the $\varepsilon$-transitions that appear in the classical Thompson construction and yields compact, linear-size automata. Figure 7 depicts some examples of our construction.

To turn the resulting coalgebra into an automaton, we simply convert the initial pseudostate into a proper state. Formally, when $\mathcal{X}_{e}=\langle X_{e},\delta_{e}\rangle$, we write $\mathcal{X}_{e}^{\iota}$ for the $G$-automaton $\langle\{\iota\}+X_{e},\delta^{\iota}_{e},\iota\rangle$, where for $x\in X_{e}$, we set $\delta^{\iota}_{e}(x)=\delta_{e}(x)$ as well as $\delta_{e}^{\iota}(\iota)=\iota_{e}$. We call $\mathcal{X}_{e}$ and $\mathcal{X}_{e}^{\iota}$ the Thompson coalgebra and Thompson automaton for $e$, respectively.

The construction translates expressions to equivalent automata in the following sense:

Theorem 4.1 (Correctness I).

The Thompson automaton for $e$ recognizes $\llbracket e\rrbracket$, that is $\ell^{\mathcal{X}_{e}^{\iota}}(\iota)=\llbracket e\rrbracket$.

Proof Sketch.

This is a direct corollary of Propositions 4.5 and 4.8, to follow. ∎

Moreover, the construction is efficiently implementable and yields small automata:

Proposition 4.2.

The Thompson automaton for $e$ is effectively constructible in time $\mathcal{O}(|e|)$ and has $\#_{\Sigma}(e)+1$ (thus, $\mathcal{O}(|e|)$) states, where $|\mathsf{At}|$ is considered a constant for the time complexity claim, $|e|$ denotes the size of the expression, and $\#_{\Sigma}(e)$ denotes the number of occurrences of actions in $e$.

4.3. Automata to Expressions: Solving Linear Systems

The previous construction shows that every GKAT expression can be translated to an equivalent G-automaton. In this section we consider the reverse direction, from G-automata to GKAT expressions. The main idea is to interpret the coalgebra structure as a system of equations, with one variable and equation per state, and show that there are GKAT expressions solving the system, modulo equivalence; this idea goes back to Conway (1971) and Backhouse (1975). Not all systems arising from G-coalgebras have a solution, and so not all G-coalgebras can be captured by GKAT expressions. However, we identify a subclass of G-coalgebras that can be represented as GKAT terms. By showing that this class contains the coalgebras produced by our expressions-to-automata translation, we obtain an equivalence between GKAT expressions and coalgebras in this class.

We start by defining when a map assigning expressions to coalgebra states is a solution.

Definition 4.3 (Solution).

Let $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ be a $G$-coalgebra. We say that $s\colon X\to\mathop{\mathsf{Exp}}$ is a solution to $\mathcal{X}$ if for all $x\in X$ it holds that

[TABLE]

Example 4.4.

Consider the Thompson automata in Figure 7.

1. (a)

Solving the first automaton requires, by Definition 4.3, finding an expression $s_{e}(*_{p})$ such that $s_{e}(*_{p})\equiv p\cdot s_{e}(*_{p})+_{b}1$. By (LABEL:ax:unroll), we know that $s_{e}(*_{p})=p^{(b)}$ is valid; in fact, (LABEL:ax:fixpoint) tells us that this choice of $x$ is the only valid solution up to GKAT-equivalence. If we include $\iota_{e}$ as a state, we can choose $s_{e}(\iota_{e})=p^{(b)}$ as well. 2. (b)

The second automaton has an easy solution: both $*_{q}$ and $*_{r}$ are solved by setting $s_{f}(*_{q})=s_{f}(*_{r})=1$. If we include $\iota_{f}$ as a state, we can choose $s_{f}(\iota_{f})=q\cdot s_{f}(*_{q})+_{b}r\cdot s_{f}(*_{r})\equiv q+_{b}r$. 3. (c)

The third automaton was constructed from the first two; similarly, we can construct its solution from the solutions to the first two. We set $s_{g}(*_{p})=s_{e}(*_{p})\cdot s_{f}(\iota_{f})$, and $s_{g}(*_{q})=s_{f}(*_{q})$, and $s_{g}(*_{r})=s_{f}(*_{r})$. If we include $\iota_{g}$ as a state, we can choose $s_{g}(\iota_{g})=s_{e}(\iota_{e})\cdot s_{f}(\iota_{f})$.

Solutions are language-preserving maps from states to expressions in the following sense:

Proposition 4.5.

If $s$ solves $\mathcal{X}$ and $x$ is a state, then $\llbracket s(x)\rrbracket=\ell^{\mathcal{X}}(x)$.

Proof Sketch.

Show that $w\in\llbracket s(x)\rrbracket\Leftrightarrow w\in\ell^{\mathcal{X}}(x)$ by induction on the length of $w\in\mathsf{GS}$. ∎

We would like to build solutions for $G$-coalgebras, but Kozen and Tseng (2008) showed that this is not possible in general: there is a 3-state $G$-coalgebra that does not correspond to any $\boldsymbol{\mathsf{while}}$ program, but instead can only be modeled by a program with multi-level breaks. In order to obtain an exact correspondence to GKAT programs, we first identify a sufficient condition for $G$-coalgebras to permit solutions, and then show that the Thompson coalgebra defined previously meets this condition.

Definition 4.6 (Well-nested Coalgebra).

Let $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ and $\mathcal{Y}=\langle Y,\delta^{\mathcal{Y}}\rangle$ range over $G$-coalgebras. The collection of well-nested coalgebras is inductively defined as follows:

1. (i)

If $\mathcal{X}$ has no transitions, i.e., if $\delta^{\mathcal{X}}\in X\to 2^{\mathsf{At}}$, then $\mathcal{X}$ is well-nested. 2. (ii)

If $\mathcal{X}$ and $\mathcal{Y}$ are well-nested and $h\in G(X+Y)$, then $(\mathcal{X}+\mathcal{Y})[X,h]$ is well-nested.

We are now ready to construct solutions to well-nested coalgebras.

Theorem 4.7 (Existence of Solutions).

Any well-nested coalgebra admits a solution.

Proof Sketch.

Assume $\mathcal{X}$ is well-nested. We proceed by rule induction on the well-nestedness derivation.

1. (i)

Suppose $\delta^{\mathcal{X}}\colon X\to 2^{\mathsf{At}}$. Then

[TABLE]

is a solution to $\mathcal{X}$. 2. (ii)

Let $\mathcal{Y}=\langle Y,\delta^{\mathcal{Y}}\rangle$ and $\mathcal{Z}=\langle Z,\delta^{\mathcal{Z}}\rangle$ be well-nested $G$-coalgebras, and let $h\in G(Y+Z)$ be such that $\mathcal{X}=(\mathcal{Y}+\mathcal{Z})[Y,h]$. By induction, $\mathcal{Y}$ and $\mathcal{Z}$ admit solutions $s^{\mathcal{Y}}$ and $s^{\mathcal{Z}}$ respectively; we need to find a solution $s^{\mathcal{X}}$ to $X=Y+Z$. The idea is to retain the solution that we had for states in $\mathcal{Z}$—whose behavior has not changed under uniform continuation—while modifying the solution to states in $\mathcal{Y}$ in order to account for transitions from $h$. To this end, we choose the following expressions:

[TABLE]

We can then define $s$ by setting $s(x)=s^{\mathcal{Y}}(x)\cdot\ell$ for $x\in Y$, and $s(x)=s^{\mathcal{Z}}(x)$ for $x\in Z$. A detailed argument showing that $s$ is a solution can be found in the appendix. ∎

As it turns out, we can do a round-trip, showing that the solution to the (initial state of the) Thompson automaton for an expression is equivalent to the original expression.

Theorem 4.8 (Correctness II).

Let $e\in\mathop{\mathsf{Exp}}$. Then $\mathcal{X}_{e}^{\iota}$ admits a solution $s$ such that $e\equiv s(\iota)$.

Finally, we show that the automata construction of the previous section gives well-nested automata.

Theorem 4.9 (well-nestedness of Thompson construction).

$\mathcal{X}_{e}$* and $\mathcal{X}_{e}^{\iota}$ are well-nested for all expressions $e$.*

Proof.

We proceed by induction on $e$. In the base, let $\mathcal{Z}=\langle\varnothing,\varnothing\rangle$ and $\mathcal{I}=\langle\{*\},*\mapsto\bf{1}\rangle$ denote the coalgebras with no states and with a single all-accepting state, respectively. Note that $\mathcal{Z}$ and $\mathcal{I}$ are well-nested, and that for $b\in\mathsf{BExp}$ and $p\in\Sigma$ we have $\mathcal{X}_{b}=\mathcal{Z}$ and $\mathcal{X}_{p}=\mathcal{I}$.

All of the operations used to build $\mathcal{X}_{e}$, as detailed in Figure 4, can be phrased in terms of an appropriate uniform continuation of a coproduct; for instance, when $e=f^{(b)}$ we have that $\mathcal{X}_{e}=(\mathcal{X}_{f}+\mathcal{I})[X_{f},\iota_{e}]$. Consequently, the Thompson automaton $\mathcal{X}_{e}$ is well-nested by construction. Finally, observe that $\mathcal{X}_{e}^{\iota}=(\mathcal{I}+\mathcal{X}_{e})[\{*\},\iota_{e}]$; hence, $\mathcal{X}_{e}^{\iota}$ is well-nested as well. ∎

Theorems 4.1, 4.7 and 4.9 now give us the desired Kleene theorem.

Corollary 4.10 (Kleene Theorem).

Let $L\subseteq\mathsf{GS}$. The following are equivalent:

1. (1)

$L=\llbracket e\rrbracket$* for a GKAT expression $e$.* 2. (2)

$L=\ell^{\mathcal{X}}(\iota)$* for a well-nested, finite-state $G$-automaton $\mathcal{X}$ with initial state $\iota$.*

5. Decision procedure

We saw in the last section that GKAT expressions can be efficiently converted to equivalent automata with a linear number of states. Equivalence of automata can be established algorithmically, supporting a decision procedure for GKAT that is significantly more efficient than decision procedures for KAT. In this section, we describe our algorithm.

First, we define bisimilarity of automata states in the usual way (Kozen and Tseng, 2008).

Definition 5.1 (Bisimilarity).

Let $\mathcal{X}$ and $\mathcal{Y}$ be $G$-coalgebras. A bisimulation between $\mathcal{X}$ and $\mathcal{Y}$ is a binary relation ${R}\subseteq X\times Y$ such that if $x\mathrel{R}y$, then the following implications hold:

1. (i)

if $\delta^{\mathcal{X}}(x)(\alpha)\in 2$, then $\delta^{\mathcal{Y}}(y)(\alpha)=\delta^{\mathcal{X}}(x)(\alpha)$; and 2. (ii)

if $\delta^{\mathcal{X}}(x)(\alpha)=(p,x^{\prime})$, then $\delta^{\mathcal{Y}}(y)(\alpha)=(p,y^{\prime})$ and $x^{\prime}\mathrel{R}y^{\prime}$ for some $y^{\prime}$.

States $x$ and $y$ are called bisimilar, denoted $x\sim y$, if there exists a bisimulation relating $x$ and $y$.

As usual, we would like to reduce automata equivalence to bisimilarity. It is easy to see that bisimilar states recognize the same language.

Lemma 5.2.

If $\mathcal{X}$ and $\mathcal{Y}$ are G-coalgebras with bisimilar states $x\sim y$, then $\ell^{\mathcal{X}}(x)=\ell^{\mathcal{Y}}(y)$.

Proof.

We verify that $w\in\ell^{\mathcal{X}}(x)\Leftrightarrow w\in\ell^{\mathcal{Y}}(y)$ by induction on the length of $w\in\mathsf{GS}$:

• •

For $\alpha\in\mathsf{GS}$, we have $\alpha\in\ell^{\mathcal{X}}(x)\Leftrightarrow\delta^{\mathcal{X}}(x)(\alpha)=1\Leftrightarrow\delta^{\mathcal{Y}}(y)(\alpha)=1\Leftrightarrow\alpha\in\ell^{\mathcal{Y}}(y)$.

• •

For $\alpha pw\in\mathsf{GS}$, we use bisimilarity and the induction hypothesis to derive

[TABLE]

The converse direction, however, does not hold for $G$-coalgebras in general. To see the problem, consider the following automaton, where $\alpha\in\mathsf{At}$ is an atom and $p\in\Sigma$ is an action:

[TABLE]

Both states recognize the empty language, that is i.e., $\ell(s_{1})=\ell(s_{2})=\varnothing$; but $s_{2}$ rejects immediately, whereas $s_{1}$ may first take a transition. As a result, $s_{1}$ and $s_{2}$ are not bisimilar. Intuitively, the language accepted by a state does not distinguish between early and late rejection, whereas bisimilarity does. We solve this by disallowing late rejection, i.e., transitions that can never lead to an accepting state; we call coalgebras that respect this restriction normal.

5.1. Normal Coalgebras

We classify states and coalgebras as follows.

Definition 5.3 (Live, Dead, Normal).

Let $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ denote a $G$-coalgebra. A state $s\in X$ is accepting if $\delta^{\mathcal{X}}(s)(\alpha)=1$ for some $\alpha\in\mathsf{At}$. A state is live if it can transition to an accepting state one or more steps, or dead otherwise. A coalgebra is normal if it has no transitions to dead states.

Remark 5.4.

Note that, equivalently, a state is live iff $\ell^{\mathcal{X}}(s)\neq\varnothing$ and dead iff $\ell^{\mathcal{X}}(s)=\varnothing$. Dead states can exist in a normal coalgebra, but they must immediately reject all $\alpha\in\mathsf{At}$, since any successor of a dead state would also be dead.

Example 5.5.

Consider the following automaton.

[TABLE]

The state $s_{3}$ is accepting. The states $\iota$ and $s_{3}$ are live, since they can reach an accepting state. The states $s_{1}$ and $s_{2}$ are dead, since they can only reach non-accepting states. The automaton is not normal, since it contains the transitions \iota\mathrel{\raisebox{-2.0pt}{\xrightarrow{\alpha/p}}}s_{1}, s_{1}\mathrel{\raisebox{-2.0pt}{\xrightarrow{\alpha/q}}}s_{2}, and s_{2}\mathrel{\raisebox{-2.0pt}{\xrightarrow{\alpha/q}}}s_{2} to dead states $s_{1}$ and $s_{2}$. We can normalize the automaton by removing these transitions:

[TABLE]

The resulting automaton is normal: the dead states $s_{1}$ and $s_{2}$ reject all $\alpha\in\mathsf{At}$ immediately. ∎

The example shows how $G$-coalgebra can be normalized. Formally, let $\mathcal{X}=\langle X,\delta\rangle$ denote a coalgebra with dead states $D\subseteq X$. We define the normalized coalgebra $\widehat{\mathcal{X}}\coloneqq\langle X,\widehat{\delta}\rangle$ as follows:

[TABLE]

Lemma 5.6 (Correctness of normalization).

Let $\mathcal{X}$ be a $G$-coalgebra. Then the following holds:

1. (i)

$\mathcal{X}$* and $\widehat{\mathcal{X}}$ have the same solutions: that is, $s:X\to\mathop{\mathsf{Exp}}$ solves $\mathcal{X}$ if and only if $s$ solves $\widehat{\mathcal{X}}$; and* 2. (ii)

$\mathcal{X}$* and $\widehat{\mathcal{X}}$ accept the same languages: that is, $\ell^{\mathcal{X}}=\ell^{\widehat{\mathcal{X}}}$; and* 3. (iii)

$\widehat{\mathcal{X}}$* is normal.*

Proof.

For the first claim, suppose $s$ solves $\mathcal{X}$. It suffices (by Lemma A.3) to show that for $x\in X$ and $\alpha\in\mathsf{At}$ we have $\alpha\cdot s(x)\equiv\alpha\cdot\lfloor\delta^{\widehat{\mathcal{X}}}(x)(\alpha)\rfloor_{s}$. We have two cases.

• •

If $\delta^{\mathcal{X}}(x)(\alpha)=(p,x^{\prime})$ with $x^{\prime}$ dead, then by Proposition 4.5 we know that $\llbracket s(x^{\prime})\rrbracket=\ell^{\mathcal{X}}(x^{\prime})=\varnothing$. By Corollary 3.13, it follows that $s(x^{\prime})\equiv 0$. Recalling that $\delta^{\widehat{\mathcal{X}}}(x)(\alpha)=0$ by construction,

[TABLE]

• •

Otherwise, we know that $\delta^{\widehat{\mathcal{X}}}(x)(\alpha)=\delta^{\mathcal{X}}(x)(\alpha)$, and thus

[TABLE]

The other direction of the first claim can be shown analogously.

For the second claim, we can establish $x\in\ell^{\mathcal{X}}(s)\Leftrightarrow x\in\ell^{\widehat{\mathcal{X}}}(s)$ for all states $s$ by a straightforward induction on the length of $x\in\mathsf{GS}$, using that dead states accept the empty language.

For the third claim, we note that the dead states of $\mathcal{X}$ and $\widehat{\mathcal{X}}$ coincide by claim two; thus $\widehat{\mathcal{X}}$ has no transition to dead states by construction. ∎

5.2. Bisimilarity for Normal Coalgebras

We would like to show that, for normal coalgebras, states are bisimilar if and only if they accept the same language. This will allow us to reduce language-equivalence to bisimilarity, which is easy to establish algorithmically. We need to take a slight detour.

Recall the determinacy property satisfied by GKAT languages (Definition 2.2): a language $L\subseteq\mathsf{GS}$ is deterministic if, whenever strings $x,y\in L$ agree on the first $n$ atoms, they also agree on the first $n$ actions (or absence thereof). Now, let $\mathcal{L}\subseteq 2^{\mathsf{GS}}$ denote the set of deterministic languages. $\mathcal{L}$ carries a coalgebra structure $\langle\mathcal{L},\delta^{\mathcal{L}}\rangle$ whose transition map $\delta^{\mathcal{L}}$ is the semantic Brzozowski derivative:

[TABLE]

Note that the map is well-defined by determinacy: precisely one of the three cases holds.

Next, we define structure-preserving maps between $G$-coalgebras in the usual way:

Definition 5.7 (Homomorphism).

A homomorphism between G-coalgebras $\mathcal{X}$ and $\mathcal{Y}$ is a map $h\colon X\to Y$ from states of $\mathcal{X}$ to states of $\mathcal{Y}$ that respects the transition structures in the following sense:

[TABLE]

More concretely, for all $\alpha\in\mathsf{At}$, $p\in\Sigma$, and $x,x^{\prime}\in X$,

1. (i)

if $\delta^{\mathcal{X}}(x)(\alpha)\in 2$, then $\delta^{\mathcal{Y}}(h(x))(\alpha)=\delta^{X}(x)(\alpha)$; and 2. (ii)

if $\delta^{\mathcal{X}}(x)(\alpha)=(p,x^{\prime})$, then $\delta^{\mathcal{Y}}(h(x))(\alpha)=(p,h(x^{\prime}))$. ∎

We can now show that the acceptance map $\ell^{\mathcal{X}}\colon X\to 2^{\mathsf{GS}}$ is structure-preserving in the above sense. Moreover, it is the only structure-preserving map from states to deterministic languages:

Theorem 5.8.

If $\mathcal{X}$ is normal, then $\ell^{\mathcal{X}}\colon X\to 2^{\mathsf{GS}}$ is the unique homomorphism $\mathcal{X}\to\mathcal{L}$.

Since the identity function is trivially a homomorphism, Theorem 5.8 implies that $\ell^{\mathcal{L}}$ is the identity. That is, in the G-coalgebra $\mathcal{L}$, the state $L\in\mathcal{L}$ accepts the language $L$! This proves that every deterministic language is recognized by a $G$-coalgebra, possibly with an infinite number of states.

Theorem 5.8 says that $\mathcal{L}$ is final for normal $G$-coalgebras. The desired connection between bisimilarity and language-equivalence is then a standard corollary (Rutten, 2000):

Corollary 5.9.

Let $\mathcal{X}$ and $\mathcal{Y}$ be normal with states $s$ and $t$. Then $s\sim t$ if and only if $\ell^{\mathcal{X}}(s)=\ell^{\mathcal{Y}}(t)$.

Proof.

The implication from left to right is Lemma 5.2. For the other implication, we observe that the relation $R\coloneqq\{(s,t)\in X\times Y\mid\ell^{\mathcal{X}}(s)=\ell^{\mathcal{Y}}(t)\}$ is a bisimulation, using that $\ell^{\mathcal{X}}$ and $\ell^{\mathcal{Y}}$ are homomorphisms by Theorem 5.8:

• •

Suppose $s\mathrel{R}t$ and $\delta^{\mathcal{X}}(s)(\alpha)\in 2$. Then $\delta^{\mathcal{X}}(s)(\alpha)=\delta^{\mathcal{L}}(\ell^{\mathcal{X}}(s))(\alpha)=\delta^{\mathcal{L}}(\ell^{\mathcal{Y}}(t))(\alpha)=\delta^{\mathcal{Y}}(t)(\alpha)$.

• •

Suppose $s\mathrel{R}t$ and $\delta^{\mathcal{X}}(s)(\alpha)=(p,s^{\prime})$. Then $\delta^{\mathcal{L}}(\ell^{\mathcal{Y}}(t))(\alpha)=\delta^{\mathcal{L}}(\ell^{\mathcal{X}}(s))(\alpha)=(p,\ell^{\mathcal{X}}(s^{\prime}))$.

This implies that $\delta^{\mathcal{Y}}(t)(\alpha)=(p,t^{\prime})$ for some $t^{\prime}$, using that $\ell^{\mathcal{Y}}$ is a homomorphism. Hence

[TABLE]

by the above equation, which implies $s^{\prime}\mathrel{R}t^{\prime}$ as required. ∎

We prove a stronger version of this result in Lemma C.1.

5.3. Deciding Equivalence

We now have all the ingredients required for deciding efficiently whether two expressions are equivalent. Given two expressions $e_{1}$ and $e_{2}$, the algorithm proceeds as follows:

1. (1)

Convert $e_{1}$ and $e_{2}$ to equivalent Thompson automata $\mathcal{X}_{1}$ and $\mathcal{X}_{2}$; 2. (2)

Normalize the automata, obtaining $\widehat{\mathcal{X}}_{1}$ and $\widehat{\mathcal{X}}_{2}$; 3. (3)

Check bisimilarity of the start states $\iota_{1}$ and $\iota_{2}$ using Hopcroft-Karp (see Algorithm 1); 4. (4)

Return true if $\iota_{1}\sim\iota_{2}$, otherwise return false.

Theorem 5.10.

The above algorithm decides whether $\llbracket e_{1}\rrbracket=\llbracket e_{2}\rrbracket$ in time $\mathcal{O}(n\cdot\alpha(n))$ for $|\mathsf{At}|$ constant, where $\alpha$ denotes the inverse Ackermann function and $n=|e_{1}|+|e_{2}|$.

Proof.

The algorithm is correct by Theorem 4.1, Lemma 5.6, and Corollary 5.9:

[TABLE]

For the complexity claim, we analyze the running time of steps (1)–(3) of the algorithm:

1. (1)

Recall by Proposition 4.2 that the Thompson construction converts $e_{i}$ to an automaton with $\mathcal{O}(|e_{i}|)$ states in time $\mathcal{O}(|e_{i}|)$. Hence this step takes time $\mathcal{O}(n)$. 2. (2)

Normalizing $\mathcal{X}_{i}$ amounts to computing its dead states. This requires time $\mathcal{O}(|e_{i}|)$ using a breadth-first traversal as follows (since there are at most $|\mathsf{At}|\in\mathcal{O}(1)$ transitions per state). We find all states that can reach an accepting state by first marking all accepting states, and then performing a reverse breadth-first search rooted at the accepting states. All marked states are then live; all unmarked states are dead. 3. (3)

Since $\widehat{\mathcal{X}}_{i}$ has $\mathcal{O}(|e_{i}|)$ states and there are at most $|\mathsf{At}|\in\mathcal{O}(1)$ transitions per state, Hopcroft-Karp requires time $\mathcal{O}(n\cdot\alpha(n))$ by a classic result due to Tarjan (1975). ∎

Theorem 5.10 establishes a stark complexity gap with KAT, where the same decision problem is PSPACE-complete (Cohen et al., 1996) even for a constant number of atoms. Intuitively, the gap arises because GKAT expressions can be translated to linear-size deterministic automata, whereas KAT expressions may require exponential-size deterministic automata.

A shortcoming of Algorithm 1 is that it may scale poorly if the number of atoms $|\mathsf{At}|$ is large. It is worth noting that there are symbolic variants (Pous, 2015) of the algorithm that avoid enumerating $\mathsf{At}$ explicitly (cf. Algorithm 1 of Algorithm 1), and can often scale to very large alphabets in practice. As a concrete example, a version of GKAT specialized to probabilistic network verification was recently shown (Smolka et al., 2019) to scale to data-center networks with thousands of switches. In the worst case, however, we have the following hardness result:

Proposition 5.11.

If $|\mathsf{At}|$ is not a constant, GKAT equivalence is co-NP-hard, but in PSPACE.

Proof.

For the hardness result, we observe that Boolean unsatisfiability reduces to GKAT equivalence: $b\in\mathsf{BExp}$ is unsatisfiable, interpreting the primitive tests as variables, iff $\llbracket b\rrbracket=\varnothing$. The PSPACE upper bound is inherited from KAT by Remark 2.1. ∎

6. Completeness for the language model

In Section 3 we presented an axiomatization that is sound with respect to the language model, and put forward the conjecture that it is also complete. We have already proven a partial completeness result (Corollary 3.13). In this section, we return to this matter and show we can prove completeness with a generalized version of (LABEL:ax:fixpoint).

6.1. Systems of Left-affine Equations

A system of left-affine equations (or simply, a system) is a finite set of equations of the form

[TABLE]

where $+_{b}$ associates to the right, the $\boldsymbol{x_{i}}$ are variables, the $e_{ij}$ are GKAT expressions, and the $b_{ij}$ and $d_{i}$ are Boolean guards satisfying the following row-wise disjointness property for row $1\leq i\leq n$:

• •

for all $j\neq k$, the guards $b_{ij}$ and $b_{ik}$ are disjoint: $b_{ij}\cdot b_{ik}\equiv_{\text{BA}}0$; and

• •

for all $1\leq j\leq n$, the guards $b_{ij}$ and $d_{i}$ are disjoint: $b_{ij}\cdot d_{i}\equiv_{\text{BA}}0$.

Note that by the disjointness property, the ordering of the summands is irrelevant: the system is invariant (up to $\equiv$) under column permutations. A solution to such a system is a function $s:\{\boldsymbol{x_{1}},\dots,\boldsymbol{x_{n}}\}\to\mathop{\mathsf{Exp}}$ assigning expressions to variables such that, for row $1\leq i\leq n$:

[TABLE]

Note that any finite $G$-coalgebra gives rise to a system where each variable represents a state, and the equations define what it means to be a solution to the coalgebra (c.f. Definition 4.3); indeed, a solution to a $G$-coalgebra is precisely a solution to its corresponding system of equations, and vice versa. In particular, for a coalgebra $\mathcal{X}$ with states $x_{1}$ to $x_{n}$, the parameters for equation $i$ are:

[TABLE]

Systems arising from $G$-coalgebras have a useful property: for all $e_{ij}$, it holds that $E(e_{ij})\equiv 0$. This property is analogous to the empty word property in Salomaa’s axiomatization of regular languages (Salomaa, 1966); we call such systems Salomaa.

To obtain a general completeness result beyond Section 3.4, we assume an additional axiom:

Uniqueness axiom. Any system of left-affine equations that is Salomaa has at most one solution, modulo $\equiv$. More precisely, whenever $s$ and $s^{\prime}$ are solutions to a Salomaa system, it holds that $s(x_{i})\equiv s^{\prime}(x_{i})$ for all $1\leq i\leq n$.

Remark 6.1.

We do not assume that a solution always exists, but only that if it does, then it is unique up to $\equiv$. It would be unsound to assume that all such systems have solutions; the following automaton and its system, due to (Kozen and Tseng, 2008), constitutes a counterexample:

[TABLE]

As shown in (Kozen and Tseng, 2008), no corresponding while program exists for this system.

When $n=1$, a system is a single equation of the form $x=ex+_{b}d$. In this case, (LABEL:ax:unroll) tells us that a solution does exist, namely $e^{(b)}d$, and (LABEL:ax:fixpoint) says that this solution is unique up to $\equiv$ under the proviso $E(e)\equiv 0$. In this sense, we can regard the uniqueness axiom as a generalization of (LABEL:ax:fixpoint) to systems with multiple variables.

Theorem 6.2.

The uniqueness axiom is sound in the model of guarded strings: given a system of left-affine equations as in (3) that is Salomaa, there exists at most one $R:\{x_{1},\ldots,x_{n}\}\to 2^{\mathsf{GS}}$ s.t.

[TABLE]

Proof Sketch.

We recast this system as a matrix-vector equation of the form $x=Mx+D$ in the KAT of $n$-by-$n$ matrices over $2^{\mathsf{GS}}$; solutions to $x$ in this equation are in one-to-one correspondence with functions $R$ as above. We then show that the map $\sigma(x)=Mx+D$ on the set of $n$-dimensional vectors over $2^{\mathsf{GS}}$ is contractive in a certain metric, and therefore has a unique fixpoint by the Banach fixpoint theorem; hence, there can be at most one solution $x$. ∎

6.2. General Completeness

Using the generalized version of the fixpoint axiom, we can now establish completeness.

Theorem 6.3 (Completeness).

The axioms are complete w.r.t. $\llbracket-\rrbracket$: given $e_{1},e_{2}\in\mathop{\mathsf{Exp}}$,

[TABLE]

Proof.

Let $\mathcal{X}_{1}$ and $X_{2}$ be the Thompson automata corresponding to $e_{1}$ and $e_{2}$, with initial states $\iota_{1}$ and $\iota_{2}$, respectively. Theorem 4.8 shows there are solutions $s_{1}$ and $s_{2}$, with $s_{1}(\iota_{1})\equiv e_{1}$ and $s_{2}(\iota_{2})\equiv e_{2}$; and we know from Lemma 5.6 that $s_{1}$ and $s_{2}$ solve the normalized automata $\widehat{\mathcal{X}_{1}}$ and $\widehat{\mathcal{X}_{2}}$. By Lemma 5.6, Theorem 4.1, and the premise, we derive that $\widehat{\mathcal{X}_{1}}$ and $\widehat{\mathcal{X}_{2}}$ accept the same language:

[TABLE]

This implies, by Corollary 5.9, that there is a bisimulation $R$ between $\widehat{\mathcal{X}_{1}}$ and $\widehat{\mathcal{X}_{2}}$ relating $\iota_{1}$ and $\iota_{2}$. This bisimulation can be given the following transition structure,

[TABLE]

turning $\mathcal{R}=\langle R,\delta^{\mathcal{R}}\rangle$ into a $G$-coalgebra; note that $\delta^{\mathcal{R}}$ is well-defined since $R$ is a bisimulation.

Now, define $s_{1}^{\prime},s_{2}^{\prime}:R\to\mathop{\mathsf{Exp}}$ by $s_{1}^{\prime}(x_{1},x_{2})=s_{1}(x_{1})$ and $s_{2}^{\prime}(x_{1},x_{2})=s_{2}(x_{2})$. We claim that $s_{1}^{\prime}$ and $s_{2}^{\prime}$ are both solutions to $\mathcal{R}$; to see this, note that for $\alpha\in\mathsf{At}$, $(x_{1},x_{2})\in R$, and $i\in\{1,2\}$, we have that

[TABLE]

Thus, $s_{i}^{\prime}$ is a solution by Lemma A.3.

Since the system of left-affine equations induced by $\mathcal{R}$ is Salomaa, the uniqueness axiom then tells us that $s_{1}(\iota_{1})=s_{1}^{\prime}(\iota_{1},\iota_{2})\equiv s_{2}^{\prime}(\iota_{1},\iota_{2})=s_{2}(\iota_{2})$; hence, we can conclude that $e_{1}\equiv e_{2}$. ∎

7. Coalgebraic Structure

The coalgebraic theory of GKAT is quite different from that of KA and KAT because the final $G$-coalgebra, without the normality assumption from § 5.1, is not characterized by sets of finite guarded strings. Even including infinite accepted strings is not enough, as this still cannot distinguish between early and late rejection. It is therefore of interest to characterize the final $G$-coalgebra and determine its precise relationship to the language model. We give a brief overview of these results, which give insight into the nature of halting versus looping and underscore the role of topology in coequational specifications.

In Appendix C we give two characterizations of the final $G$-coalgebra, one in terms of nonexpansive maps $\mathsf{At}^{\omega}\to\Sigma^{*}\cup\Sigma^{\omega}$ with natural metrics defined on both spaces (§ C.1.1) and one in terms of labeled trees with nodes indexed by $\mathsf{At}^{+}$ (§ C.1.2), and show their equivalence. In § C.2, we state and prove Lemma C.1 a stronger form of the bisimilarity lemma (Corollary 5.9).

We have discussed the importance of the determinacy property (Definition 2.2). In § C.3 we identify another important property satisfied by all languages $L^{\mathcal{X}}(s)$, a certain closure property defined in terms of a natural topology on $\mathsf{At}^{\omega}$. In § C.4, we define a language model $\mathcal{L}^{\prime}$, a $G$-coalgebra whose states are the subsets of $\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ satisfying the determinacy and closure properties and whose transition structure is the semantic Brzozowski derivative:

[TABLE]

Although this looks similar to the language model $\mathcal{L}$ of Section 5.2, they are not the same: states of $\mathcal{L}$ contain finite strings only, and $\mathcal{L}$ and $\mathcal{L}^{\prime}$ are not isomorphic.

We show that $L$ is identity on $\mathcal{L}^{\prime}$ and that $\mathcal{L}^{\prime}$ is isomorphic to a subcoalgebra of the final $G$-coalgebra. It is not the final $G$-coalgebra, because early and late rejection are not distinguished: an automaton could transition before rejecting or reject immediately. Hence, $L:(X,\delta^{X})\to\mathcal{L}^{\prime}$ is not a homomorphism in general. However, normality prevents this behavior, and $L$ is a homomorphism if $(X,\delta^{X})$ is normal. Thus $\mathcal{L}^{\prime}$ contains the unique homomorphic image of all normal $G$-coalgebras.

Finally, in Theorem C.5 we identify a subcoalgebra $\mathcal{L}^{\prime\prime}\subseteq\mathcal{L}^{\prime}$ that is normal and final in the category of normal $G$-coalgebras. The subcoalgebra $\mathcal{L}^{\prime\prime}$ is defined topologically; roughly speaking, it consists of sets $A\subseteq\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ such that $A$ is the topological closure of $A\cap\mathsf{GS}$. Thus $\mathcal{L}^{\prime\prime}$ is isomorphic to the language model $\mathcal{L}$ of Section 5.2: the states of $\mathcal{L}$ are obtained from those of $\mathcal{L}^{\prime\prime}$ by intersecting with $\mathsf{GS}$, and the states of $\mathcal{L}^{\prime\prime}$ are obtained from those of $\mathcal{L}$ by taking the topological closure. Thus $\mathcal{L}$ is isomorphic to a coequationally-defined subcoalgebra of the final $G$-coalgebra.

We also remark that $\mathcal{L}^{\prime}$ itself is final in the category of $G$-coalgebras that satisfy a weaker property than normality, the so-called early failure property, which can also be characterized topologically.

8. Related Work

Program schematology is one of the oldest areas of study in the mathematics of computing. It is concerned with questions of translation and representability among and within classes of program schemes, such as flowcharts, while programs, recursion schemes, and schemes with various data structures such as counters, stacks, queues, and dictionaries (Garland and Luckham, 1973; Ianov, 1960; Rutledge, 1964; Paterson and Hewitt, 1970; Shepherdson and Sturgis, 1963; Luckham et al., 1970). A classical pursuit in this area was to find mechanisms to transform unstructured flowcharts to structured form (Ashcroft and Manna, 1972; Böhm and Jacopini, 1966; Kosaraju, 1973; Oulsnam, 1982; Peterson et al., 1973; Ramshaw, 1988; Williams and Ossher, 1978; Morris et al., 1997). A seminal result was the Böhm-Jacopini theorem (Böhm and Jacopini, 1966), which established that all flowcharts can be converted to while programs provided auxiliary variables are introduced. Böhm and Jacopini conjectured that the use of auxiliary variables was necessary in general, and this conjecture was confirmed independently by Ashcroft and Manna (1972) and Kosaraju (1973).

Early results in program schematology, including those of (Böhm and Jacopini, 1966; Ashcroft and Manna, 1972; Kosaraju, 1973), were typically formulated at the first-order uninterpreted (schematic) level. However, many restructuring operations can be accomplished without reference to first-order constructs. It was shown in (Kozen and Tseng, 2008) that a purely propositional formulation of the Böhm-Jacopini theorem is false: there is a three-state deterministic propositional flowchart that is not equivalent to any propositional while program. As observed by a number of authors (e.g. (Kosaraju, 1973; Peterson et al., 1973)), while loops with multi-level breaks are sufficient to represent all deterministic flowcharts without introducing auxiliary variables, and (Kosaraju, 1973) established a strict hierarchy based on the allowed levels of the multi-level breaks. That result was reformulated and proved at the propositional level in (Kozen and Tseng, 2008).

The notions of functions on a domain, variables ranging over that domain, and variable assignment are inherent in first-order logic, but are absent at the propositional level. Moreover, many arguments rely on combinatorial graph restructuring operations, which are difficult to formalize. Thus the value of the propositional view is twofold: it operates at a higher level of abstraction and brings topological and coalgebraic concepts and techniques to bear.

Propositional while programs and their encoding in terms of the regular operators goes back to early work on Propositional Dynamic Logic (Fischer and Ladner, 1979). GKAT as an independent system and its semantics were introduced in (Kozen and Tseng, 2008; Kozen, 2008) under the name propositional while programs, although the succinct form of the program operators is new here. Also introduced in (Kozen and Tseng, 2008; Kozen, 2008) were the functor $G$ and automaton model (Section 4), the determinacy property (Definition 2.2) (called strict determinacy there), and the concept of normality (Section 5.1) (called liveness there). The linear construction of an automaton from a while program was sketched in (Kozen and Tseng, 2008; Kozen, 2008), based on earlier results for KAT automata (Kozen, 2003), but the complexity of deciding equivalence was not addressed. The more rigorous alternative construction given here (Section 4.2) is needed to establish well-nestedness, thereby enabling our Kleene theorem. The existence of a complete axiomatization was not considered in (Kozen and Tseng, 2008; Kozen, 2008).

Guarded strings, which form the basis of our language semantics, come from (Kaplan, 1969).

The axiomatization we propose for GKAT is closely related to Salomaa’s axiomatization of regular expressions based on unique fixed points (Salomaa, 1966) and to Silva’s coalgebraic generalization of KA (Silva, 2010). The proof technique we used for completeness is inspired by (Silva, 2010).

The relational semantics is inspired by that for KAT (Kozen and Smith, 1996), which goes back to work on Dynamic Logic (Fischer and Ladner, 1979). Because the fixpoint axiom uses a non-algebraic side condition, extra care is needed to define the relational interpretation for GKAT.

9. Conclusions and Future Directions

We have presented a comprehensive algebraic and coalgebraic study of GKAT, an abstract programming language with uninterpreted actions. Our main contributions include: (i) a new automata construction yielding a nearly linear time decidability result for program equivalence; (ii) a Kleene theorem for GKAT providing an exact correspondence between programs and a well-defined class of automata; and (iii) a set of sound and complete axioms for program equivalence.

We hope this paper is only the beginning of a long and beautiful journey into understanding the (co)algebraic properties of efficient fragments of imperative programming languages. We briefly discuss some limitations of our current development and our vision for future work.

As in Salomaa’s axiomatization of KA, our axiomatization is not fully algebraic: the side condition of (LABEL:ax:fixpoint) is only sensible for the language model. As a result, the current completeness proof does not generalize to other natural models of interest—e.g., probabilistic or relational. To overcome this limitation, we would like to adapt Kozen’s axiomatization of KA to GKAT by developing a natural order for GKAT programs. In the case of KA we have $e\leq f~{}\mathrel{\vcentcolon\Longleftrightarrow}~{}e+f=f$, but this natural order is no longer definable in the absence of $+$ and so we need to axiomatize $e\leq f$ for GKAT programs directly. This appears to be the main missing piece to obtain an algebraic axiomatization.

On the coalgebraic side, we are interested in studying the different classes of $G$-coalgebras from a coequational perspective. Normal coalgebras, for instance, form a covariety, and hence are characterized by coequations. If well-nested $G$-coalgebras could be shown to form a covariety, this would imply completeness of the axioms without the extra uniqueness axiom from Section 6.

Various extensions of KAT to reason about richer programs (KAT+B!, NetKAT, ProbNetKAT) have been proposed, and it is natural to ask whether extending GKAT in similar directions will yield interesting algebraic theories and decision procedures for domain-specific applications. For instance, recent work (Smolka et al., 2019) on a probabilistic network verification tool suggests that GKAT is better suited for probabilistic models than KAT, as it avoids mixing non-determinism and probabilities. The complex semantics of probabilistic programs would make a framework for equational and automated reasoning especially valuable.

In a different direction, a language model containing infinite traces could be interesting in many applications, as it could serve as a model to reason about non-terminating programs—e.g., loops in NetKAT in which packets may be forwarded forever. An interesting open question is whether the infinite language model can be finitely axiomatized.

Finally, another direction would be to extend the GKAT decision procedure to handle extra equations. For instance, both KAT+B! and NetKAT have independently-developed decision procedures, that are similar in flavor. This raises the question of whether the GKAT decision procedure could be extended in a more generic way, similar to the Nelson-Oppen approach (Nelson and Oppen, 1979) for combining decision procedures used in SMT solving.

Acknowledgements.

We are grateful to the anonymous reviewers for their feedback and help in improving this paper, and thank Paul Brunet, Fredrik Dahlqvist, and Jonathan DiLorenzo for numerous discussions and suggestions on GKAT. Jonathan DiLorenzo and Simon Docherty provided helpful feedback on drafts of this paper. We thank the Bellairs Research Institute of McGill University for providing a wonderful research environment. This work was supported in part by the University of Wisconsin, a Facebook TAV award, ERC starting grant Profoundnet (679127), a Royal Society Wolfson fellowship, a Leverhulme Prize (PLP-2016-129), NSF grants AitF-1637532, CNS-1413978, and SaTC-1717581, and gifts from Fujitsu and InfoSys.

Appendix A Omitted Proofs

See 2.4

Proof.

Recall from Remark 2.1 that there is a language-preserving map $\varphi$ from GKAT to KAT expressions. As with GKAT’s language model, GKAT’s relational model is inherited from KAT; that is, $\mathcal{R}_{i}\llbracket-\rrbracket=\mathcal{R}^{\mathsf{KAT}}_{i}\llbracket-\rrbracket\circ\varphi$. Thus, the claim follows by Kozen and Smith (1996), who showed the equivalent of Theorem 2.4 for KAT:

[TABLE]

Lemma A.1.

$\mathcal{P}_{i}\llbracket e\rrbracket$* is a well-defined subprobability kernel. In particular, $\mathcal{P}_{i}\llbracket{(e+_{b}1)}^{n}\cdot\overline{b}\rrbracket(\sigma)(\sigma^{\prime})$ increases monotonically in $n$ and the limit for $n\to\infty$ exists.*

Proof.

We begin by showing the first claim by well-founded induction on $\prec$, the smallest partial order subsuming the subterm order and satisfying

[TABLE]

for all $e,b,n$. The claim is obvious except when $e=f^{(b)}$. In that case, we have by induction hypothesis that $F_{n}\coloneqq\mathcal{P}_{i}\llbracket{(f+_{b}1)}^{n}\cdot\overline{b}\rrbracket(\sigma)(\sigma^{\prime})$ is well defined and bounded above by $1$ for all $n$. To establish that $\lim_{n\to\infty}F_{n}$ exist and is also bounded above by $1$, it then suffices to show the claim that $F_{n}$ increases monotonically in $n$.

If $F_{n}=0$ then $F_{n+1}\geq F_{n}$ holds trivially, so assume $F_{n}>0$. This implies that $\sigma^{\prime}\in\operatorname{\mathsf{sat}}^{\dagger}(\overline{b})$. Thus

[TABLE]

See 2.7

Proof.

By mutual implication.

• $\Rightarrow$:

For soundness, we will define a map $\kappa_{i}\colon\mathsf{GS}\to\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ that interprets guarded strings as sub-Markov kernels, and lift it to languages via pointwise summation:

[TABLE]

To establish the claim, we will then show the following equality:

[TABLE]

We define $\kappa_{i}\colon\mathsf{GS}\to\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ inductively as follows:

[TABLE]

To prove Equation 4, it suffices to establish the following equations:

[TABLE]

From there, Equation 4 follows by a straightforward well-founded induction on $\prec$, the partial from the proof of Lemma A.1.

For Equation 5, we have

[TABLE]

where the last line follows because $\{\operatorname{\mathsf{sat}}^{\dagger}(b)\mid b\in\mathsf{BExp}\}\subseteq 2^{\mathsf{State}}$ is a Boolean algebra of sets with atoms $\operatorname{\mathsf{sat}}^{\dagger}(\alpha)$, $\alpha\in\mathsf{At}$, meaning that

[TABLE]

For Equation 6, we have

[TABLE]

For Equation 7, we need the following auxiliary facts:

1. (A1)

$\kappa_{i}(\alpha x)(\sigma)(\sigma^{\prime})=[\sigma\in\operatorname{\mathsf{sat}}^{\dagger}(\alpha)]\cdot\kappa_{i}(\alpha x)(\sigma)(\sigma^{\prime})$ 2. (A2)

$\kappa_{i}(x\alpha)(\sigma)(\sigma^{\prime})=[\sigma^{\prime}\in\operatorname{\mathsf{sat}}^{\dagger}(\alpha)]\cdot\kappa_{i}(x\alpha)(\sigma)(\sigma^{\prime})$ 3. (A3)

$\kappa_{i}(x\alpha y)(\sigma)(\sigma^{\prime})=\sum_{\sigma^{\prime\prime}}\kappa_{i}(x\alpha)(\sigma)(\sigma^{\prime\prime})\cdot\kappa_{i}(\alpha y)(\sigma^{\prime\prime})(\sigma^{\prime})$ 4. (A4)

$\llbracket e\rrbracket\diamond\llbracket f\rrbracket\cong\{(\alpha,x\alpha,\alpha y)\mid\alpha\in\mathsf{At},x\alpha\in\llbracket e\rrbracket,\alpha y\in\llbracket f\rrbracket\}$

Fact (A1) is immediate by definition of $\kappa_{i}$, and facts (A2) and (A3) follow by straightforward inductions on $|x|$. We defer the proof of (A4) to Lemma A.2. We can then compute:

[TABLE]

and, observing that

[TABLE]

we obtain Equation 7:

[TABLE]

For Equation 8, we need the following identity (for all $\alpha,x,b,\sigma$):

[TABLE]

Using A1, it suffices to show the equivalence

[TABLE]

The implication from left to right follows directly by monotonicity of $\operatorname{\mathsf{sat}}^{\dagger}$. For the implication from right to left, we have that either $\alpha\leq b$ or $\alpha\leq\overline{b}$. Using again monotonicity of $\operatorname{\mathsf{sat}}^{\dagger}$, the possibility $\alpha\leq\overline{b}$ is seen to cause a contradiction.

With Identity 9 at our disposal, Equation 8 is easy to establish:

[TABLE]

This concludes the soundness proof.

• $\Leftarrow$:

For completeness, we will exhibit an interpretation $i$ over the state space $\mathsf{GS}$ such that

[TABLE]

Define $i\coloneqq(\mathsf{GS},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$, where

[TABLE]

We need two auxiliary observations:

1. (A1)

$\alpha\in\operatorname{\mathsf{sat}}^{\dagger}(b)\iff\alpha\in\llbracket b\rrbracket$ 2. (A2)

Monotonicity: $\mathcal{P}_{i}\llbracket e\rrbracket(v)(w)\neq 0\implies\exists x.\,w=vx$.

They follow by straightforward inductions on $b$ and $e$, respectively. To establish Equation 10, it suffices to show the following equivalence for all $x,y\in{(\mathsf{At}\cup\Sigma)}^{*}$:

[TABLE]

We proceed by well-founded induction on the ordering $\prec$ on expressions from the proof of Lemma A.1:

1. •

For $e=b$, we use fact (A1) to derive that

[TABLE]

Thus we have

[TABLE] 2. •

For $e=p$, we have that

[TABLE]

It follows that

[TABLE] 3. •

For $e+_{b}f$, we have that

[TABLE]

We will argue the case $\alpha\in\operatorname{\mathsf{sat}}^{\dagger}(b)$ explicitly; the argument for the case $\alpha\in\operatorname{\mathsf{sat}}^{\dagger}(\overline{b})$ is analogous. We compute:

[TABLE] 4. •

For $e\cdot f$, recall that

[TABLE]

Thus,

[TABLE] 5. •

For $e^{*}$, recall that

[TABLE]

Since this is the limit of a monotone sequence by Lemma A.1, it follows that

[TABLE]

The penultimate step is justified by the identity

[TABLE]

which we establish by induction on $n\geq 0$:

The case $n=0$ is trivial. For $n>0$, we have the following KAT equivalence:

[TABLE]

where the induction hypothesis yields the KAT equivalence

[TABLE]

thanks to completeness of the KAT axioms for the language model. The claim follows by soundness of the KAT axioms.

This concludes the proof of Theorem 2.7. ∎

Lemma A.2.

For deterministic languages $L,K\in\mathcal{L}$, we have the following isomorphism:

[TABLE]

Proof.

We clearly have a surjective map

[TABLE]

from right to left. To see that this map is also injective, we show that for all $x_{1}\alpha,x_{2}\beta\in L$ and $\alpha y_{1},\beta y_{2}\in K$ satisfying $x_{1}\alpha y_{1}=x_{2}\beta y_{2}$, we must have $(\alpha,x_{1}\alpha,\alpha y_{2})=(\beta,x_{2}\beta,\beta y_{2})$. This is obvious when $|x_{1}|=|x_{2}|$, so assume $|x_{1}|\neq|x_{2}|$. We will show that this is impossible.

W.l.o.g. we have $|x_{1}|<|x_{2}|$. By the assumed equality, it follows that $x_{2}$ must be of the form $x_{2}=x_{1}\alpha z$ for some $z$, and further $zy_{1}=\beta y_{2}$. Now consider the language

[TABLE]

The language is deterministic, and it contains both $\alpha$ and $\alpha z\beta$; but the latter contradicts the former. ∎

See 3.3

Proof.

Formally, the proof proceeds by induction on the construction of $\equiv$ as a congruence. Practically, it suffices to verify soundness of each rule—the inductive cases of the congruence are straightforward because of how $\llbracket-\rrbracket$ is defined.

• (LABEL:ax:idemp)

For $e+_{b}e\equiv e$, we derive

[TABLE]

This completes the proof. ∎

See 3.7

Proof.

By induction on $e$. For a primitive action $p$, $D_{\alpha}(p)=(p,1)$, for all $\alpha\in\mathsf{At}$, and $E(p)=0$. Then

[TABLE]

For a primitive test $c$, $D_{\alpha}(c)=[\alpha\leq c]$ and $E(c)=c$. Then

[TABLE]

For a conditional $e_{1}+_{c}e_{2}$, we have inductively:

[TABLE]

Then

[TABLE]

For sequential composition $e_{1}\cdot e_{2}$, suppose $e_{1}$ and $e_{2}$ are decomposed as in (12).

[TABLE]

Finally, for a while loop $e^{(c)}$ we will use Lemma 3.9 (Productive Loop):

[TABLE]

∎

See 3.8

Proof.

[TABLE]

Note that for * we use the observation that for all $\alpha$ such that $D_{\alpha}(e)=(p_{\alpha},e_{\alpha})$ it is immediate that $\alpha\not\leq E(e)$ and hence the condition $\alpha\leq\overline{E(e)}$ is redundant. ∎

See 3.10

Proof.

We start by deriving the remaining facts for guarded union.

• (LABEL:fact:skewassoc-dual)

For $e+_{b}(f+_{c}g)\equiv(e+_{b}f)+_{b+c}g$, we derive

[TABLE]

Next, we derive the remaining loop facts.

• (LABEL:fact:guard-loop-out)

For $e^{(b)}\equiv e^{(b)}\overline{b}$, we derive

[TABLE]

This completes the proof. ∎

See 3.12

Proof.

By induction on $e$. In the base, there are two cases to consider.

• •

If $e=d$ for some Boolean $d$, then the claim follows by completeness of the Boolean algebra axioms, which $\equiv$ subsumes by definition.

• •

If $e=a\in\Sigma$, then $\llbracket bec\rrbracket=\llbracket be\rrbracket$ implies $\llbracket c\rrbracket=\llbracket 1\rrbracket$, hence $c\equiv 1$ by completeness of Boolean algebra; the claim then follows.

For the inductive step, there are three cases:

• •

If $e=e_{0}+_{d}e_{1}$, then $\llbracket bec\rrbracket=\llbracket be\rrbracket$ implies that $\llbracket dbe_{0}c\rrbracket=\llbracket dbe_{0}\rrbracket$ and $\llbracket\overline{d}be_{1}c\rrbracket=\llbracket\overline{d}be_{1}\rrbracket$. By induction, we then know that $dbe_{0}c\equiv dbe_{0}$ and $\overline{d}be_{1}c\equiv\overline{d}be_{1}$. We can then derive as follows:

[TABLE]

• •

If $e=e_{0}\cdot e_{1}$, then let $d=\sum\{\alpha\in\mathsf{At}:\llbracket be_{0}\alpha\rrbracket\neq\varnothing\}$. We then know that $\llbracket be_{0}d\rrbracket=\llbracket be_{0}\rrbracket$, and hence $be_{0}d\equiv be_{0}$ by induction. We furthermore claim that $\llbracket de_{1}c\rrbracket=\llbracket de_{1}\rrbracket$. To see this, note that if $\alpha{}w\beta\in\llbracket de_{1}\rrbracket$, then $\alpha\leq d$, and hence there exists an $x\alpha\in\llbracket be_{0}\alpha\rrbracket\subseteq\llbracket be_{0}d\rrbracket=\llbracket be_{0}\rrbracket$. Thus, we know that $x\alpha{}w\beta\in\llbracket be_{0}e_{1}\rrbracket=\llbracket be_{0}e_{1}c\rrbracket$, meaning that $\beta\leq c$; hence, we know that $\alpha{}w\beta\in\llbracket de_{1}c\rrbracket$. By induction, $de_{1}c\equiv de_{1}$. We then derive:

[TABLE]

• •

If $e=e_{0}^{(d)}$, first note that if $b\equiv 0$, then the claim follows trivially. Otherwise, let

[TABLE]

We make the following observations.

1. (i)

Since $b\not\equiv 0$, we have that $\llbracket b\rrbracket\diamond\llbracket{de_{0}}\rrbracket^{0}\diamond\llbracket b\rrbracket=\llbracket b\rrbracket\neq\varnothing$, and thus $b\leq h$. 2. (ii)

If $\alpha\leq h\overline{d}$, then in particular $\gamma{}w\alpha\in\llbracket b\rrbracket\diamond\llbracket de_{0}\rrbracket^{n}\diamond\llbracket\alpha\rrbracket$ for some $n$ and $\gamma{}w$. Since $\alpha\leq\overline{d}$, it follows that $\gamma{}w\alpha\in\llbracket be_{0}^{(d)}\rrbracket=\llbracket be_{0}^{(d)}c\rrbracket$, and thus $\alpha\leq c$. Consequently, $h\overline{d}\leq c$. 3. (iii)

If $\alpha{}w\beta\in\llbracket dhe_{0}\rrbracket$, then $\alpha\leq h$ and hence there exists an $n$ such that $\gamma{}x\alpha\in\llbracket b\rrbracket\diamond\llbracket de_{0}\rrbracket^{n}\diamond\llbracket\beta\rrbracket$. But then $\gamma{}x\alpha{}w\beta\in\llbracket b\rrbracket\ \diamond\llbracket de_{0}\rrbracket^{n+1}\diamond\llbracket\beta\rrbracket$, and therefore $\beta\leq h$. We can conclude that $\llbracket dhe_{0}\rrbracket=\llbracket dhe_{0}h\rrbracket$; by induction, it follows that $dhe_{0}h\equiv dhe_{0}$.

Using these observations and the invariance lemma (Lemma 3.11), we derive

[TABLE]

This completes the proof.∎

See 4.5

Proof.

We show that

[TABLE]

for all states $x$ by induction on the length of $w\in\mathsf{GS}$. We will use that $w$ is of the form $w=\alpha u$ for some $\alpha\in\mathsf{At}$, $u\in{(At\cdot\Sigma)}^{*}$ and thus

[TABLE]

This concludes the proof. ∎

Lemma A.3.

Let $\mathcal{X}=\langle X,\delta^{\mathcal{X}}\rangle$ be a $G$-coalgebra. A function $s\colon X\to\mathop{\mathsf{Exp}}$ is a solution to $\mathcal{X}$ if and only if for all $\alpha\in\mathsf{At}$ and $x\in X$ it holds that $\alpha\cdot s(x)\equiv\alpha\cdot\lfloor\delta^{\mathcal{X}}(x)(\alpha)\rfloor_{s}$.

Proof.

We shall use some of the observations about \operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}} from Appendix B.

• $(\Rightarrow)$

Let $s$ be a solution to $\mathcal{X}$; we then derive for $\alpha\in\mathsf{At}$ and $x\in X$ that

[TABLE]

This completes the proof. ∎

See 4.7

Proof.

Assume $\mathcal{X}$ is well-nested. We proceed by rule induction on the well-nestedness derivation.

1. (i)

Suppose $\delta^{\mathcal{X}}\colon X\to 2^{\mathsf{At}}$. Then

[TABLE]

is a solution to $\mathcal{X}$. 2. (ii)

Suppose $\mathcal{X}=(\mathcal{Y}+\mathcal{Z})[Y,h]$, where $h\in G(Y+Z)$ and $\mathcal{Y}$ and $\mathcal{Z}$ are well-nested with solutions $s^{\mathcal{Y}}$ and $s^{\mathcal{Z}}$. We need to exhibit a solution $s^{\mathcal{X}}$ to $\mathcal{X}$. For $y\in Y$ and $z\in Z$ we define

[TABLE]

By Lemma A.3, it then suffices to prove that for $x\in Y+Z$ and $\alpha\in\mathsf{At}$, we have

[TABLE]

There are two cases to distinguish.

• •

If $x\in Z$, then

[TABLE]

• •

If $x\in Y$, then we find by choice of $s^{\mathcal{X}}$ and $s^{\mathcal{Y}}$ that

[TABLE]

We distinguish three subcases:

• –

If $\delta^{\mathcal{Y}}(x)(\alpha)\in\{0\}\cup\Sigma\times Y$ then $\delta^{\mathcal{Y}}(x)(\alpha)=\delta^{\mathcal{X}}(x)(\alpha)$ and thus

[TABLE]

This completes the proof. ∎

Lemma A.4.

Let $e\in\mathop{\mathsf{Exp}}$ and $\alpha\in\mathsf{At}$. Then $\iota_{e}(\alpha)=1$ if and only if $\alpha\leq E(e)$.

Proof.

We proceed by induction on $e$. In the base, there are two cases.

• •

If $e=b\in\mathsf{BExp}$, then $\iota_{e}(\alpha)=1$ if and only if $\alpha\leq b=E(b)$.

• •

If $e=p\in\Sigma$, then $\iota_{e}(\alpha)=0$ and $E(e)=0$.

For the inductive step, there are three cases.

• •

If $e=f+_{b}g$, then suppose $\alpha\leq b$. In that case, $\iota_{e}(\alpha)=1$ holds if and only if $\iota_{f}(\alpha)=1$, which by induction is true precisely when $\alpha\leq E(f)$, which is equivalent to $\alpha\leq E(f+_{b}g)$. The other case can be treated analogously.

• •

If $e=f\cdot g$, then $\iota_{e}(\alpha)=1$ implies that $\iota_{f}(\alpha)=1$ and $\iota_{g}(\alpha)=1$, which means that $\alpha\leq E(f)$ and $\alpha\leq E(g)$ by induction, and hence $\alpha\leq E(e)$. The other implication can be derived in a similar fashion.

• •

If $e=f^{(b)}$, then $\iota_{e}(\alpha)=1$ is equivalent to $\alpha\leq\overline{b}=E(e)$. ∎

See 4.8

Proof.

We proceed by induction on $e$, showing that we can construct a solution $s_{e}$ to $\mathcal{X}_{e}$. For the main claim, if we then show that e\equiv\operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}}_{\alpha\leq 1}\lfloor\iota_{e}(\alpha)\rfloor_{s_{e}}, it follows that we can extend $s_{e}$ to a solution $s$ of $\mathcal{X}_{e}^{\iota}$, by setting $s(\iota)=e$ and $s(x)=s_{e}(x)$ for $x\in X_{e}$. In the base, there are two cases.

• •

If $e=b\in\mathsf{BExp}$, then we choose for $s_{e}$ the (empty) map from $X_{e}$ to $\mathop{\mathsf{Exp}}$; this (vacuously) makes $s_{e}$ a solution to $\mathcal{X}_{e}$. For the second part, we can derive using Lemmas B.3 and B.4:

[TABLE]

• •

If $e=p\in\Sigma$, then we choose $s_{e}(*)=1$. To see that $s_{e}$ is a solution to $\mathcal{X}_{e}$, note by Lemma B.3:

[TABLE]

For the second part, derive as follows, using the same Lemma:

[TABLE]

For the inductive step, there are three cases.

• •

If $e=f+_{b}g$, then by induction we have solutions $s_{f}$ and $s_{g}$ to $\mathcal{X}_{f}$ and $\mathcal{X}_{g}$ respectively. We now choose $s_{e}$ as follows:

[TABLE]

To see that $s_{e}$ is a solution, we use Lemma A.3. Suppose $x\in\mathcal{X}_{f}$; we derive for $\alpha\in\mathsf{At}$ that

[TABLE]

The case where $x\in\mathcal{X}_{g}$ is similar. For the second part of the claim, we derive

[TABLE]

The case where $\alpha\leq\overline{b}$ follows similarly.

• •

If $e=f\cdot g$, then by induction we have solutions $s_{f}$ and $s_{g}$ to $\mathcal{X}_{f}$ and $\mathcal{X}_{g}$ respectively. We now choose $s_{e}$ as follows:

[TABLE]

To see that $s_{e}$ is a solution to $\mathcal{X}_{e}$, we use Lemma A.3; there are three cases to consider.

• –

If $x\in X_{f}$ and $\delta_{f}(x)(\alpha)=1$, then we can derive

[TABLE]

For the second claim, suppose $\iota_{f}(\alpha)=1$; we then derive

[TABLE]

From the above and Lemma B.3 we can conclude that e=f\cdot g\equiv\operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}}_{\alpha\leq 1}\lfloor\iota_{e}(\alpha)\rfloor_{s_{e}}.

• •

If $e=f^{(b)}$, then by induction we have a solution $s_{f}$ to $\mathcal{X}_{f}$. We now choose $s_{e}$ by setting $s_{e}(x)=s_{f}(x)\cdot e$. To see that $s_{e}$ is a solution to $\mathcal{X}_{e}$, we use Lemma A.3; there are two cases:

• –

If $\delta_{f}(x)(\alpha)=1$, then we can derive

[TABLE]

For the second part of the claim, we consider three cases:

• –

If $\alpha\leq b$ and $\iota_{f}(\alpha)=1$, then derive

[TABLE]

The claim then follows by Lemma B.3. ∎

See 5.8

Proof.

We need to establish the following claims:

1. (1)

the language $\ell^{\mathcal{X}}(s)$ is deterministic for all states $s\in X$; 2. (2)

the map $\ell^{\mathcal{X}}$ is a homomorphism $\mathcal{X}\to\mathcal{L}$; and 3. (3)

the map $\ell^{\mathcal{X}}$ is the unique homomorphism $\mathcal{X}\to\mathcal{L}$.

Before we turn to proving these claims, let $L\subseteq\mathsf{GS}$ be a language and define

[TABLE]

We will need the following implication:

[TABLE]

To see that it holds, we observe that given the premise, we have

[TABLE]

We can now show the main claims:

1. (1)

We begin by showing that $\ell^{\mathcal{X}}(s)$ is deterministic for $s\in X$. Recall that a language $L$ is deterministic if, whenever $x,y$ are in the language and $x$ and $y$ agree on their first $n$ atoms, then they agree on their first $n$ actions (or lack thereof). More precisely, we need to show that

[TABLE]

where the final actions may be absent (i.e., $p_{n}=x^{\prime}=\varepsilon$ or $q_{n}=y^{\prime}=\varepsilon$). We proceed by induction on $n$. The case $n=0$ is trivially true. For $n\geq 1$, take $x$ and $y$ as above. We proceed by case distinction:

• •

If $p_{1}$ is absent, i.e., $n=1$ and $p_{1}=x^{\prime}=\varepsilon$, then by Equation 2 we must have $\delta^{\mathcal{X}}(s)(\alpha_{1})=1$ and thus cannot have $q_{1}\in\Sigma$; hence $q_{1}$ is also absent, as required.

• •

Otherwise $p_{1}\in\Sigma$ is a proper action. Then by Equation 2, there exist $t,t^{\prime}\in X$ such that:

[TABLE]

This implies $(p_{1},t)=(q_{1},t^{\prime})$ and hence

[TABLE]

Using the induction hypothesis we can now also conclude that $p_{2}=q_{2}$, …$p_{n}=q_{n}$. 2. (2)

Next, we show that $\ell^{\mathcal{X}}$ is a homomorphism: $(G\,\ell^{\mathcal{X}})\circ\delta^{\mathcal{X}}=\delta^{\mathcal{L}}\circ\ell^{\mathcal{X}}$.

If $\delta^{\mathcal{X}}(x)(\alpha)=1$, then $\alpha\in\ell^{\mathcal{X}}(x)$ and hence $\delta^{\mathcal{L}}(\ell^{\mathcal{X}}(x))(\alpha)=1$ by definition of $\delta^{\mathcal{L}}$.

If $\delta^{\mathcal{X}}(x)(\alpha)=0$, then $\alpha\not\in\ell^{\mathcal{X}}(x)$ and for all $p\in\Sigma,w\in\mathsf{GS}$, $\alpha pw\not\in\ell^{\mathcal{X}}(x)$ and hence ${\ell^{\mathcal{X}}(x)}_{\alpha p}=\varnothing$. Thus $\delta^{\mathcal{L}}(\ell^{\mathcal{X}}(x))(\alpha)=0$ by definition of $\delta^{\mathcal{L}}$.

If $\delta^{\mathcal{X}}(x)(\alpha)=\langle p,y\rangle$, then $y$ is live by normality and thus there exists a word $w_{y}\in\ell^{\mathcal{X}}(y)$. Thus,

[TABLE] 3. (3)

For uniqueness, let $L$ denote an arbitrary homomorphism $\mathcal{X}\to\mathcal{L}$. We will show that

[TABLE]

by induction on $|w|$.

For $w=\alpha$,

[TABLE]

For $w=\alpha pv$,

[TABLE]

This concludes the proof. ∎

See 6.2

Proof.

We recast this system as a matrix-vector equation of the form $x=Mx+D$ in the Kleene algebra with Tests of $n$-by-$n$ matrices over $2^{\mathsf{GS}}$; solutions to $x$ in this equation are in one-to-one correspondence with functions $R$ as above.

We now argue that the solution is unique when the system is Salomaa. We do this by showing that the map $\sigma(x)=Mx+D$ is contractive in a certain metric on ${(2^{\mathsf{GS}})}^{n}$, therefore has a unique fixpoint by the Banach fixpoint theorem.

For a finite guarded string $x\in\mathsf{GS}$, let $|x|$ denote the number of action symbols in $x$. For example, $|\alpha|=0$ and $|\alpha p\beta|=1$. For $A,B\subseteq\mathsf{GS}$, define

[TABLE]

where $2^{-\infty}=0$ by convention. One can show that $d(-,-)$ is a metric; in fact, it is an ultrametric, as $d(A,C)\leq\max d(A,B),d(B,C)$, a consequence of the inclusion $A\mathrel{\triangle}C\subseteq A\mathrel{\triangle}B\cup B\mathrel{\triangle}C$. Intuitively, two sets $A$ and $B$ are close if they agree on short guarded strings; in other words, the shortest guarded string in their symmetric difference is long. Moreover, the space is complete, as any Cauchy sequence $A_{n}$ converges to the limit

[TABLE]

For $n$-tuples of sets $A_{1},\ldots,A_{n}$ and $B_{1},\ldots,B_{n}$, define

[TABLE]

This also gives a complete metric space ${(2^{\mathsf{GS}})}^{n}$.

For $A,B,C\subseteq\mathsf{GS}$, from Lemma A.5(i) and the fact $|A\diamond B|\geq|A|+|B|$, we have

[TABLE]

from which it follows that

[TABLE]

In particular, if $D_{\alpha}(e)\neq 1$ for all $\alpha$, it is easily shown by induction on $e$ that $|x|\geq 1$ for all $x\in\llbracket e\rrbracket$, thus $|\llbracket e\rrbracket|\geq 1$, and

[TABLE]

From Lemma A.5(ii) and the fact $|A\cup B|=\min|A|,|B|$, we have

[TABLE]

from which it follows that

[TABLE]

Extrapolating to any guarded sum by induction,

[TABLE]

Putting everything together,

[TABLE]

Thus the map $\sigma$ is contractive in the metric $d$ with constant of contraction $1/2$. By the Banach fixpoint theorem, $\sigma$ has a unique solution. ∎

Lemma A.5.

Let $A\mathrel{\triangle}B$ denote the symmetric difference of $A$ and $B$. We have:

1. \edefitn(i)

$(A\diamond B)\mathrel{\triangle}(A\diamond C)\subseteq A\diamond(B\mathrel{\triangle}C)$. 2. \edefitn(ii)

$(bA_{1}\cup\overline{b}A_{2})\mathrel{\triangle}(bB_{1}\cup\overline{b}B_{2})=(bA_{1}\mathrel{\triangle}bB_{1})\cup(\overline{b}A_{2}\mathrel{\triangle}\overline{b}B_{2})$.

Proof.

(i) Suppose $x\in(A\diamond B)\setminus(A\diamond C)$. Then $x=y\diamond z$ with $y\in A$ and $z\in B$. But $z\not\in C$ since $x\not\in A\diamond C$, so $z\in B\setminus C$, therefore $x\in A\diamond(B\setminus C)$. Since $x$ was arbitrary, we have shown

[TABLE]

It follows that

[TABLE]

(ii) Using the facts

[TABLE]

we have

[TABLE]

therefore

[TABLE]

∎

Appendix B Generalized guarded union

In Section 3.2 we needed a more general type of guarded union:

See 3.5

The definition above is ambiguous in that the choice of $\beta$ is not fixed. However, that does not change the meaning of the expression above, as far as $\equiv$ is concerned.

Lemma B.1.

The operator \operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}} above is well-defined up-to $\equiv$.

Proof.

We proceed by induction on the number of atoms in $\Phi$. In the base cases, when $\Phi=\varnothing$ or $\Phi=\{\alpha\}$, the claim holds immediately as the whole expression is equal to, respectively, [math] and $e_{\alpha}$. For the inductive step, we need to show that for any $\beta,\gamma\in\Phi$:

[TABLE]

We can derive

[TABLE]

This completes the proof. ∎

The following properties are useful for calculations with \operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}}.

Lemma B.2.

Let $b,c\in\mathsf{BExp}$ and suppose that for every $\alpha\leq b$, we have an $e_{\alpha}\in\mathop{\mathsf{Exp}}$. The following then holds:

[TABLE]

Recall from above that the predicate $\alpha\leq b$ is replacing the set $\Phi=\{\alpha\mid\alpha\leq b\}$.

Proof.

We proceed by induction on the number of atoms below $b$. In the base, where $b\equiv 0$, the claim holds vacuously. For the inductive step, assume the claim holds for all $b^{\prime}$ with strictly fewer atoms. Let $\beta\in\mathsf{At}$ with $b=\beta+b^{\prime}$ and $\beta\not\leq b^{\prime}$. There are two cases.

• •

If $\beta\leq c$, then we derive

[TABLE]

where for the last step we use $bc\equiv(b^{\prime}+\beta)c=b^{\prime}c$. ∎

Lemma B.3.

For all $e\in\mathop{\mathsf{Exp}}$ and $b\in\mathsf{BExp}$, we have \operatorname*{\mathchoice{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\displaystyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{15.00015pt}{10.00012pt}{\hbox{\raisebox{0.83333pt}{\textstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{16.42873pt}{10.00012pt}{\hbox{\raisebox{0.58333pt}{\scriptstyle+}}}}}{\raisebox{-10.00012pt}{\leavevmode\resizebox{18.33354pt}{10.00012pt}{\hbox{\raisebox{0.41666pt}{\scriptscriptstyle+}}}}}}\limits_{\alpha\leq b}e\equiv be

Proof.

The proof proceeds by induction on the number of atoms below $b$. In the base, where $b\equiv 0$, the claim holds immediately. Otherwise, assume the claim holds for all $b^{\prime}\in\mathsf{BExp}$ with strictly fewer atoms than $b$. Let $\beta\in\mathsf{At}$ be such that $b=\beta\vee b^{\prime}$ and $\beta\not\leq b^{\prime}$. We then calculate:

[TABLE]

This completes the proof. ∎

Lemma B.4.

Let $b\in\mathsf{BExp}$ and suppose that for $\alpha\leq b$ we have an $e_{\alpha}\in\mathop{\mathsf{Exp}}$. The following holds:

[TABLE]

Proof.

The proof proceeds by induction on the number of atoms below $b$. In the base, where $b\equiv 0$, the claim holds immediately. Otherwise, assume that the claim holds for all $b^{\prime}\in\mathsf{BExp}$ with strictly fewer atoms. Let $\beta\in\mathsf{At}$ be such that $b=\beta\vee b^{\prime}$ and $\beta\not\leq b^{\prime}$. We then calculate:

[TABLE]

This completes the proof. ∎

Appendix C Coalgebraic Structure

C.1. Final coalgebra

We give two alternative characterizations of the final $G$-coalgebra.

C.1.1. Nonexpansive maps

For any $x\in A^{*}+A^{\omega}$, let $x|_{n}$ denote the prefix of $x$ of length $n$, or $x$ itself if the length of $x$ is less than $n$. One characterization of the final $G$-coalgebra is $(\mathcal{F},D)$, where

• •

$\mathcal{F}$ is the set of maps $f:\mathsf{At}^{\omega}\to(\Sigma^{*}\times 2)+\Sigma^{\omega}$ that are nonexpansive under the usual metric on $\mathsf{At}^{\omega}$ and $(\Sigma^{*}\times 2)+\Sigma^{\omega}$; that is, if $x,y\in\mathsf{At}^{\omega}$ and $x|_{n}=y|_{n}$, then $f(x)|_{n}=f(y)|_{n}$.

Nonexpansiveness is the manifestation of determinacy in the final coalgebra. It follows from nonexpansiveness that $\mathop{\mathsf{hd}}f(\alpha x)=\mathop{\mathsf{hd}}f(\alpha y)$ for all $x,y\in\mathsf{At}^{\omega}$. Here $\mathop{\mathsf{hd}}$ and $\mathop{\mathsf{tl}}$ are the usual head and tail functions on nonnull finite or infinite sequences.

• •

$D_{\alpha}:\mathcal{F}\to 2+\Sigma\times\mathcal{F}$, where

[TABLE]

The unique homomorphism $N:(X,\delta)\to(\mathcal{F},D)$ is defined coinductively by

[TABLE]

A state $s$ of this coalgebra is live if $N(s)(x)\in\Sigma^{*}\times\{1\}$ for some $x\in\mathsf{At}^{\omega}$.

C.1.2. Labeled trees

Another characterization of the final $G$-coalgebra is in terms of labeled trees. The nodes of the trees are represented by elements of $\mathsf{At}^{*}$ and the labels are elements of $\Sigma$ and $2$. A labeled tree is a partial map $t:\mathsf{At}^{+}\rightharpoonup\Sigma+2$ such that if $t(x)\in 2$, then $t(y)\in\Sigma$ for all nonnull proper prefixes $y$ of $x$, and $t(z)$ is undefined for all proper extensions $z$ of $x$. The root $\varepsilon$ is always unlabeled. In this characterization, the structure map is

[TABLE]

where $t@\alpha$ is the subtree rooted at $\alpha$: $(t@\alpha)(x)=t(\alpha x)$, $x\in\mathsf{At}^{+}$.

The unique homomorphism $T$ from $(X,\delta)$ to the final coalgebra is defined coinductively by

[TABLE]

C.2. Bisimilarity

Let $N$ and $T$ denote the unique homomorphisms from any $G$-coalgebra to the final $G$-coalgebra as characterized in § C.1.1 and C.1.2, respectively. Let $\sim$ denote bisimilarity (Definition 5.1).

Lemma C.1.

The following are equivalent:

1. \edefitn(i)

$s\sim t$; 2. \edefitn(ii)

$N(s)=N(t)$; 3. \edefitn(iii)

$T(s)=T(t)$.

In addition, if $X$ and $Y$ are normal, then these conditions are also equivalent to

1. \edefitn(iv)

$\ell(s)=\ell(t)$; 2. \edefitn(v)

$L(s)=L(t)$.

Proof.

The equivalence of (ii) and (iii) follows from the one-to-one correspondence between non-expansive maps $f:\mathsf{At}^{\omega}\to(\Sigma^{*}\times 2)+\Sigma^{\omega}$ and labeled trees $t:\mathsf{At}^{+}\rightharpoonup\Sigma+2$ and the observation that $N$ and $T$ assign corresponding values to any state. Given a labeled tree $t$, the corresponding non-expansive map $f$ assigns to $x\in\mathsf{At}^{\omega}$ the concatenation of the labels $t(x|_{n})$ along the path $x$. Conversely, given $f$, the corresponding $t$ assigns to $x\in\mathsf{At}^{n}$ the $n$-th symbol of $f(y)$ for any $y\in\mathsf{At}^{\omega}$ such that $x\prec y$.

To show the equivalence of (i) and (ii), we show that the kernel of $N$ is the maximal bisimulation. To show that it is a bisimulation, suppose $N(s)=N(t)$. If $\delta_{\alpha}(s)\in 2$, then for any $x$, $N(t)(\alpha x)=N(s)(\alpha x)=\delta_{\alpha}(s)\in 2$, so $\delta_{\alpha}(t)=N(t)(\alpha x)=N(s)(\alpha x)=\delta_{\alpha}(s)$.

If $\delta_{\alpha}(s)=(p,u)$, then for any $x$, $N(t)(\alpha x)=N(s)(\alpha x)=p\cdot N(u)(x)$. Thus it must be that $\delta_{\alpha}(t)=(p,v)$ for some $v$ and

[TABLE]

Since $x$ was arbitrary, $N(u)=N(v)$.

Now we show that any bisimulation refines the kernel of $N$; that is, if $s\equiv t$, then $N(s)=N(t)$. Let $\alpha x\in\mathsf{At}^{\omega}$ be arbitrary. If $\delta_{\alpha}(s)=\delta_{\alpha}(t)\in 2$, then

[TABLE]

On the other hand, if $\delta_{\alpha}(s)=(p,u)$ and $\delta_{\alpha}(t)=(p,v)$, then $u\equiv v$ and

[TABLE]

By the coinductive hypothesis, $N(u)=N(v)$, therefore

[TABLE]

Thus in all cases, $N(s)(\alpha x)=N(t)(\alpha x)$. As $\alpha x$ was arbitrary, $N(s)=N(t)$.

For (iv) and (v), see (Kozen and Tseng, 2008, §2.5). It was shown there that if the two normal $G$-automata accept the same set of finite strings, then they are bisimilar. This is because normality implies that $\ell(s)$ is dense in $L(s)$. The result of (Kozen and Tseng, 2008, §2.5) was proved under the assumption of no failures, but this assumption turns out not to be needed. Normality implies that any dead state $s$ must immediately fail under all inputs, that is, $\delta_{\alpha}(s)=0$ for all $\alpha$, thus any two such states are bisimilar. ∎

C.3. Determinacy and closure

We have discussed the importance of the determinacy property (Definition 2.2) of languages represented by GKAT expressions and $G$-automata.

In addition to the determinacy property, the languages $L(s)$ satisfy a certain topological closure property. Let $\mathsf{At}^{\omega}$ have its Cantor space topology generated by basic open sets $\{y\in\mathsf{At}^{\omega}\mid x\preceq y\}$ for $x\in\mathsf{At}^{*}$, where $\preceq$ is the prefix relation. This is the same as the metric topology generated by the metric $d(x,y)=2^{-n}$, where $n$ is the length of the longest prefix on which $x$ and $y$ agree, or [math] if $x=y$. The space is compact and metrically complete (all Cauchy sequences converge to a limit).

For $x\in\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$, let $\mathsf{at}(x)\in\mathsf{At}^{+}\cup\mathsf{At}^{\omega}$ be the sequence of atoms in $x$ and let $\mathsf{ac}(x)\in\Sigma^{*}\cup\Sigma^{\omega}$ be the sequence of actions in $x$. E.g., $\mathsf{at}(\alpha p\beta q\gamma)=\alpha\beta\gamma$ and $\mathsf{ac}(\alpha p\beta q\gamma)=pq$. For $A\subseteq\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$, let

[TABLE]

The property of $L(s)$ of interest is

Closure

A set $A\subseteq\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ satisfies the closure property if $A{\kern 1.0pt\uparrow}$ is topologically closed in $\mathsf{At}^{\omega}$.

The set $L(s){\kern 1.0pt\uparrow}$ is the set of infinite sequences of atoms leading to acceptance, starting from state $s$. This is a closed set, as the limit of any Cauchy sequence of atoms leading to acceptance—whether after a finite or infinite time—also leads to acceptance.

The set $\ell(s){\kern 1.0pt\uparrow}$ is the set of infinite sequences of atoms leading to acceptance after a finite time, starting from state $s$. This is an open set, as it is the union of basic open sets $\{x\}{\kern 1.0pt\uparrow}$ for $x\in\ell(s)$.

The set $L(s){\kern 1.0pt\uparrow}$ is the disjoint union of strings in $\mathsf{At}^{\omega}$ leading to acceptance after a finite (respectively, infinite) time:

[TABLE]

The two sets on the right-hand side are disjoint due to the determinacy property. The complement of this set is $\mathsf{At}^{\omega}\setminus L(s){\kern 1.0pt\uparrow}$, the set of strings leading to rejection after a finite time starting from $s$. Since $L(s){\kern 1.0pt\uparrow}$ is closed, its complement $\mathsf{At}^{\omega}\setminus L(s){\kern 1.0pt\uparrow}$ is open, thus a union of basic open sets. Let $B\subseteq\mathsf{At}^{*}$ be a collection of minimal-length finite strings of atoms such that

[TABLE]

Because the strings in $B$ are of minimal length, they are prefix-incomparable, thus the basic open sets $\{x\}{\kern 1.0pt\uparrow}$ for $x\in B$ are disjoint and maximal with respect to set inclusion.

C.4. Language models

The subsets of $\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ satisfying the determinacy property and the closure property form the carrier of a $G$-coalgebra $\mathcal{L}^{\prime}$. The structure map is the semantic Brzozowski derivative:

[TABLE]

Exactly one of these conditions holds by determinacy. Although this looks similar to the language model $\mathcal{L}$ of Section 5.2, they are not the same: the states of $\mathcal{L}^{\prime}$ contain finite and infinite strings, whereas the states of $\mathcal{L}$ contain of finite strings only. The models $\mathcal{L}$ and $\mathcal{L}^{\prime}$ are not isomorphic. We derive the precise relationship below.

Lemma C.2.

If $A\subseteq\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ satisfies determinacy and closure, then so does $\{x\mid\alpha px\in A\}$.

Proof.

Suppose $A$ satisfies determinacy. Let $y,z\in\{x\mid\alpha px\in A\}$ agree on their first $n$ atoms. Then $\alpha py,\alpha pz\in A$ and agree on their first $n+1$ atoms. Since $A$ satisfies determinacy, $\alpha py$ and $\alpha pz$ agree on their first $n+1$ actions. Then $y$ and $z$ agree on their first $n$ actions. As $y$ and $z$ were arbitrary, $\{x\mid\alpha px\in A\}$ satisfies determinacy.

Now suppose $A$ also satisfies closure. Let $x_{0},x_{1},\ldots$ be a Cauchy sequence in $\{x\mid\alpha px\in A\}{\kern 1.0pt\uparrow}$. Then $\alpha x_{0},\alpha x_{1},\ldots$ is a Cauchy sequence in $A{\kern 1.0pt\uparrow}$. Since $A{\kern 1.0pt\uparrow}$ is closed, the sequence has a limit $\alpha x\in A{\kern 1.0pt\uparrow}$. There must exist $z\in A$ such that $\alpha x=\mathsf{at}(z)$. By determinacy, $z$ must be of the form $\alpha py$, and $\alpha x=\mathsf{at}(z)=\alpha\mathsf{at}(y)$, thus $\mathsf{at}(y)$ is the limit of $x_{0},x_{1},\ldots~{}$. ∎

Lemma C.3.

For $A$ a state of $\mathcal{L}^{\prime}$, $L(A)=A$.

Proof.

We wish to show that $\mathsf{accept}(A,x)$ iff $x\in A$. For $\alpha\in\mathsf{At}$,

[TABLE]

For $\alpha px$,

[TABLE]

The language model $\mathcal{L}^{\prime}$ embeds in the final $G$-coalgebra $\mathcal{F}$ of § C.1.1. For $x\in\mathsf{At}^{\omega}$ and $z\in\Sigma^{*}\cup\Sigma^{\omega}$, let us write $x\|z$ for the unique $y\in\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ such that $\mathsf{at}(y)\preceq x$ and $\mathsf{ac}(y)=z$. For $A$ satisfying the determinacy and closure conditions,

[TABLE]

However, $\mathcal{L}^{\prime}$ and $\mathcal{F}$ are not isomorphic, because $\mathcal{L}^{\prime}$ does not distinguish early and late rejection: an automaton could take several transitions before rejecting or reject immediately, and the same set of finite and infinite strings would be accepted. Consequently, $L:(X,\delta^{X})\to\mathcal{L}^{\prime}$ is not a coalgebra homomorphism in general. However, normality rules out this behavior. As we show in Lemma C.4, $L$ is a homomorphism if $(X,\delta^{X})$ is normal. Thus $\mathcal{L}^{\prime}$ contains the unique homomorphic image of all normal $G$-coalgebras.

In Theorem C.5 we will identify a subcoalgebra $\mathcal{L}^{\prime\prime}$ of $\mathcal{L}^{\prime}$ that is final in the category of normal $G$-coalgebras.

Lemma C.4.

If $(X,\delta^{X})$ is normal, then the following hold:

1. \edefitn(i)

$L(s){\kern 1.0pt\uparrow}$* is the closure of $\ell(s){\kern 1.0pt\uparrow}$ in $\mathsf{At}^{\omega}$;* 2. \edefitn(ii)

$L:(X,\delta^{X})\to\mathcal{L}^{\prime}$* is a coalgebra homomorphism.*

Proof.

(i) Let $y\in L(s){\kern 1.0pt\uparrow}$. Then there exists $x\in\mathsf{GS}\cup\omega\mathchar 45\relax\mathsf{GS}$ such that either (a) $x\in\ell(s)$ and $\mathsf{at}(x)\prec y$, or (b) $x\in L_{\omega}(s)$ and $\mathsf{at}(x)=y$. In the (a) case, $y\in\ell(s){\kern 1.0pt\uparrow}$ and we are done. In the (b) case, by normality, all prefixes $z$ of $x$ have an extension $z^{\prime}$ such that $z^{\prime}\in\ell(s)$. The strings $\mathsf{at}(z^{\prime})$ are in $\ell(s){\kern 1.0pt\uparrow}$ and form a Cauchy sequence with limit $\mathsf{at}(x)=y$, thus $y$ is in the closure of $\ell(s){\kern 1.0pt\uparrow}$.

(ii) We wish to show that for any $s\in X$ and $\alpha\in\mathsf{At}$,

[TABLE]

where $GL(p,t)=(p,L(t))$, $GL(1)=1$, and $GL(0)=0$. We have

[TABLE]

so (16) holds if $\delta_{\alpha}^{X}(s)=1$. Similarly,

[TABLE]

so (16) holds if $\delta_{\alpha}^{X}(s)=0$.

Finally, if $\delta_{\alpha}^{X}(s)=(p,t)$, then by normality $t$ is live, so $\ell(t)\neq\varnothing$. But if $x\in\ell(t)$, then $\alpha px\in\ell(s)\subseteq L(s)$, so $\{x\mid\alpha px\in L(s)\}\neq\varnothing$. By definition of $\mathcal{L}^{\prime}$, $\delta_{\alpha}^{\mathcal{L}^{\prime}}(L(s))=(p,\{x\mid\alpha px\in L(s)\})$, and $L(t)=\{x\mid\alpha px\in L(s)\}$ since $\mathsf{accept}(s,\alpha px)$ iff $\mathsf{accept}(t,x)$. Thus

[TABLE]

Theorem C.5.

Let $\mathcal{L}^{\prime\prime}$ denote the subcoalgebra of $\mathcal{L}^{\prime}$ consisting of those sets $A\in\mathcal{L}^{\prime}$ such that $A{\kern 1.0pt\uparrow}$ is the closure of $(A\cap\mathsf{GS}){\kern 1.0pt\uparrow}$; that is, such that $(A\cap\mathsf{GS}){\kern 1.0pt\uparrow}$ is dense in $A{\kern 1.0pt\uparrow}$. Then $\mathcal{L}^{\prime\prime}$ is normal and final in the category of normal $G$-coalgebras.

Proof.

To show that $\mathcal{L}^{\prime\prime}$ is normal, we need to show that $\llbracket A\rrbracket$ is nonempty for all nonempty $A\in\mathcal{L}^{\prime\prime}$. Suppose $x\in A$. Either $x\in\mathsf{GS}$ itself or $\mathsf{at}(x)\in A{\kern 1.0pt\uparrow}$, in which case $\mathsf{at}(x)$ is the limit of strings in $(A\cap\mathsf{GS}){\kern 1.0pt\uparrow}$. In either case $A\cap\mathsf{GS}$ is nonempty, thus

[TABLE]

We have shown that $\mathcal{L}^{\prime\prime}$ is normal. By Lemma C.4(ii), for any normal $G$-coalgebra $(X,\delta)$, $L:X\to\mathcal{L}^{\prime}$ is a coalgebra homomorphism, and by Lemma C.4(i), its image is in $\mathcal{L}^{\prime\prime}$. By Lemma C.3, $L$ is the identity on $\mathcal{L}^{\prime\prime}$, thus $\mathcal{L}^{\prime\prime}$ is final. ∎

We conclude that $\mathcal{L}^{\prime\prime}$ is isomorphic to the language model $\mathcal{L}$ of Section 5.2: the states of $\mathcal{L}$ are obtained from those of $\mathcal{L}^{\prime\prime}$ by intersecting with $\mathsf{GS}$, and the states of $\mathcal{L}^{\prime\prime}$ are obtained from those of $\mathcal{L}$ by taking the topological closure. This establishes that $\mathcal{L}$ is isomorphic to a coequationally-defined subcoalgebra of the final $G$-coalgebra.

We remark that there is a weaker notion of normality that corresponds exactly to the language model $\mathcal{L}^{\prime}$. Let us call a state $s$ of a $G$-coalgebra an explicit failure state if all computations from $s$ lead to explicit failure after a finite time; that is, if $L(s)=\varnothing$. By König’s lemma, if $s$ is an explicit failure state, then there is a universal bound $k$ such that all computations from $s$ fail before $k$ steps. Every explicit failure state is a dead state, but the converse does not hold in general.

Let us say a $G$-coalgebra satisfies the early failure property if there are no transitions to explicit failure states. The coalgebra $\mathcal{L}^{\prime}$ satisfies the early failure property and is final in the category of $G$-coalgebras satisfying early failure.

One can identify explicit failure states by depth-first search and convert to an equivalent automaton satisfying early failure by replacing all transitions to explicit failure states with immediate failure.

Appendix D Probabilistic Models – continuous version

In this subsection, we give a more general version of the probabilistic models of Section 2.4, in terms of Markov kernels, a common class of interpretations for probabilistic programming languages (PPLs). We show that the language model is sound and complete for this class of models as well. We assume familiarity with basic measure theory.

We briefly review some basic primitives commonly used in the denotational semantics of PPLs. For a measurable space $(X,\mathcal{B})$, we let $\operatorname{\mathcal{D}}(X,\mathcal{B})$ denote the set of subprobability measures over $X$, i.e., the set of countably additive maps $\mu:\mathcal{B}\to[0,1]$ of total mass at most $1$: $\mu(X)\leq 1$. In the interest of readability, in what follows we will write $\operatorname{\mathcal{D}}(X)$ leaving the $\mathcal{B}$ implicit. A common distribution is the Dirac distribution or point mass on $x\in X$, denoted $\delta_{x}\in\operatorname{\mathcal{D}}(X)$; it is the map $A\mapsto[x\in A]$ assigning probability $1$ or [math] to a measurable set $A$ according as $A$ contains $x$.444The Iverson bracket $[\varphi]$ is defined to be $1$ if the statement $\varphi$ is true, and [math] otherwise. Denotational models of PPLs typically interpret programs as Markov kernels, maps of type $X\to\operatorname{\mathcal{D}}(X)$. Such kernels can be composed in sequence using Kleisli composition, since $\operatorname{\mathcal{D}}(-)$ is a monad.

Definition D.1 (Probabilistic Interpretation).

Let $i=(\mathsf{State},\mathcal{B},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ be a triple consisting of

• •

a measurable space $(\mathsf{State},\mathcal{B})$ with states $\mathsf{State}$ and a $\sigma$-algebra of measurable sets $\mathcal{B}\subseteq 2^{\mathsf{State}}$,

• •

for each action $p\in\Sigma$, a Markov kernel $\operatorname{\mathsf{eval}}(p)\colon\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$, and

• •

for each primitive test $t\in T$, a measurable set of states $\operatorname{\mathsf{sat}}(t)\in\mathsf{B}$.

The probabilistic interpretation of $e\in\mathop{\mathsf{Exp}}$ with respect to $i$ is the Markov kernel $\mathcal{P}_{i}\llbracket e\rrbracket\colon\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ defined as follows:

[TABLE]

It is known from (Kozen, 1985) that the limit in the definition of $\mathcal{P}_{i}\llbracket e^{(b)}\rrbracket$ exists, and that $\mathcal{P}_{i}\llbracket e\rrbracket$ is a Markov kernel for all $e$.

Theorem D.2.

The language model is sound and complete for the probabilistic model in the following sense:

[TABLE]

Proof Sketch.

The $\Rightarrow$ direction is essentially Lemma 1 of (Kozen, 1985).

• $\Rightarrow$:

For soundness, we define a map $\kappa_{i}\colon\mathsf{GS}\to\mathsf{State}\to\operatorname{\mathcal{D}}(\mathsf{State})$ that interprets guarded strings as Markov kernels as follows:

[TABLE]

We then lift $\kappa_{i}$ to languages via pointwise summation,

[TABLE]

and establish that any probabilistic interpretation factors through the language model via $\kappa_{i}$:

[TABLE]

• $\Leftarrow$:

For completeness, we construct an interpretation $i\coloneqq(\mathsf{GS},\mathcal{B},\operatorname{\mathsf{eval}},\operatorname{\mathsf{sat}})$ over the state space $\mathsf{GS}$ as follows. Let $\mathcal{B}$ be the Borel sets of the Cantor space topology on $\mathsf{GS}$.

[TABLE]

and show that $\llbracket e\rrbracket$ is fully determined by $\mathcal{P}_{i}\llbracket e\rrbracket$:

[TABLE]