Partial Reductions for Kleene Algebra
with Linear Hypotheses
January 20, 2026
Kleene algebra \((\KA)\) is an important tool for reasoning about general program equivalences, with a decidable and complete equational theory. However, \(\KA\) cannot always prove equivalences between specific programs. For this purpose, one adds hypotheses to \(\KA\) that encode program-specific knowledge. Traditionally, a map on regular expressions called a reduction then lets us lift decidability and completeness to these more expressive systems. Explicitly constructing such a reduction requires significant labour. Moreover, due to regularity constraints, a reduction may not exist for all combinations of expression and hypothesis.
We describe an automaton-based construction to mechanically derive reductions for a wide class of hypotheses. These reductions can be partial, in which case they yield partial completeness: completeness for expressions in their domain. This allows us to automatically establish the provability of more equivalences than what is covered in existing work.
Program equivalence is a high-value but generally undecidable problem. In spite of this, there are alternatives for the enterprising computer scientist, by modifying the problem or restricting its domain. One possibility is to model program behaviour using regular expressions, and then use the laws of Kleene algebra () to prove equivalence, typically with respect to a standard, language-based semantics. Kozen [1] proved that is sound and complete with respect to this semantics. Due to their connection with finite automata, equivalence of regular expressions is decidable, and so we can decide provable equivalence, too.
Unfortunately, many true equivalences are unprovable by pure , as the standard language semantics is concerned with propositional equivalences, i.e., those that hold for any interpretation of the programs’ primitive statements. In particular, this excludes the reordering of independent operations. thus trades expressive power for decidability: one can prove equivalence of propositionally similar programs, while complex equivalences remain unprovable by alone.
At the same time, often there is more program-specific information available, in the form of (in)equations of the form \(e \leq f\) for \(e,f\) regular expressions. By introducing these into the proof system as hypotheses, new equivalences become provable. Examples include the properties of Boolean assertions [2] as well as the behaviour of network packets [3] and concurrent programs [4].
By altering to make new equivalences provable, however, the system is no longer sound with respect to regular language semantics. For example, \(\la\lb\) and \(\lb\la\) have different languages, though we might add a hypothesis to say that \(\la\lb = \lb\la\). A new semantics is therefore necessary; for example in the case of Kleene algebra with tests [2] the guarded string semantics [5] was proposed. In general, significant work is required to develop such a semantics and subsequently recover soundness, completeness, and decidability — cf. [3]–[6].
To make matters worse, not every extension of admits such results. For instance, commutativity hypotheses like the aforementioned \(\la\lb = \lb\la\) can be used to encode Post’s correspondence problem as an equivalence in with hypotheses, dashing any hope of decidability [2], [7], [8]. This is unfortunate, as commutativity hypotheses are especially useful in program equivalence reasoning [2].
In recent literature a meta-theory has developed around Kleene algebra with hypotheses. The cornerstone of this approach is the hypothesis closure operation on languages [9], which gives rise to a sound-by-construction semantics of with additional equations. The goal then becomes to recover completeness and decidability, by constructing a reduction: a map on regular expressions that syntactically implements hypothesis closure, such that the regular expression semantics of a reduced expression coincides with its hypothesis-closed semantics. Existing work discusses how to construct reductions for some kinds of hypotheses [9], [10], or combine reductions for different hypotheses [11].
The Achilles heel of this approach is that a reduction must be defined on all expressions. Sometimes, however, hypothesis closure does not preserve regularity, preventing a syntactic realization of its effects; this includes the aforementioned combination of expressions and commutativity hypotheses that encode Post’s correspondence problem [2]. In such cases, the method falters, even though regularity might be preserved for some expressions. Our key idea is to define partial reductions, which in turn give completeness over their domain of definition. Using this relaxed notion of reduction, we can recover a limited form of completeness for with hypotheses in a wider variety of scenarios.
The following comprise the core technical contributions of this work:
a translation of the hypothesis closure on languages into a construction on automata, for hypotheses of the form \(e \leq w\) (where \(w\) is a word);
a proof that, when this operation produces a finite automaton, it gives rise to a reduction to \(\KA\); and
a new technique to automatically check and prove equivalence of expressions in with hypotheses in this format, limited to expressions on whose automaton our construction has finite output.
If our construction always outputs a finite automaton for a given hypothesis, our method yields a full completeness proof for extended with that hypothesis.
The remainder of this paper is organised as follows. 2 gives context and necessary definitions. 3 discusses and verifies an initial version of our construction, which is improved in 4. We conclude in 5. brevity’s sake, proofs are sketched; full arguments appear in Appendix 7. brevity’s sake, proofs are sketched; details appear in the full version [12].
Kleene algebra () models a program as a set of instructions that, depending on various factors (the input, ambient environment) may execute in different ways. The instructions of the program (e.g., print("hi") or x := 5) are
represented as letters in a finite alphabet \(\Sigma = \{ \la, \lb, \dots \}\). Each possible program execution is a finite sequence of these letters, which creates a word, or element of \(\Sigma^{*}\). The semantics of a program is then a set of words, known as a language.
By focusing on the sequences of events, abstracts from their specific meaning — equivalence in is only concerned with which actions happen, and in what order. We refer to this as propositional equivalence.
Example 1. The following programs are propositionally equivalent — they behave the same regardless of the effects of \(\test_1\), \(\pa\), \(\pb\), and \(\pc\).
\(\test_1\)
+ \(\pa\)
\(\pb\)
-
+ \(\pc\)
\(\pb\)
\(\test_1\)
+ \(\pa\)
-
+ \(\pc\)
- \(\pb\)
To represent the programs themselves, we use regular expressions. These are formed over the alphabet \(\Sigma\), and composed inductively using sequencing (\(e \cdot f\)), non-deterministic choice (\(e + f\)) and iteration (\(e^{*}\)). Together, these operations can be used to model traditional program composition — often in conjunction with so called “tests” to represent boolean control flow [2]. For instance, the latter program can be modelled as \((\test_1 \cdot \pa + \overline{\test_1} \cdot \pc) \cdot \pb\), where \(\test_{1}\) (resp.\(\overline{\test_1}\)) should be read an instruction asserting that \(\test_1\) does (resp.does not) hold, which aborts the non-deterministic branch on failure.
We formalise these operations, and their connection to languages, here. From here on, we fix a finite alphabet \(\Sigma\).
Definition 1 (Regular expressions, regular language). The set of regular expressions* \(\Exp\) is formed by the following grammar: \[e, f ::= 0 \mid 1 \mid \la \in \Sigma \mid e \cdot f \mid e + f \mid e^{*}\] Every regular expression \(e \in \Exp\) can be assigned a regular language \(\sem{e} \subseteq \Sigma^{*}\):*
Here, \(ww'\) denotes the concatenation of \(w\) and \(w'\), and \(\epsilon\) denotes the empty word.
A language \(L \subseteq \Sigma^{*}\) such that \(L = \sem{e}\) for some \(e \in \Exp\) is called regular.
We can also represent potential orderings of events using (finite) automata.
Definition 2 (Automaton). An automaton* \(\MX\) is a tuple \((X, \rightarrow, x_{\oplus}, x_0)\), in which \(X\) is a set of states, \({\rightarrow} \subseteq X \times (\Sigma \cup \{\epsilon\}) \times X\) is the transition relation, and \(x_{\oplus}, x_0 \in X\) are the final and initial state respectively. \(\MX\) is finite when \(X\) is; the collection of automata (resp.finite automata) is written \(\NA^\infty\) (resp.\(\NA\)).*
When \((x, a, x') \in {\rightarrow}\) for some \(a \in \Sigma \cup \{ \epsilon \}\), we write \(x \tr{a} x'\). Using similar notation, we can then define \(\rightarrow^{*}\) as the smallest subset of \(X \times {\Sigma^{*}} \times X\) satisfying:
An element \((x, w, x') \in {\rightarrow^{*}}\) is known as an \(\MX\)-trace* for \(w\); it is called accepting when \(x' = x_{\oplus}\), in which case we say \(x\) accepts \(w\). For a state \(x \in X\), the language accepted by \(x\) is the set of words it accepts: \[l_\MX(x) := \{ w \in \words : x \str{w} x_{\oplus} \}\] The language accepted by \(\MX\), denoted \(L_\MX\), is the language of its initial state \(x_0\).*
The intuitive link between automata and regular expressions as program specifications is legitimised by Kleene’s theorem [13], which states that any automaton can be converted into a regular expression with the corresponding language, and vice versa — thus, they describe the same set of languages.
Theorem 1 (Kleene’s theorem). A language \(L \in \langs\) is regular if and only if it is the language of a finite automaton. That is, there is an \(e \in \Exp\) such that \(\sem{e} = L\) if and only if there is a finite automaton \(\MX\) such that \(L_\MX = L\).
Kleene’s theorem allows us to move seamlessly between regular expressions and finite automata. It becomes straightforward to decide equivalence of regular expressions, by simply checking whether their automata are equivalent.
One can also reason algebraically about equivalence of regular expressions, using the rules that make up the proof system [1]. These include familiar laws such as associativity and commutativity of \(+\), in addition to the fixpoint rules that dictate the behaviour of the Kleene star.
Definition 3 (Kleene algebra). The proof system has these axioms:
where in the last two rules, we use \(e \leq f\) as a shorthand for \(e + f = f\).
If \(\KA \vdash e = f\), we say that \(e \equiv f\); equivalently, \(\equiv\) is the least congruence on \(\Exp\) satisfying the rules of . We write \(e \leqq f\) as a shorthand for \(e + f \equiv f\).
It is not too hard to show that these rules are sound for language equivalence. A landmark result by Kozen [1] shows that is complete for the standard language semantics — i.e., every true \(\sem{-}\) equivalence is provable in .
Theorem 2 (Kozen’s theorem). is sound and complete w.r.t.\(\sem{-}\): for all expressions \(e,f \in \Exp\), we have that \(\sem{e} = \sem{f}\) if and only if \(e \equiv f\).
Combining decidability of semantic equivalence for regular expressions with completeness of , it follows that equivalence in is decidable.
The key insight necessary to prove 2 is that every automaton can be thought of as a system of equations in , and that solving this system yields an expression representing the language of a state [1], [13], [14]. We will leverage this idea heavily in this paper, and so we take a moment to discuss it in depth.
Definition 4 (Solution to automaton). Let \(\MX = (X, \rightarrow, x_{\oplus}, x_0)\) be an automaton. A solution to \(\MX\) is a map \(s : X \to \Exp\) satisfying the following rules:
A least* solution \(s\) is a solution where \(s(x) \leqq s'(x)\) for all solutions \(s'\) and \(x \in X\).*
Since least solutions are unique up to \(\equiv\), we often speak of the least solution to an automaton. Solutions are connected to the languages in the following way.
Lemma 1. For any solution \(s : X \to \Exp\) to an automaton \(\MX\), we have that for every \(x \in X\), \(l_\MX(x) \sube \sem{s(x)}\). This inclusion is an equality when \(s\) is least.
Crucially, for any finite automaton a least solution exists, and we can compute it. This is typically done with a matrix representation of the transitions of the automaton that we will not cover here; we refer to [1], [14] for more information.
Lemma 2. For any finite automaton, we can construct a least solution \(s_\MX\).
Because of ’s focus on propositional equivalence, it concedes significant expressive abilities, leaving many program equivalences on the table.
examplecommWhile Suppose \(\pb\) and \(\pa\) are interchangeable in order with no effect on program behaviour, perhaps because they operate on distinct parts of memory; and \(\pb\) has no effect on whether \(\test_1\) holds. Then these programs are equivalent:
\(\pb\)
\(\test_1\)
+ \(\pa\)
\(\test_1\)
+ \(\pa\)
- \(\pb\)
Still, the corresponding regular expressions have different languages: \[\sem{ \pb \cdot {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} } \neq \sem{ {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \cdot \pb }\] It is however possible to prove equivalence of these expressions using , under assumptions about the primitives such as \(\pa \cdot \pb = \pb \cdot \pa\),\(\pb \cdot \test_1 = \test_1 \cdot \pb\),\(\pb \cdot \overline{\test_1} = \overline{\test_1} \cdot \pb\). a proof, see Appendix 6. a proof, see [12].
This example illustrates that when we represent a program as a sequence of instructions, we forget that some programs have special relationships with others. In spite of this, can still be used to prove relevant equivalences, provided we incorporate assumptions into our reasoning in the form of (in)equations. To a significant extent, the situation can be improved by identifying general subclasses of programs that satisfy additional equations, and incorporating those into the theory. A prime example is Kleene algebra with tests (\(\KAT\)) [2] which distinguishes a subset of the atomic programs as Boolean “tests”, and adds Boolean reasoning principles into the proof system. \(\KAT\) can be given a semantics in terms of guarded languages, w.r.t.which it is complete and decidable [5].
While this approach is feasible, it is an enormous amount of work to develop such a theory for an individual use-case where we have information that is not indicative of some deeper lack of expressiveness (e.g., Boolean assertions in the case of ), but is rather just useful case-specific information that we want to employ in our reasoning. Recent literature has developed a meta-theory called Kleene algebra with hypotheses [4], [9]–[11], which parameterises over the specific hypotheses used. Through this abstraction, we can ask: for which hypotheses are classical results about completeness and decidability recoverable?
Definition 5. A Kleene algebra hypothesis* is an (in)equation of two regular expressions, that is, \(e \leq f\) for some \(e,f \in \Exp\). A hypothesis is called a linear hypothesis if it is of the form \(e \leq w\) for some \(w \in \Sigma^{*}\).*
Given some set of hypotheses \(H\), the proof system augmented by the equations in \(H\) as additional axioms is called \(\KA_H\). We define \(\equiv_H\) as the smallest congruence that satisfies both the axioms of and those asserted by \(H\), with the \(-_H\) subscript extended to define \(\leqq_H\) in a similar manner to \(\leqq\).
Letters in a hypothesis \(H\) are not universally quantified! That is, if \(H = \{ \la\la \leq \la \}\), the \(\la\) is a specific letter; \(\lb\lb \leqq_H \lb\) is only true when \(\la = \lb\).
We would like to show completeness and decidability of \(\KA_H\) for as many sets of hypotheses \(H\) as possible. In doing so, we could be optimistic and hope for a “silver bullet” theorem that would work for any set of hypotheses, but that would contradict undecidability of program equivalence. Indeed, even with commutativity hypotheses, equivalence between certain expressions is undecidable [2], [7], [8]. This underscores that we cannot carelessly add axioms into .
Setting decidability and completeness aside for a moment, it is important to be clear about what semantics we are working with for \(\KA_H\). Indeed, adding any non-trivial hypotheses to the system will render it unsound with respect to the standard regular language semantics. For example, if \(H = \{ \la\lb \leq \lb\la \}\), then clearly \(\la\lb \leqq_H \lb\la\), even though \(\sem{\la\lb} \not\subseteq \sem{\lb\la}\). So, to show completeness of \(\KA_H\) (or indeed for that to mean much of anything) we first need a new semantics. Doumane et al.introduced the hypothesis closure semantics [9] for this purpose.
Definition 6. We define the one-step hypothesis closure* for hypotheses \(H\): \[H: \langs \to \langs \quad \text{given by} \quad L \mapsto L \cup \bigcup \{ u \sem{e} v : u \sem{f} v \subseteq L, e \leq f \in H \}\] Where \(u \sem{f} v = \{ uwv : w \in \sem{f} \}\), and similarly for \(\sem{e}\).*
The hypothesis closure* of \(L\), written \(H^{*}(L)\), is the smallest superset of \(L\) such that \(H(H^{*}(L)) = H^{*}(L)\). We can now define the hypothesis closure semantics: \[\sem{-}_H : \Exp \to \langs \quad\quad \text{given by} \quad\quad e \mapsto H^{*}(\sem{e})\]*
For example, the \(H\)-closure of \(\{\la\la\la\la \}\) under \(\la \leq \la\la\) is \(\{ \la, \la\la, \la\la\la, \la\la\la\la \}\). \(\KA_H\) is sound w.r.t.\(\sem{-}_{H}\) [9], but completeness is generally much harder. Methods for some hypotheses were proposed in [9], which were later developed to recover completeness of \(\KAT\) and \(\netkat\) [11]. Notably, the hypothesis closure semantics is isomorphic to the established semantics for these systems.
The approach to completeness in existing work [4], [5], [9]–[11], [15], has been to leverage 2 by realising the semantics of the expanded system in syntax. Formally, this takes the form of a reduction [11]. We call such reductions “total”, allowing for a “partial” version with the totality requirement relaxed.
Definition 7 (Reduction). A total reduction* for a set of hypotheses \(H\) is a total map \(r: \Exp \to \Exp\) such that for every \(e\) in \(\Exp\), the following hold:*
A partial reduction* for \(H\) is a partial map \(r': \Exp \rightharpoonup \Exp\) that satisfies the above two conditions for every \(e\) in its domain.*
Partial reductions give us completeness and decidability over their domain; we record this restatement of a well-known fact [4], [9] below.
Lemma 3. Let \(H\) be a set of hypotheses, and \(r\) a partial reduction for \(H\). Then \(\KA_H\) is complete (w.r.t.\(\sem{-}_H\)) and decidable over the domain of \(r\): if \(r\) is defined on \(e\) and \(f\), then \(\sem{e}_H = \sem{f}_H\) implies \(e \equiv_H f\), and \(e \equiv_H f\) is decidable. In particular, if \(r\) happens to be total, the above is true for all \(e, f \in \Exp\).
Proof. Note that by definition, for any \(f \in \Exp\), \(\sem{f} \sube \sem{f}_H\). Since \(r\) is a reduction, \(r(e) \leqq_H e\); then by soundness of \(\KA_H\), \(\sem{r(e)}_H \sube \sem{e}_H\), so \(\sem{r(e)} \sube \sem{e}_H\). Again since \(r\) is a reduction, \(\sem{e}_H \sube \sem{r(e)}\), so \(\sem{e} \sube \sem{r(e)}\). Therefore by 2, \(e \leqq r(e)\). So if \(r\) is a reduction, \(\sem{e}_H = \sem{r(e)}\) and \(e \equiv_H r(e)\).
Now let \(e,f \in \Exp\) in the domain of \(r\) be such that \(\sem{e}_H = \sem{f}_H\). Then: \[\sem{r(e)} = \sem{e}_H = \sem{f}_H = \sem{r(f)}.\] We can then apply 2 to find that \(r(e) \equiv r(f)\) — these expressions are equivalent by alone. Since \(\KA_H\) has all of the rules of , it follows that \(r(e) \equiv_H r(f)\). Lastly, we can then combine this with the other requirement for partial reductions to conclude that \(e \equiv_H r(e) \equiv_H r(f) \equiv_H f\).
As for decidability, note that the above (in combination with soundness) tells us that to decide \(e \equiv_H f\) is to decide whether \(\sem{r(e)} = \sem{r(f)}\), and equivalence of regular expressions is decidable. ◻
Various works have defined reductions tailored to specific hypotheses. For example, in [6] (see also [10]) the “contraction” hypothesis \(\la \leq \la\la\) is realised by applying “transitive closure” to automata, as detailed below.
Example 2. Let \(H = \{ \la \leq \la\la \}\). This hypothesis can quite naturally be seen as transitive closure at the automaton level. Any two states connected by a sequence of two -transitions should also be connected by just one -transition: \[\begin{tikzcd} \bullet & \bullet & \bullet \arrow["\la"', from=1-1, to=1-2] \arrow["\la", curve={height=-12pt}, dashed, from=1-1, to=1-3] \arrow["\la"', from=1-2, to=1-3] \end{tikzcd}\] For any expression \(e\), converting \(e\) to an automaton, applying this “transitive closure”, and converting back to regular expression constitutes a total reduction.
Indeed many reductions are defined through automata in some fashion: we can think of a hypothesis \(e \leq f\) as “if we can move between two states with any word from \(f\), we should be able to do the same while reading any word from \(e\)”. In contrast, working directly on expressions to define a reduction is difficult, because their inductive structure is of little help.
We therefore approach the general reduction problem by converting a regular expression \(g\) into an automaton, applying a closure construction there, and then converting the result back into an expression \(r(g)\). We can then use algebraic representations of the automata to prove that \(r(g) \leqq_H g\).
Of course, for a reduction of \(g\) to be feasible at all, \(\sem{g}_H\) needs to be a regular language; if it is not, then there is no hope of finding a sensible expression for \(r(g)\). This can happen for commutativity hypotheses.
Example 3. Let \(H := \{ \la\lb \leq \lb\la \}\). Then \(\sem{{(\la\lb)}^{*}}_H\) cannot be regular, because otherwise \(\sem{{(\la\lb)}^{*}}_H \cap \sem{\la^{*}\lb^{*}}\) would also be regular, and the latter is precisely \(\{ \la^{n}\lb^{n} : n \in \mathbb{N} \}\), which is a well-known non-regular (but context free) language.
While a total reduction, which gives a decision procedure and completeness all in one, is undoubtedly the best case scenario, it fails for certain combinations of hypothesis and expression, as in 3. However, this also means giving up on many useful equivalences, even if all of the (hypothesis-closed) languages involved are regular. Our main innovation is a technique to construct reductions for some expressions w.r.t.hypotheses \(H\), even if it might fail for others. We thereby widen the perspective beyond systems we can show to be decidable and complete via a total reduction.
We now define a notion of hypothesis closure on automata. When paired with standard algorithms converting between regular expressions and automata (e.g. [16]), this operation yields a partial reduction for the given hypothesis.
assumebigAssumption From here on, unless specified, we use a hypothesis set \(H = \{ e \leq w \}\), and an automaton \(\MX := (X, \rightarrow, x_{\oplus}, x_{0})\).
We first state the desired effect on one state. Recall that the hypothesis \(e \leq w\) enforces that if there is a word in \(L\) with \(w\) as a subword — i.e., \(uwv \in L\) — then we can replace \(w\) with any word from \(\sem{e}\), giving \(uw'v \in H(L)\) for each \(w' \in \sem{e}\). To mimic this effect on automata, we will seek out states where we can read \(w\) to reach some other state. We then add an alternate path: instead of following \(w\), step to a new automaton recognising \(\sem{e}\), and from the accepting state of that automaton, go back to any of the states we could have gone to with \(w\). \[\begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/ytelibqp.png}\label{tjsbcwlh}\end{figure}\tag{1}\]
Definition 8 (Patching). Let \(x \in X\), let \(\MZ := (Z, \rightarrow_\MZ, z_\oplus, z_0)\) be an automaton. We define the automaton \(\MX\xpatch\) (read: \(\MX\) with \(\MZ\) \(w\)-patched at \(x\)) as \((X \cup Z, \rightarrow_P, x_\oplus, x_0)\),1 where \(\rightarrow_P\) is the smallest subset of \((X \cup Z) \times (\Sigma \cup \{\epsilon\}) \times (X \cup Z)\) satisfying the following rules, where \(a \in \Sigma \cup \{ \epsilon \}\):
Patching mimics hypothesis closure w.r.t.\(H\) on automata, local to one state.
Example 4. As seen in 2, an automaton construction was used in [6] to realise the hypothesis \(\la \leq \la\la\). The hypothesis replaces any instance of the subword \(\la\la\) with \(\la\), and in automaton terms, any instance of two \(\la\)-transitions can also be traversed by a single \(\la\)-transition: a kind of “transitive closure”. As can be seen below, patching replicates this notion, up to \(\epsilon\)-removal: \[\begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/kfzcgjve.png}\label{ghdvckne}\end{figure} \quad\quad \Rightarrow \quad\quad \begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/grcxktwj.png}\label{mhlqytun}\end{figure}\] {#eq: sublabel=eq:ghdvckne,eq:mhlqytun}
Just like the one-step language closure operation is iterated to define language closure, multiple patching operations may be necessary to achieve the desired closure — either to the newly added states, or to states already in \(\MX\). The latter happens when, after patching one state, opportunities to patch other states become apparent, as shown in the example below.
Example 5. Let \(H = \{ \la \leq \lb\la \}\), and consider the expression \(\lb\lb\la\). Then, applying our patching construction one time, we obtain an automaton whose language is not yet closed: the output automaton needs to accept \(\la\), as \(\la \in \sem{\lb\lb\la}_{\la \leq \lb\la}\). So we patch again, obtaining the desired output: \[\begin{tikzcd} \circ && \textcolor{rgb,255:red,214;green,92;blue,92}{\circ} &&& \circ && \bullet \\ \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} & \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \bullet & \bullet & \bullet \\ \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \bullet & \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \bullet & \bullet \\ \textcolor{rgb,255:red,214;green,92;blue,92}{\oplus} && \oplus &&& \oplus \arrow["\lb"', from=1-1, to=2-1] \arrow["\lb"', color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=2-3] \arrow["\epsilon", from=1-6, to=1-8] \arrow["\lb"', from=1-6, to=2-6] \arrow["\la", from=1-8, to=2-8] \arrow[""{name=0, anchor=center, inner sep=0}, "\lb"', color={rgb,255:red,214;green,92;blue,92}, from=2-1, to=3-1] \arrow["\epsilon", color={rgb,255:red,214;green,92;blue,92}, from=2-3, to=2-4] \arrow[""{name=1, anchor=center, inner sep=0}, "\lb"', from=2-3, to=3-3] \arrow[""{name=2, anchor=center, inner sep=0}, "\la", color={rgb,255:red,214;green,92;blue,92}, from=2-4, to=3-4] \arrow["\epsilon", from=2-6, to=2-7] \arrow[""{name=3, anchor=center, inner sep=0}, "\lb"', from=2-6, to=3-6] \arrow["\la"', from=2-7, to=3-7] \arrow["\epsilon", from=2-8, to=3-7] \arrow["\la"', color={rgb,255:red,214;green,92;blue,92}, from=3-1, to=4-1] \arrow["\la"', from=3-3, to=4-3] \arrow["\epsilon", from=3-4, to=4-3] \arrow["\lb"', from=3-6, to=4-6] \arrow["\epsilon", from=3-7, to=4-6] \arrow[between={0.4}{0.6}, Rightarrow, from=0, to=1] \arrow[between={0.4}{0.6}, Rightarrow, from=2, to=3] \end{tikzcd}\] For each step, the part to be patched next is highlighted. Clearly, we can force patching to be necessary up to \(n\) times if we like, by using \(H = \{ \la \leq \lb\la\}\) on an automaton for the expression \(\lb^n\la\).
Of course, repeated patching opens up the possibility that we never stop patching, despite the fact that the constructed automaton must be finite to extract an expression. Indeed, no correct automaton closure construction (in the sense that it outputs an automaton for the closed language) always preserves finite automata, since hypothesis closure does not preserve regularity (cf.3).
While the construction we seek to define may need to iterate patching to reach a correct output, it should terminate where possible. Therefore, it needs a criterion to judge if a state should be patched, and indeed if its work on the automaton as a whole is done. To this end, we recall the Brzozowski derivative, as well as its generalisation, which operates on languages.
Definition 9 (Brzozowski derivative). Let \(L\) be a language, and \(w \in \words\) a word. The Brzozowski derivative* of \(L\) with respect to \(w\) is defined as follows: \[w\inv L := \{ u \in \words : wu \in L \}.\] Let \(L,M\) be languages. The generalised Brzozowski derivative (also known as the left residual) of \(L\) with respect to \(M\) is defined as follows: \[M\inv L := \bigcap_{w \in M} w\inv L = \{ v \in \words : wv \in L, \text{ for all } w \in M \}.\]*
The following characterisation can then be used to check whether an automaton requires any more patching — that is, if the languages of each of the automaton’s states are closed with respect to the hypothesis.
lemmatermCond For any automaton \(\MX\), \[\forall x \in X,\;w\inv l_\MX(x) \sube \sem{e}\inv l_\MX(x) \text{ if and only if } \forall x \in X,\;l_\MX(x) = H(l_\MX(x)).\]
Note the location of the quantifiers: the language containment holds at all states if and only if all states are hypothesis closed. This equivalence relates hypothesis-closure of the language of each state to a containment of one Brzozowski derivative in another. Since regular languages are closed under (generalised) Brzozowski derivatives, the latter is computable.
We now define the first version of our construction on automata. First we patch all states in the automaton as needed according to the criterion from [lem:term-cond]. This will imitate the action of \(H\) at every state in \(\MX\) at once.
Definition 10 (\(T_0\)). Write \(X = \{ x_0, \dots, x_{n-1} \}\); we define \(T_0(\MX) = \MX_n\), where
The languages used to check whether \(T_0\) pastes onto a state \(x_i\) are from \(\MX\), not the intermediate automata \(\MX_i\). Thus all patches occur simultaneously, and the output of \(T_0\) is independent of the order states are considered.
One application of \(T_0\) to \(\MX\) introduces new states and grows the language of existing ones, potentially necessitating further patching. Consequently, \(T_0\) must be iterated (potentially infinitely often) until a hypothesis-closed automaton arises. To rigorously define this process and formalise the notion of “building” the output of the construction, we introduce an order on automata.
Definition 11 (Automaton order). Let \(\sqsube\) be the order on automata where \[(X, \rightarrow, x_\oplus, x_0) \sqsube (X', \rightarrow', x_\oplus', x_0') \text{ iff } X \sube X', {\rightarrow} \sube {\rightarrow'}, x_0 = x_0', x_{\oplus} = x_{\oplus}'.\]
Clearly, if \(\MX \sqsube \MX'\), then \(l_{\MX}(x) \sube l_{\MX'}(x)\) for every state \(x\) in \(\MX\).
When equipped with \(\sqsube\), automata form an \(\omega\)-complete partial order, meaning any chain \(\MX_0 \sqsube \MX_1 \sqsube \cdots\) must have a limit \(\MX_*\), which is the \(\sqsube\)-least automaton such that \(\MX_i \sqsube \MX_*\) for each \(i\). This allows us to define the output of the construction as the limit of a chain — with possibly infinitely many states.
Definition 12 (\(T_0^*\)). \(T_0^{*}(\MX)\) is the limit of \(\MX \sqsube T_0(\MX) \sqsube T_0^2(\MX) \sqsube \cdots\).
With standard constructions, \(T_0^*\) lifts to a partial function on regular expressions.
Definition 13 (Candidate partial reduction: \(r_0\)). Given a regular expression \(g\), let \(\MX\) be its finite automaton. If \(T_0^*(\MX)\) is finite, then \(r_0(g)\) is the regular expression for the initial state of \(T_0^{*}(\MX)\). Otherwise, it is undefined.
For \(r_0\) to be a partial reduction, 7 tells us we need to show two things when it is defined on a regular expression \(g\). First, \(\sem{g}_H\) should be contained in \(\sem{r_0(g)}\); this boils down to showing that the \(H\)-closure of the language of an automaton \(\MX\) is contained in the (plain) language of \(T_0^*(\MX)\).
lemmaTZcorrect For every \(x \in X\), it holds that \(H^{*}(l_\MX(x)) \sube l_{T_0^{*}(\MX)}(x)\).
Proof sketch. One can more easily show the inclusion at one step: for every \(x \in X\), \(H(l_{\MX(x)}) \sube l_{T_0}(\MX)(x)\). This requires taking a word of the form \(u w v \in l_{\MX}(x)\) and verifying that \(u w' v \in l_{T_0(\MX)}(x)\) for any \(w' \in \sem{e}\), which is simply a matter of applying the criterion in [lem:term-cond] and tracing the patch as it is constructed. ◻
To validate the second part of 7, we must show that \(r_0(g) \leqq_H g\). We will achieve this using the systems of equations for the automata corresponding to these expressions, \(\MX\) and \(T_0^{*}(\MX)\). To this end, we first extend the machinery around least solutions to \(\KA_H\).
Definition 14. An \(H\)-solution* to \(\MX\) is a map \(s : X \to \Exp\) satisfying the rules from 4, but with \(\leqq_H\) instead of \(\leqq\).*
lemmasolnAutExtended The (plain) least solution \(s_\MX\) to \(\MX\) from 2 is also an \(H\)-solution to \(\MX\), and in fact it is least among all \(H\)-solutions to \(\MX\).
Proof sketch. The first claim follows because \(\leqq_H\) is weaker than \(\leqq\). One can then use the same construction used for 2 to obtain a least \(H\)-solution, but the expression constructed is the same as that obtained for the least solution. ◻
Of course, (least) \(H\)-solutions may not be (least) solutions in the sense of 4. [lem:solnAutExtended] provides leverage, relating \(H\)-solutions of an automaton to its (plain) least solution. To use this, we first show that \(T_0^{*}\) does not (up to \(H\)) perturb a solution of \(\MX\) — we only need to include the new states.
lemmaextendSolnTZ Suppose \(T_0^{*}(\MX)\) is finite, and \(s\) is a solution to \(\MX\). We can construct an \(H\)-solution \(s^{*}\) to \(T_0^{*}(\MX)\), which moreover agrees with \(s\) on all \(x \in X\).
Proof sketch. Since \(T_0^{*}(\MX)\) is finite, it is \(T_0\) applied to \(\MX\) finitely many times. We prove the claim just for \(T_0(\MX)\); the main claim then follows by induction. Let \(s_{\MZ}\) be the least solution to \(\MZ\). \(T_0(\MX)\) has \(\MZ_1, \ldots \MZ_n\) (all copies of \(\MZ\)) with state sets \(Z_1, \dots, Z_n\) \(w\)-patched on at states \(x_1, \ldots x_n\). One defines \(s^{*}\) as follows. \[s^{*}(y) = \begin{cases} s(y) & y \in X \\ s_{\MZ}(y) \cdot r_i & y \in Z_i \end{cases} \quad\quad\text{where}\quad\quad r_i := \sum_{x_i \str{w} x' }s(x')\] For a state in \(\MX\), \(s^*\) just looks at \(s\); for a state in \(\MZ_i\), it uses \(s_{\MZ}\) while accounting for the fact that we need to re-enter \(\MX\), by composing with \(r_i\).
The majority of the equations required for \(s^{*}\) to be an \(H\)-solution to \(T_0^{*}(\MX)\) (i.e., the ones resulting from the first two rules in 8) follow by definition. The only ones that remain correspond to \(\epsilon\)-transitions out to, and back from, the patched on automata (the last two rules in 8). We first look at equations resulting from the fourth rule, where an \(\epsilon\)-transition from some \(\MZ_i\) goes back into \(\MX\). Here, we must prove that \(s^{*}(x') \leqq s^{*}(z_{\oplus}^{i})\) where \(x'\) is one of the states where \(\MZ_i\) transitions back to \(\MX\). This is proved as follows: \[s^{*}(x') \equiv 1 \cdot s^{*}(x') \leqq s_{\MZ}(z_{\oplus}^i) \cdot s^{*}(x') \leqq s_{\MZ}(z_{\oplus}^i) \cdot r_i = s^{*}(z_{\oplus}^i)\] For the second-to-last step, we use the definition of \(r_i\) to observe that \(s^{*}(x') = s(x') \leqq r_i\) because \(x_i \str{w} x'\). All other steps follow by the axioms of \(\KA\), the fact that \(z_{\oplus}^i\) is the accepting state of \(\MZ_i\) with \(s_\MZ\) as solution, and the definition of \(s^{*}\).
Lastly, each equation corresponding to an \(\epsilon\)-transition from \(\MX\) out to some \(\MZ_i\) is of the form \(s^{*}(z_{0}^i) \leqq s^{*}(x_i)\), which is proved as follows: \[\label{eq:extend-soln-change-next} s^{*}(z_0^i) \equiv s_{\MZ}(z_0^i) \cdot r_i \equiv e \cdot r_i \leqq_H w \cdot r_i \leqq s(x_i) = s^{*}(x_i).\tag{2}\] For the second-to-last step, i.e., \(w \cdot r_i \leqq s(x_i)\), it suffices to show that for all \(x'\) such that \(x_i \str{w} x'\), \(w \cdot s(x') \leqq s(x_i)\). This follows directly from the definition of solution, applied in an induction on the construction of \(x_i \str{w} x'\).
All other steps in 2 follow by the definition of \(s^{*}\), the definition of \(\MZ_i\) as representing \(e\), and the (only) hypothesis in \(H\). The use of \(H\) in the middle is the reason that \(s^{*}\) is an \(H\)-solution of \(T_0(\MX)\), not necessarily a plain solution. ◻
Since the least solution of \(\MX\) is part of an \(H\)-solution for \(T_0^{*}(\MX)\), it is above the least solution for \(T_0^{*}(\MX)\), up to \(H\). Because \(r_0(g)\) is created from the least solution (and thus the least \(H\)-solution) to \(T_0^*(\MX)\), we can relate \(g\) to \(r_0(g)\).
Theorem 3. \(r_0\) is a partial reduction.
Proof. We show that for every \(g \in \Exp\) on which \(r_0\) is defined, we have \(\sem{g}_{H} \sube \sem{r_0(g)}\) and \(r_0(g) \leqq_H g\). The former follows from [lem:T0correct]: \[\sem{g}_{H} = H^{*}(L_{\MX}) \sube L_{T_0^{*}(\MX)} = \sem{r_0(g)}\] For the latter, let \(s\) be the least solution to \(\MX\), the automaton representing \(g\); by 2, \(s(x_0) \equiv g\). Let \(s'\) be the least solution to \(T_0^{*}(\MX)\); by definition, \(r_0(g) = s'(x_0)\). [lem:extend-soln-T0] extends \(s\) to an \(H\)-solution \(s^*\) for \(T_0^{*}(\MX)\). Since \(s'\) is the least solution to \(T_0^{*}(\MX)\), it is a least \(H\)-solution, allowing us to derive: \[r_0(g) = s'(x_0) \leqq_{H} s^*(x_0) = s(x_0) \equiv g \qedhere\] ◻
With our partial reduction in hand, we can now conclude decidability and completeness for the cases where it is defined, by way of 3.
Corollary 1. Let \(g,h\) be expressions for which \(r_0\) is defined. If \(\sem{g}_H = \sem{h}_H\), then \(g \equiv_H h\); moreover, the latter is decidable. Thus, if \(r_0\) is known to output finite automata for all expressions in \(\Exp\), then \(\KA_H\) is complete and decidable.
In the next section we will improve on \(T_0\), so that its output is finite in more situations. This will allow for wider domains of reduction for some hypotheses. However, we can already apply \(T_0^{*}\) to recover some known results.
For contraction hypotheses \(\la \leq \la\la\) (so-named in [4]), \(T_0^{*}\) always outputs finitely. As such, the reduction given in op.cit., and the completeness achieved as a result, are recoverable using this method. In [4], linear hypotheses (called “grounded” there) are also shown to lift to a concurrent setting. Finite output generalises to other “contraction hypotheses” \(\la \leq w\), as \(T_0\) emulates the “descendent construction” described in the proof of [17].
While \(T_0^{*}\) only operates on one hypothesis at a time, we can still make use of it for “independent” sets of hypotheses, where closure with respect to all of them at once is the same as closure w.r.t.each hypothesis individually, in some order [4], [11]. Then we can use \(T_0^{*}\) to construct a reduction from \(\KA_H\) down to \(\KA\), removing one hypothesis at a time. This is easily shown to be the case for a set of contraction hypotheses, for example \(H := \{ \la \leq \la\la,\;\lb \leq \lb\lb,\;\ldots \}\).
1 is predicated on the domain of \(r_0\), and by extension on whether \(T_0^*\) outputs a finite automaton when fed the automata for \(g\) and \(h\), but does not tell us when this might be the case. While we cannot expect \(T_0^{*}\) to always produce a finite automaton (per 3), we wish for it to do so when possible — i.e., when the hypothesis closure of the language in question is regular. Unfortunately, there are cases where \(T_0^*\) unnecessarily outputs an infinite automaton.
Example 6. Let \(H := \{ \lb\la \leq \la \}\), and consider the expression \(\la\). We can easily calculate that the desired output expression is \(\lb^{*}\la\), but \(T_0^{*}\) proceeds infinitely: \[\begin{tikzcd}[sep=scriptsize] \textcolor{rgb,255:red,214;green,92;blue,92}{\circ} & \textcolor{rgb,255:red,214;green,92;blue,92}{\oplus} && \circ & \oplus & {} && \circ & \oplus \\ & {} && \bullet & {{\color{q-red} \bullet}} & \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \bullet & \bullet & \bullet \\ &&&&&&&& \bullet & {{\color{q-red} \bullet}} & {{\color{q-red} \bullet}} \arrow["\la", color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=1-2] \arrow[""{name=0, anchor=center, inner sep=0}, draw=none, from=1-2, to=2-2] \arrow["\la", from=1-4, to=1-5] \arrow[""{name=1, anchor=center, inner sep=0}, "\epsilon"', from=1-4, to=2-4] \arrow[""{name=2, anchor=center, inner sep=0}, draw=none, from=1-6, to=2-6] \arrow["\la", from=1-8, to=1-9] \arrow[""{name=3, anchor=center, inner sep=0}, "\epsilon"', from=1-8, to=2-8] \arrow["\lb"', from=2-4, to=2-5] \arrow["\la"', color={rgb,255:red,214;green,92;blue,92}, from=2-5, to=2-6] \arrow["\epsilon"', from=2-6, to=1-5] \arrow["\lb"', from=2-8, to=2-9] \arrow["\la"', from=2-9, to=2-10] \arrow["\epsilon"', from=2-9, to=3-9] \arrow["\epsilon"', from=2-10, to=1-9] \arrow["\lb"', from=3-9, to=3-10] \arrow["\la"', color={rgb,255:red,214;green,92;blue,92}, from=3-10, to=3-11] \arrow["\epsilon"', from=3-11, to=2-10] \arrow["{T_0}", between={0.4}{0.6}, Rightarrow, from=0, to=1] \arrow["{T_0}", between={0.4}{0.6}, Rightarrow, from=2, to=3] \end{tikzcd}\] Since each step adds an \(\la\)-transition that needs patching, \(T_0^{*}\) will be infinite.
There is also a symmetric counterexample: with \(H := \{ \la\lb \leq \la \}\) applied to \(\{\la\}\), the output should be \(\la\lb^{*}\) but \(T_0^{*}\) will again produce an infinite automaton.
To deal with these cases we will improve the construction.2 Examining the target expression \(\lb^{*}\la\), our output should have a \(\lb\)-loop. Indeed, the (sub)word to be expanded, \(\la\), appears in in the expansion \(\lb\la\); on the automaton level, there is a state with \(\la\) in its language. So, rather than starting a new patch, we reset the current one to its initial state. We call this an initial state reset. \[\begin{tikzcd}[row sep=scriptsize] \circ && \oplus && \circ && \oplus \\ \bullet & \bullet & \bullet && \bullet & \bullet & \bullet \arrow["\la", from=1-1, to=1-3] \arrow["\epsilon"', from=1-1, to=2-1] \arrow["\la", from=1-5, to=1-7] \arrow[""{name=0, anchor=center, inner sep=0}, "\epsilon"', from=1-5, to=2-5] \arrow["\lb"', from=2-1, to=2-2] \arrow["\la"', from=2-2, to=2-3] \arrow[""{name=1, anchor=center, inner sep=0}, "\epsilon"', from=2-3, to=1-3] \arrow["\lb"', from=2-5, to=2-6] \arrow["\epsilon"', curve={height=6pt}, dashed, from=2-6, to=2-5] \arrow["\la"', from=2-6, to=2-7] \arrow["\epsilon"', from=2-7, to=1-7] \arrow[between={0.4}{0.6}, Rightarrow, from=1, to=0] \end{tikzcd}\] Using this new automaton, the automaton in 6 needs only one patch.
For the symmetric hypothesis \(\la\lb \leq \la\), we apply a similar tactic — in this case we search for states that have an \(\la\) path from the initial state. For such states introduce a final state reset, back to that state from the final state. \[\begin{tikzcd}[row sep=scriptsize] \circ && \oplus && \circ && \oplus \\ \bullet & \bullet & \bullet && \bullet & \bullet & \bullet \arrow["\la", from=1-1, to=1-3] \arrow["\epsilon"', from=1-1, to=2-1] \arrow["\la", from=1-5, to=1-7] \arrow[""{name=0, anchor=center, inner sep=0}, "\epsilon"', from=1-5, to=2-5] \arrow["\la"', from=2-1, to=2-2] \arrow["\lb"', from=2-2, to=2-3] \arrow[""{name=1, anchor=center, inner sep=0}, "\epsilon"', from=2-3, to=1-3] \arrow["\la"', from=2-5, to=2-6] \arrow["\lb"', from=2-6, to=2-7] \arrow["\epsilon"', from=2-7, to=1-7] \arrow["\epsilon"', curve={height=6pt}, dashed, from=2-7, to=2-6] \arrow[between={0.4}{0.6}, Rightarrow, from=1, to=0] \end{tikzcd}\] Both initial and final state resets prevent the need to patch a patched on automaton \(\MZ\), when that work could have been done before even attaching \(\MZ\) to \(\MX\). We now define the general case of adding these transitions, then use it in place of the automaton for \(e\) when patching.
Definition 15 (Saturated automaton). Let \(\MZ = (Z, \rightarrow, z_\oplus, z_0)\) be an automaton, and \(w\) a word. The \(w\)-saturation* of \(\MZ\), written \(\MZ^w\), is \((Z, \to_S, z_\oplus, z_0)\), where \(\to_S\) is the smallest subset of \(Z \times (\Sigma \times \{\epsilon\}) \times Z\) satisfying the rules:*
The latter rules correspond to initial and final state resets respectively.
Saturation adds only transitions, so it will preserve finiteness of automata. Note that the transition relation of \(\MZ^w\) is well-defined, as adding a new \(\epsilon\)-transition does not prevent any other \(\epsilon\)-transition from being added.
Example 7. We compute the \(\la\)-saturation of the automaton for \(\la\lb + \lb\la\). \[\begin{tikzcd} \circ & \bullet_2 &&& \circ & \bullet_2 \\ \bullet_1 & \oplus &&& \bullet_{1} & \oplus \arrow["\la", from=1-1, to=1-2] \arrow["\lb"', from=1-1, to=2-1] \arrow[""{name=0, anchor=center, inner sep=0}, "\lb", from=1-2, to=2-2] \arrow["\la", from=1-5, to=1-6] \arrow[""{name=1, anchor=center, inner sep=0}, "\lb"', from=1-5, to=2-5] \arrow["\lb"', from=1-6, to=2-6] \arrow["\la"', from=2-1, to=2-2] \arrow["\epsilon"', color={rgb,255:red,214;green,92;blue,92}, curve={height=6pt}, from=2-5, to=1-5] \arrow["\la"', from=2-5, to=2-6] \arrow["\epsilon"', color={rgb,255:red,214;green,92;blue,92}, curve={height=6pt}, from=2-6, to=1-6] \arrow["{\text{(\la-saturation)}}", between={0.4}{0.6}, Rightarrow, from=0, to=1] \end{tikzcd}\] The left \(\eptr\) is added because \(\bullet_1 \tr{\la} \oplus\) in the original automaton; it is an initial state reset. The right \(\eptr\) is added because \(\circ \tr{\la} \bullet_{2}\); it is a final state reset.
Incorporating the saturated automaton into the existing construction gives a revised version of \(T_0\), which patches using \(\MZ^w\) in place of \(\MZ\).
Definition 16 (\(T_H\)). Write \(X = \{ x_0, \dots, x_{n-1} \}\); we define \(T_H(\MX) = \MX_n\), with
Finally, \(T_H^{*}(\MX)\) is the limit of the chain \(\MX \sqsube T_H(\MX) \sqsube T_H^2(\MX) \sqsube \ldots\).
Definition 17 (Candidate partial reduction: \(r_H\)). Given a regular expression \(g\), let \(\MX\) be its finite automaton. If \(T_H^*(\MX)\) is finite, then \(r_H(g)\) is the regular expression for the initial state of \(T_H^{*}(\MX)\). Otherwise, it is undefined.
To show that \(r_H\) is a partial reduction, we first show \(\sem{g}_H \sube \sem{r_H(g)}\):
Lemma 4. For every \(x \in X\), it holds that \(H^{*}(l_\MX(x)) \sube l_{T_H^{*}(\MX)}(x)\).
Proof. The proof follows fairly directly from the corresponding proof for \(T_0\) ([lem:T0correct]). There, we proved that \(H(l_\MX(x)) \sube l_{T_0(\MX)}(x)\). Since \(\MZ \sqsubseteq \MZ^w\), we have \(T_0(\MX) \sqsube T_H(\MX)\); therefore, for any \(x \in X\), it follows that \(l_{T_0(\MX)}(x) \sube l_{T_H(\MX)}(x)\). Thus, the desired inclusion follows by transitivity. ◻
Now we verify that \(r_H(g) \leqq_H g\). Similarly to \(T_0\), we leverage completeness of \(\KA\) (see 2). However, the proof for \(T_0\) required that the least solution to the patched on \(\MZ\) at the initial state \(z_0\) is equivalent to \(e\). In contrast, for \(T_H\), the patched on automaton is \(w\)-saturated, so its least solution is generally above \(e\). This makes sense: the automaton was \(w\)-saturated so that it would accept more words, so its least solution should grow w.r.t.\(\leqq\). However, it should not change w.r.t.\(\leqq_H\), which is exactly what we will show: though the least solution at the initial state is not equivalent to \(e\), it is equivalent to \(e\) up to \(H\).
The proof requires that we briefly introduce the reverse operation on words, languages, etc. We write \(w^r\) for the reverse of a word \(w\); this lifts to languages: \(L^r = \{ w^r : w \in L \}\). The reverse \(g^r\) of an expression \(g\) sends \(g_1 \cdot g_2\) to \(g_2^r \cdot g_1^r\), and acts homomorphically on the other operators, so \(\sem{g^r} = \sem{g}^r\). The laws of \(\KA\) are unperturbed under reversal, so \(\KA \vdash f = g\) iff \(\KA \vdash f^r = g^r\).
The reverse automaton \(\MX^r\) refers to \(\MX\) with all transitions reversed, and initial and final states swapped; clearly, \(L_\MX^r = L_{\MX^r}\). We can then speak of reverse solutions, i.e., solutions to the reversed automaton \(\MX^r\). There is a tight relationship between solutions and reverse solutions at the initial and final states.
Lemma 5. If \(s\) and \(s^r\) are respectively the least and least reverse solution to some automaton \(\MZ\), then \(s^r(z_\oplus) \equiv {s(z_0)}^r\)
Proof. Since \(s\) is the least solution to \(\MZ\), we know by 1 that \(\sem{s(z_0)} = L_\MZ\); similarly, \(\sem{s^r(z_\oplus)} = L_{\MZ^r}\). With the observations above, we then derive: \[\sem{s^r(z_\oplus)} = L_{\MZ^r} = L_\MZ^r = \sem{s(z_0)}^r = \sem{{s(z_0)}^r}\] The claim follows from the above by 2. ◻
lemmasatPresInitSoln Suppose that \(\MZ\) is an automaton representing the expression \(e\). Let \(s^{+}\) be the least solution to the \(w\)-saturated automaton \(\MZ^w\). Then \(e \equiv_H s^{+}(z_0)\).
Proof Sketch. \(\MZ^w\) can be constructed by adding one \(\epsilon\)-transition to \(\MZ\) at a time. One can then show that when an initial state reset is added, solutions are preserved, but only up to \(H\). Similarly, when a final state reset is added, reverse solutions are preserved, up to \(H^r\), the reveresed hypothesis.
5 is then applied to relate the least reverse solution at the final state to the reverse of the least solution at the initial state, with its result expanded to \(H\) and \(H^r\)-least solutions. Therefore, at each step the least solution at the initial state does not change, up to \(H\). ◻
Now we can replay the proof strategy for [lem:extend-soln-T0] to obtain a corresponding lemma that \(T_H\) preserves \(H\)-solutions.
lemmaextendSolnTH Suppose \(T_H^{*}(\MX)\) is finite, and \(s\) is a solution to \(\MX\). We can construct an \(H\)-solution \(s^{*}\) to \(T_H^{*}(\MX)\), which moreover agrees with \(s\) on all \(x \in X\).
Proof Sketch. Define \(s^{*}\) as in the proof of [lem:extend-soln-T0], but for states in \(\MZ^w_i\) use \(s^w\), the least solution to \(\MZ^w\), rather than \(s_{\MZ}\). This map satisfies most conditions to be a solution of \(T_H(\MX)\), in particular those in \(\MZ^w_i\), even for reset transitions.
It remains to validate the conditions originating from \(\epsilon\)-transitions into and out of the patched on automata, and these can be solved in the same way as in [lem:extend-soln-T0] — with one alteration. To show that \(s^{*}(z_{0}^i) \leqq s^{*}(x_i)\) for each \(x_i\), instead of using \(s_{\MZ}(z_0^i) \equiv e\), we now use that \(s_{\MZ^w}(z_0^i) \equiv_H e\) (per 5). ◻
The proof that \(r_H\) is a partial reduction is effectively the same as that of 3, using analogous lemmas about \(T_H\), so we do not spell it out here.
theorempartialRedTH \(r_H\) is a partial reduction.
Using 3 we then conclude decidability and completeness for expressions in the domain of \(r_H\), i.e., expressions where \(T_H^{*}\) outputs a finite automaton.
Corollary 2. Let \(g,h\) be expressions for which \(r_H\) is defined. If \(\sem{g}_H = \sem{h}_H\), then \(g \equiv_H h\); moreover, the latter is decidable. Thus, if \(r_H\) is known to output finite automata for all expressions in \(\Exp\), then \(\KA_H\) is complete and decidable.
\(T_0^{*}\) never outputs a finite automaton when \(T_H^{*}\) does not, and \(T_H^{*}\) outputs finitely for the hypothesis/expression pairs from 6. But does \(T_0^*\) output a finite automaton when it can? Unfortunately, this is not the case.
Example 8. Let \(H := \{ \la\lb \leq \lb\la \}\), and consider \(\lb\la^{*}\). The hypothesis closure of this expression is \(\la^{*}\lb\la^{*}\). \(T_H^{*}\) proceeds infinitely, as sketched below: \[\begin{tikzcd} \textcolor{rgb,255:red,214;green,92;blue,92}{\circ} && \circ & \bullet && \circ & \bullet \\ &&& \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} &&& \bullet & \bullet \\ \textcolor{rgb,255:red,214;green,92;blue,92}{\oplus} && \textcolor{rgb,255:red,214;green,92;blue,92}{\oplus} & \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} && \textcolor{rgb,255:red,214;green,92;blue,92}{\oplus} & \bullet & \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} \\ &&&&&&& \textcolor{rgb,255:red,214;green,92;blue,92}{\bullet} \arrow[""{name=0, anchor=center, inner sep=0}, "\lb", color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=3-1] \arrow["\epsilon", from=1-3, to=1-4] \arrow[""{name=1, anchor=center, inner sep=0}, "\lb", from=1-3, to=3-3] \arrow["\la", from=1-4, to=2-4] \arrow[""{name=2, anchor=center, inner sep=0}, draw=none, from=1-4, to=3-4] \arrow["\epsilon", from=1-6, to=1-7] \arrow[""{name=3, anchor=center, inner sep=0}, "\lb"', from=1-6, to=3-6] \arrow["\la", from=1-7, to=2-7] \arrow["\lb", color={rgb,255:red,214;green,92;blue,92}, from=2-4, to=3-4] \arrow["\epsilon", from=2-7, to=2-8] \arrow["\lb", from=2-7, to=3-7] \arrow["\la", from=2-8, to=3-8] \arrow["\la", color={rgb,255:red,214;green,92;blue,92}, from=3-1, to=3-1, loop, in=145, out=215, distance=10mm] \arrow["\la", color={rgb,255:red,214;green,92;blue,92}, from=3-3, to=3-3, loop, in=145, out=215, distance=10mm] \arrow["\epsilon"', color={rgb,255:red,214;green,92;blue,92}, from=3-4, to=3-3] \arrow["\la", color={rgb,255:red,214;green,92;blue,92}, from=3-6, to=3-6, loop, in=145, out=215, distance=10mm] \arrow["\epsilon"', from=3-7, to=3-6] \arrow["\lb", color={rgb,255:red,214;green,92;blue,92}, from=3-8, to=4-8] \arrow["\epsilon", color={rgb,255:red,214;green,92;blue,92}, curve={height=-12pt}, from=4-8, to=3-6] \arrow["{T_H}", between={0.4}{0.6}, Rightarrow, from=0, to=1] \arrow["{T_H}", between={0.4}{0.6}, Rightarrow, from=2, to=3] \end{tikzcd}\] Since \(\lb\la\) does not appear as a path in the patched-on automaton, there is nothing to saturate. Indeed, it is only in the context of \(\MX\)* that the need to introduce a loop becomes clear. This separates this example from saturation as an operation independent from patching. A further alteration to \(T_H\) to deal with this sort of scenario is an exciting endeavour, but is left for now to future work.*
Similar to \(T_0^{*}\), \(T_H^{*}\) can be applied to “independent” sets of hypotheses. There is already significant work towards creating “modular” completeness proofs by composing reductions [11]. However, this work is orthogonal to ours — composing reductions benefits from a formula for creating new ones, which \(T_H^{*}\) offers.
These techniques can also be used to construct reductions to any system that reduces to \(\KA\), via an existing reduction. For example, as per [11], both \(\KAT\) and \(\netkat\) can be regarded as \(\KA\) with infinitely many hypotheses. Reductions introduced there can be combined with one produced by \(T_H^{*}\) to show completeness of \(\KAT\) with some hypotheses added, or decide equivalence of two \(\netkat\)-expressions with hypotheses.
We have presented a general strategy to construct reductions for Kleene algebra with a linear hypothesis, through a construction on automata. Decidability and completeness of the relevant system follow for the cases where the construction terminates. This strategy can then be used for sets of independent linear hypotheses as well, and recover known reductions in the literature [4], [11].
Hypothesis closure provides a useful canonical language semantics, but they are no substitute for the insight that a “hand-crafted” semantics provides. It remains an important task to develop these for sufficiently ubiquitous systems.
There are also sets of hypotheses that the tools given here do not cover, namely those where hypotheses directly interact with one another. Another difficulty is with general hypotheses of the form \(e \leq f\), where \(f\) is some general regular expression. It is a natural direction for future work to expand the automaton construction to deal with these uncovered cases. This would allow for creating reductions to \(\KA\), or other known-complete systems like \(\KAT\), in a wider array of Kleene algebras with hypotheses.
Another direct line of future work is studying when the construction “succeeds”, i.e., outputs a finite automaton; or indeed, when that is even possible. Characterising when the construction can succeed would allow for more precise decidability and completeness results. Commutativity hypotheses in particular have already seen investigation, in [18], where they allow for modelling “parallel actions” in the style of Mazurkiewicz traces.
Finally, a word on a possible application of this work. In [19], Braibant and Pous develop a tactic in Rocq to automatically prove equivalence of regular expressions using completeness and decidability of . The techniques introduced in this paper could be used to expand this tactic, where the user designates relevant facts in the context as hypotheses.
The authors want to thank Yde Venema for valuable comments early on, and Bas Laarakker and Sean Prendi for proofreading. This work was supported by the Dutch research council (NWO) under grant no.VI.Veni.232.286 (ChEOpS).
[ex:comm-while]. Program 3 and Program 4 are inequivalent in standard regular language semantics, but equivalent with the hypotheses: \[H = \{ \pb \cdot \pa = \pa \cdot \pb,\;\pb \cdot \test_1 = \test_1 \cdot \pb,\;\pb \cdot \overline{\test_{1}} = \overline{\test_{1}} \cdot \pb \}.\] More precisely, \[\sem{ \pb \cdot {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} } \neq \sem{ {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \cdot \pb. }\] and therefore, by soundness of , \[\pb \cdot {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \not\equiv {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \cdot \pb.\] Where on the other hand, using the hypotheses, \[\pb \cdot {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \equiv_{H} {(\test_1 \cdot \pa)}^{*} \cdot \overline{\test_{1}} \cdot \pb.\]
Proof. It’s clear to see that the two expressions have different regular language semantics, because for example, the word \(\pb \test_1 \pa \overline{\test_1}\) is in the semantics of the left expression, and not of the semantics of the right one.
On the other hand, to prove that the two expressions are equivalent, we cannot rely on completeness of (because we have added extra hypotheses) and so we must prove it directly. To this end we claim that both expressions are equivalent to an intermediate one: \[\begin{align} \pb \cdot \aloop \cdot \overline{\test_1} &\equiv \aloop \cdot \pb \cdot \aloop \cdot \overline{\test_1} \\ \aloop \cdot \overline{\test_1} \cdot \pb &\equiv \aloop \cdot \pb \cdot \aloop \cdot \overline{\test_1} \end{align}\] We already apply our hypothesis \(\pb \cdot \overline{\test_1} = \overline{\test_1} \cdot \pb\), and observe that proving the above equivalences is equivalent to proving the following, by just stripping \(\overline{\test_1}\) off the right side of all expressions: \[\begin{align} \pb \cdot \aloop &\equiv \aloop \cdot \pb \cdot \aloop \\ \aloop \cdot \pb &\equiv \aloop \cdot \pb \cdot \aloop \end{align}\] Note that since \(x^{*} \equiv 1 + xx^{*}\) for all \(x\), it follows that \(1 \leqq x^{*}\) and therefore \(1 \leqq \aloop\). In this way, the \(\leqq\) direction of both equivalences follows immediately. It remains to show that: \[\begin{align} \aloop \cdot \pb \cdot \aloop &\leqq \pb \cdot \aloop\\ \aloop \cdot \pb \cdot \aloop &\leqq \aloop \cdot \pb. \end{align}\] We begin with the former. Recall the following axiom: \[e + f \cdot g \leq g \Longrightarrow f^{*} \cdot e \leq g.\] If we identify \(f = (\test_1 \cdot \pa)\) and \(e,g = \pb \cdot \aloop\), we see that to prove the above it suffices to show that: \[\pb \cdot \aloop + (\test_1 \cdot \pa) \cdot \pb \cdot \aloop \leqq \pb \cdot \aloop\] By idempotence, this is equivalent to showing that: \[(\test_1 \cdot \pa) \cdot \pb \cdot \aloop \leqq \pb \cdot \aloop.\] To show this, we reason: \[\begin{align} (\test_1 \cdot \pa) \cdot \pb \cdot \aloop &\equiv_H \pb \cdot (\test_1 \cdot \pa) \cdot \aloop \\ &\leqq \pb \cdot \aloop \end{align}\] where the first step follows by the hypotheses that \(\pb\) commutes with the test \(\test_1\) and the action \(\pa\). The inequality follows because \(\aloop \equiv 1 + (\test_1 \cdot \pa) \cdot \aloop\) (axiom), and so we have \((\test_1 \cdot \pa) \cdot \aloop \leqq \aloop\).
Now it remains to prove: \[\aloop \cdot \pb \cdot \aloop \leqq \aloop \cdot \pb\] The proof proceeds in a symmetric fashion. Recall the axiom: \[e + f \cdot g \leq f \Longrightarrow e \cdot g^{*} \leq f.\] Identifying \(g = (\test_1 \cdot \pa)\) and \(e,f = \aloop \cdot \pb\), it suffices to prove: \[\aloop \cdot \pb + \aloop \cdot \pb \cdot (\test_1 \cdot \pa) \leq \aloop \cdot \pb.\] By idempotency, this is equivalent to proving: \[\aloop \cdot \pb \cdot (\test_1 \cdot \pa) \leq \aloop \cdot \pb.\] We recall the fact that \((\test_1 \cdot \pa) \cdot \aloop \leqq \aloop\) and complete the proof: \[\begin{align} \aloop \cdot \pb \cdot (\test_1 \cdot \pa) &\equiv_H \aloop \cdot (\test_1 \cdot \pa) \cdot \pb \\ &\leqq \aloop \cdot \pb. \end{align}\] ◻
We now present proofs of the lemmas from the main text, and remind the reader of the assumption below, made at the beginning of 3.
Proof. Suppose that for every \(x \in X\), \(w\inv l_{\MX}(x) \sube \sem{e}\inv l_{\MX}(x)\). Let \(x \in X\); we want to show that \(l_{\MX}(x) = H(l_{\MX}(x))\). The \(\sube\) direction follows by the definition of \(H\). For the \(\supe\) direction, we instantiate 6: \[H(l_{\MX}(x)) := l_{\MX}(x) \cup \bigcup \{ u \sem{e} v : u w v \in l_{\MX}(x) \}\] so it suffices to show that if \(u w v \in l_{\MX}(x)\), then \(u \sem{e} v \sube l_{\MX}(x)\). To this end, take \(uw'v\) where \(w' \in \sem{e}\) and \(uwv \in l_{\MX}(x)\). Let \(x'\) be a state reached after \(u\) has been read in any accepting trace of \(uwv\). Naturally, \(wv \in l_{\MX}(x')\), and so \(v \in w\inv l_{\MX}(x')\). Because \(w\inv l_{\MX}(x') \sube \sem{e}\inv l_{\MX}(x')\), we have \(v \in \sem{e}\inv l_{\MX}(x')\), whence \(w'v \in l_{\MX}(x')\). Since we could read \(u\) while moving from \(x\) to \(x'\), \(uw'v \in l_{\MX}(x)\).
For the other direction, suppose that for every \(x \in X\), \(l_{\MX}(x) = H(l_{\MX}(x))\). We want to show that \(w\inv l_{\MX}(x) \sube \sem{e}\inv l_{\MX}(x)\). Let \(v \in w\inv l_{\MX}(x)\), so \(wv \in l_{\MX}(x)\). By the definition of \(H\), \(\sem{e} v \sube H(l_{\MX}(x))\). But we assumed that \(H(l_{\MX}(x)) = l_{\MX}(x)\), so \(\sem{e} v \sube l_{\MX}(x)\), and finally \(v \in \sem{e}\inv l_{\MX}(x)\). ◻
Proof. It suffices to prove the claim for one application of \(H\) and \(T_0\), i.e.: \[H(l_\MX(x)) \sube l_{T_0(\MX)}(x).\] To this end, we prove that when \(uwv \in l_\MX(x)\) and \(w' \in \sem{e}\), \(uw'v \in l_{T_0(\MX)}(x)\). If \(uw'v \in l_{\MX}(x)\) then we’re done, so assume it is not. We dissect the trace witnessing that \(uwv \in l_\MX(x)\) as follows: \[x \str{u} y \str{w} y' \str{v} x_\oplus.\] Note that \(wv \in l_\MX(y)\), and by our assumption above, \(w'v \not\in l_\MX(y)\) — otherwise we could sequence it after \(u\) and have an \(\MX\)-trace from \(x\). This tells us that \(l_{\MX}(y)\) is not \(H\)-closed, and thus, by [lem:term-cond], \(w\inv l_\MX(y) \not\sube \sem{e}\inv l_\MX(y)\). This being the case, in \(T_0(\MX)\) the state \(y\) will be \(w\)-patched. That is, for some \(i\), \(\MX_{i+1} = \MX_i\patch{y}\). We can now produce a new \(\MX_{i+1}\) trace: \[x \str{u} y \eptr z_0^i \str{w'} z_{\oplus}^i \eptr y' \str{v} x_\oplus\] to see that \(uw'v \in l_{\MX_{i+1}}(x)\). Finally, we observe that patching is inflationary with respect to \(\sqsube\), since it only adds states and transitions. Therefore \(\MX_i \sqsube \MX_n = T_0(\MX)\). As a result, \(uw'v \in l_{T_0(\MX)}(x)\), and we are done. ◻
Proof. Let \(s\) be a (least) solution to \(\MX\). For \(s\) to be an \(H\)-solution to \(\MX\), it must satisfy the same equations, but with \(\leqq_H\) in place of \(\leqq\). Since \(\KA_H\) contains all of the axioms of \(\KA\), this is easily seen to be the case.
To show that any least solution is also a least \(H\)-solution, we refer to the proof of 2 as seen in e.g. [1], [14]. In this proof, a solution is constructed, and shown to be least. We can use the same strategy with \(\leqq_H\) in place of \(\leqq\) to construct a least \(H\)-solution. However, in doing so, the very same map from \(X\) to \(\Exp\) will be produced. Therefore, this least solution is a least \(H\)-solution. Similar proofs can also be found in [20]. ◻
Proof. Since \(T_0^{*}(\MX)\) is a finite automaton, \(T_0^{*}(\MX) = T_0^n(\MX)\) for some \(n \in \N\). Therefore, we only concern ourselves with one application of \(T_0\), and we can re-apply the result to each successive operation of \(T_0\).
By definition, \(T_0(\MX)\) consists of \(\MX\) with finitely many copies of the automaton \(\MZ\), representing \(\sem{e}\), patched on. We will call these automata \(\MZ_1, \ldots \MZ_n\) and the states to which they are \(w\)-patched \(x_1, \ldots x_n\). The state set \(T_0(X)\) partitions into \(X \cup Z_1 \cup \cdots \cup Z_n\).
All states in \(\MX\) except \(x_1, \dots, x_n\) have transitions to other states in \(\MX\) exclusively, whereas the \(x_i\) also transition to their corresponding \(z_0^i\). Similarly, the states of \(\MZ_i\) only have outgoing transitions to other \(\MZ_i\) states (with the same \(i\)), except for the \(z_\oplus^i\) which also has an \(\epsilon\)-transition back to all \(x_i'\) such that \(x_i \str{w} x_i'\). In total, \(s': X \cup Z_1 \cup \cdots \cup Z_n \to \Exp\) is an \(H\)-solution to \(T_0(\MX)\) if it satisfies:
Where \(a \in \Sigma \cup 1\), implicitly interpreting 1 as \(\epsilon\) in transitions. We will now extend \(s\), the least solution to \(\MX\), into an \(H\)-solution for \(T_0(\MX)\). Let \(s_{\MZ}\) be the least solution to \(\MZ\), and thus \(\MZ_i\) for every \(i \leq n\). We define \(s^{*}: X \cup Z_1 \cup \cdots \cup Z_n \to \Exp\) as follows: \[s^{*}(y) = \begin{cases} s(y) & y \in X \\ s_{\MZ}(y) \cdot r_i & y \in Z_i \end{cases} \quad\quad\text{where}\quad\quad r_i := \sum_{x_i \str[\MX]{w} x' }s(x')\] By definition, \(s^{*}\) agrees with \(s\) for all \(x \in X\), so it remains to show that \(s^*\) satisfies the rules above. Since \(s^{*}\) coincides with \(s\) on all states in \(\MX\), the first two rules hold for \(\leqq\), and hence for \(\leqq_H\). The third rule comes down to showing that, if \(z \str[\MZ_i]{a} z'\), then \(a \cdot s_\MZ(z') \cdot r_i \leqq_H s_\MZ(z) \cdot r_i\), which follows by the fact that \(s_\MZ\) is a solution to \(\MZ_i\), and monotonicity of sequential composition.
It remains to show that, for each \(1 \leq i \leq n\), we have \(s^*(z_0^i) \leqq_H s^*(x_i)\). By definition of \(s^*\) and \(r_i\) it suffices to show that, for any \(i\) and \(x'\) with \(x_i \str[\MX]{w} x'\): \[s_{\MZ_i}(z_0^i) \cdot s(x') \leqq_H s(x_i).\] Now since \(\MZ_i\) is an automaton representing \(\sem{e}\) and \(z_0^i\) is its initial state, \(s_{\MZ_i}(z_0^i) \equiv e\) (by 2). Applying this fact and our hypothesis \(e \leq w\), \[s_{\MZ_i}(z_0^i) \cdot s(x') \leqq e \cdot s(x') \leqq_H w \cdot s(x') \leqq s(x_i)\] where the final containment can be argued using the fact that \(s\) is a solution to \(\MX\), by induction on the construction of the trace \(x_i \str[\MZ]{w} x'\). ◻
Proof. Suppose that \(s\) is an \(H\)-solution to \(\MZ\) satisfying \(s(z_0) \equiv_H e\). Let \(\MZ_f\) be an automaton obtained by adding an initial state reset to some state \(z\) in \(\MZ\). Then we claim that \(s\) is an \(H\)-solution to \(\MZ_f\) as well. Given that \(\MZ_f\) is just \(\MZ\) with one more \(\epsilon\)-transition, the majority of the necessary equations are satisfied immediately. The only non-trivial equation comes from the new \(\epsilon\)-transition: \[s(z_0) \leqq_H s(z).\] Because the \(\epsilon\)-transition \(z \eptr z_0\) was added as an initial state reset, \(z \str{w} z_\oplus\). Since \(s\) is an \(H\)-solution, it follows (by an easy induction) that \(w \leqq_H s(z)\). Stringing these together with our hypothesis \(e \leq w\), we see that: \[s(z_0) \equiv_H e \leqq_H w \leqq_H s(z)\] as desired. So adding an initial state reset preserves the \(H\)-solutions of \(\MZ\).
Now we make the symmetric claim: if \(s^r\) is a reverse \(H^r\)-solution to \(\MZ\) satisfying \(s^r(z_\oplus) \equiv_{H^r} e^r\) where \(H^r = \{ e^r \leq w^r \}\), and \(\MZ_b\) is an automaton obtained by adding a final state reset to some state \(z\) in \(\MZ\), then \(s^r\) is a reverse \(H^r\)-solution to \(\MZ_b\) as well. As with the first case, the majority of the requiremed equations are satisfied by definition. We are left needing to prove: \[s^r(z_\oplus) \leqq_{H^r} s^r(z)\] and we prove it in a symmetric way. Since the final state reset \(z_{\oplus} \eptr z\) was added, \(z_0 \str{w} z\), so \(w^r \leqq_{H^r} s^r(z)\). We then derive as follows: \[s^r(z_\oplus) \equiv_{H^r} e^r \leqq_{H^r} w^r \leqq_{H^r} s^r(z).\] So adding a final state reset preserves reverse \(H^r\)-solutions for the automaton \(\MZ\). We now combine these two results to prove the lemma.
Our starting point is \(\MZ\), an automaton representing \(e\). Let \(\MZ_0 := \MZ\), and \(\MZ_1, \MZ_2, \ldots \MZ_n\) be individual steps of adding either type of reset transition so that \(\MZ_n = \MZ^w\). Let \(s_0, s_1, s_2, \ldots s_n\) be the least solutions to these automata, so \(s_n = s^{+}\). We claim that for all \(i \leq n\), \(s_i(z_0) \equiv_H e\). We proceed by induction. The base case is clear: \(s_0\) is the least solution to \(\MZ_0 = \MZ\) which is by definition the automaton representing the expression \(e\), so by 1 \(\sem{s(z_0)} = \sem{e}\) and by 2, \(s(z_0) \equiv e\), allowing us to conclude that \(s(z_0) \equiv_H e\).
For the inductive step, we assume that \(e \equiv_H s_i(z_0)\) where \(s_i\) is the least solution to \(\MZ_i\). Now to obtain \(\MZ_{i+1}\), we either add an initial state reset or a final state reset. Suppose that we added an initial state reset. Then we proved above that this means \(s_i\) is also an \(H\)-solution to \(\MZ_{i+1}\). Therefore \(s_{i+1}(z_0) \leqq_H s_i(z_0)\). Since \(\MZ_i \sqsubseteq \MZ_{i+1}\), we also have \(s_i(z_0) \leqq_H s_{i+1}(z_0)\), meaning that: \[s_{i+1}(z_0) \equiv_H s_i(z_0) \equiv_H e.\] Now suppose to get from \(\MZ_i\) to \(\MZ_{i+1}\), we added a final state reset. Let \(s_i^r, s_{i+1}^r\) be the least reverse solutions to these automata. We use reasoning symmetric to the previous case to find that \(s_{i+1}^r(z_\oplus) \equiv_{H^r} s_i^r(z_\oplus)\). Taking a proof of this equivalence, we can then revert all of the expressions (including the hypotheses) to find that \({s_{i+1}^r(z_\oplus)}^r \equiv_H {s_i^r(z_\oplus)}^r\). Using 5, we can then conclude: \[s_{i+1}(z_0) \equiv {s_{i+1}^r(z_\oplus)}^r \equiv_H {s_i^r(z_\oplus)}^r \equiv s_i(z_0) \equiv_H e. \qedhere\] ◻
Proof. The proof largely follows the structure of [lem:extend-soln-T0], but with \(T_H\) instead of \(T_0\), and using \(s_{\MZ_i^w}\) (the least solution to \(\MZ^w_i\)) rather than the least solution to \(\MZ_i\). At the very end, where an appeal to 2 is made to use that \(s_{\MZ_i}(z_0^i) \equiv e\), we instead use [lem:satPresInitSoln] to find that \(s_{\MZ_i^w}(z_0^i) \equiv_H e\); this also suffices to make the final derivation go through. ◻
Proof. To show that \(r_H\) is a partial reduction, we must show for all \(g \in \Exp\) on which it is defined the following two properties hold:
The former follows from 4: if \(\MX\) is the automaton representing \(g\), then \(T_H^{*}(\MX)\) is finite (since \(r_H\) is defined on \(g\)), and: \[\sem{g}_{H} = H^*(\sem{g}) = H^{*}(L_{\MX}) \sube L_{T_H^{*}(\MX)} = \sem{r_H(g)}.\] For \(r_H(g) \leqq_H g\), let \(s\) be the least solution to \(\MX\). By 2, \(s(x_0) \equiv g\). Similarly let \(s'\) be the least solution to \(T_H^{*}(\MX)\); by definition, \(s'(x_0) = r_H(g)\). [lem:extend-soln-T0] gives an \(H\)-solution \(s^*\) to \(T_H^{*}(\MX)\) such that \(s^*(x) = s(x)\) for every \(x \in X\). Since \(s'\) is the least solution to \(T_H^{*}(\MX)\), it is a least \(H\)-solution as well: \[r_H(g) = s'(x_0) \leqq_{H} s^*(x_0) = s(x_0) \equiv g. \qedhere\] ◻
Without loss of generality, the state sets \(X\) and \(Z\) are assumed to be disjoint.↩︎
The reader may think to fix this by first “saturating” the hypothesis itself, to skip redundant steps; in the above case, obtaining \(\lb^{*}\la \leq \la\). While this works in principle, it is circular: to calculate a hypothesis closed expression, we construct the automaton; to do that, we calculate a hypothesis closed expression. Instead, we seek to create a similar effect on the automaton level, where we can be certain it will terminate.↩︎