Partial Reductions for Kleene Algebra with Linear Hypotheses

Liam Chung; Tobias Kapp\'e

REVIEW 2 major objections 3 minor 24 references

Partial Reductions for Kleene Algebra with Linear Hypotheses

T0 review · 2 major / 3 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper shows that for a hypothesis of the form e ≤ w in Kleene algebra, an automaton-based saturation construction yields a partial reduction: on expressions where the construction terminates, hypothesis-closed language equivalence matc

desk verdict Useful construction for partial reductions in KA with linear hypotheses, but the main proof has a repairable induction gap in Lemma 3.15 (and its TH analogue). read the letter →

arxiv 2601.14114 v2 pith:WRQPCQC5 submitted 2026-01-20 cs.PL

Liam Chung , Tobias Kappé This is my paper · ORCID

classification cs.PL MSC 68Q4568Q7003B2503B70

keywords Kleenealgebrahypotheseslinearpartialreductionsautomatacompletenessdecidabilitysaturation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper attacks a known bottleneck: adding program-specific hypotheses to Kleene algebra (KA) destroys completeness and decidability, and the standard fix—a total reduction—is often impossible because hypothesis closure can turn regular languages non-regular. The authors propose partial reductions instead: maps that only need to work on some expressions. They build such partial reductions automatically for linear hypotheses of the form e ≤ w, using an automaton construction that repeatedly 'patches' an automaton with a copy of an automaton for e. When the construction terminates, it yields an expression whose regular language is exactly the hypothesis-closed language of the original, and the two are provably equal up to the hypothesis. This gives completeness and decidability on the domain of termination, which is wider than what total-reduction methods cover.

What carries the argument

The central mechanism is the 'patching' operation: given an automaton X and a state x, the construction attaches a fresh automaton Z for the expression e, adding an ε-transition from x into Z's start state and ε-transitions from Z's accepting state back to every state reachable from x by reading w. The improved version uses the w-saturated automaton Z^w, which adds initial-state and final-state reset transitions so that loops introduced by the hypothesis do not force infinite re-patching. Iterating this patching, using a Brzozowski-style derivative test to decide which states need patching, yields the chain whose limit is the reduced automaton. The proof that this is a reduction relies on le

What would settle it

Run the construction on a concrete case such as H = {ba ≤ a} and expression a, where T_H terminates: check whether the language of the final automaton equals the hypothesis-closed language {b^k a : k ≥ 0}. Any mismatch would refute the reduction claim. More generally, search for a finite terminating T_H output where r_H(g) is not provably ≤_H g, which would expose a failure of the iterated extension lemma.

Watch

Extended reading notes

Core claim

The central claim is that for any linear hypothesis e ≤ w, the automaton construction T_H (patching with the w-saturated automaton for e, iterated to its limit) defines a partial reduction r_H. Concretely, whenever T_H terminates finitely on the automaton of an expression g, two properties hold: the hypothesis-closed language of g is contained in the regular language of r_H(g), and r_H(g) is provably below g in KAH. Consequently, for any two expressions g and h on which r_H is defined, equality of their hypothesis-closed languages implies g ≡_H h, and this equivalence is decidable. If T_H terminates on all expressions, this yields full completeness and decidability for KAH.

Load-bearing premise

The argument assumes that the one-step extension lemma—turning a solution of an automaton into an H-solution of its patched successor—can be applied repeatedly along the infinite chain of patched automata, even when the intermediate automaton already contains patched-in states; the paper only proves the one-step version for plain solutions, and the iterated version is not stated.

Editorial extensions

If this is right

For any linear hypothesis where the construction always terminates, KAH becomes complete and decidable for all expressions.
The construction recovers known reductions for contraction hypotheses such as a ≤ aa, giving a uniform explanation for existing completeness results.
For sets of 'independent' hypotheses, the reduction can be applied hypothesis-by-hypothesis, chaining reductions down to plain KA.
The technique lifts to any system that reduces to KA, such as Kleene algebra with tests or NetKAT, potentially extending them with additional linear hypotheses.
The termination domain of r_H precisely identifies a broad class of expressions on which hypothesis-closed equivalence is decidable, even when no total reduction exists.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A clear next step is to characterize exactly when T_H terminates; if that characterization matches a regularity criterion for hypothesis-closed languages, the method would be optimal within its class of hypotheses.
The saturation idea is local to the patched automaton; Example 4.12 suggests a context-sensitive refinement—saturating with respect to the host automaton's paths—might handle hypotheses that currently cause infinite iteration.
The partial-reduction framework could be used as a proof-assistant tactic: a user supplies a linear hypothesis, the tactic runs the automaton construction, and if it terminates, the equivalence question reduces to a decidable regular-language check.
Because the construction yields syntactic reductions, it could help synthesize witnesses: when two expressions are provably equivalent under H, the reduced expressions give an explicit KA proof bridge.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The core idea here is good: define partial reductions so you get completeness and decidability on a subdomain even when a total reduction is impossible, and derive them via an automaton patching construction for linear hypotheses e≤w. The saturation variant (TH) is a real improvement over the naive T0, and the examples (ba≤a, ab≤ba) are clear and informative. The paper is honest about where it succeeds and where it fails, and it connects well to the existing total-reduction literature of Doumane et al. and Pous et al. If the proof gap below is fixed, the conditional completeness/decidability results are a solid within-subfield contribution.

The soft spot is exactly where the reader’s report points. Lemma 3.15 proves that a plain solution of X can be extended to an H-solution of T0(X). The proof then says the finite chain X ⊑ T0(X) ⊑ ... ⊑ T0^n(X) is handled by induction. That induction does not go through as written: after one step you have an H-solution of T0(X), not a plain solution, so you cannot reapply the lemma at T0(X). The appendix repeats the same assertion rather than proving the generalized claim. The issue transfers verbatim to Lemma 4.9 for TH, and therefore to Theorem 4.10 and Corollary 4.11, so the central inequality rH(g) ≤H g is not established as the proof stands. This looks repairable: you should generalize the lemma to take an H-solution and produce an H-solution, weakening the key step w·s(x') ≤ s(xi) to ≤H. But it is currently a real gap in a load-bearing result. The lack of a termination characterization is acknowledged as future work, which is fine; that is a limitation, not an error.

Who is this for? People working on Kleene algebra with hypotheses, completeness, and decidability, and possibly the Rocq tactic community. It deserves a serious referee: the idea is novel, the exposition is good, and the gap is likely fixable without changing the shape of the construction. I would not cite the main theorem yet, but I would probably cite the construction after a repair.

Recommendation: send this to peer review, but tell the authors the proof of Lemma 3.15 / Lemma 4.9 needs to be repaired before the paper can be accepted. This is exactly the kind of preprint a good referee should see.

Referee Report

2 major / 3 minor

Summary. This paper develops an automaton-based method to construct partial reductions for Kleene algebra with a linear hypothesis e≤w. Given an expression g, one builds a finite automaton, repeatedly patches it (T0) or patches with a w-saturated automaton for e (TH), and if the chain stabilizes finitely, reads off a regular expression r(g). The authors prove that JgK_H ⊆ Jr(g)K and r(g) ≤H g, and use the standard reduction argument to obtain completeness and decidability of KAH on the domain of r. The saturated construction is shown to terminate in cases where the basic one does not, and the method recovers known reduction-based completeness results.

Significance. The partial-reduction viewpoint is a useful and honest relaxation: it gives completeness/decidability for individual expressions even when hypothesis closure is not globally regular. The constructions are algorithmic and the paper provides concrete examples and detailed appendix proofs. If the central preservation lemmas are correctly established, the main theorems are valuable and would meaningfully extend the toolkit for Kleene algebra with hypotheses. The main caveat is that Lemma 3.15 (and the analogous Lemma 4.9) contain a genuine, though apparently local, induction gap; the core ideas look sound and repairable.

major comments (2)

[Appendix B, Lemma 4.9 / Theorem 4.10] The proof says 'we only concern ourselves with one application of T0, and we can re-apply the result to each successive operation of T0.' This induction is not justified. The one-step construction turns a plain solution s of X into an H-solution s* of T0(X). To re-apply the lemma at T0(X), one would need a plain solution of T0(X); no such solution is produced, and s* is generally not plain because the ε-transition equation from x_i to z_i^0 is proved only up to H via e≤w. Thus r0(g) ≤H g in Theorem 3.16 is not established as written. The gap is repairable: state and prove the one-step extension for an arbitrary H-solution (checking all inequalities in KAH), then iterate along the chain.
[Appendix B, Lemma 4.9 / Theorem 4.10] Lemma 4.9 is said to 'largely follow' Lemma 3.15, so it inherits the same induction gap. Since Theorem 4.10 and Corollary 4.11 are the central results for the saturated construction, this is a load-bearing omission. The same repair works: prove a one-step extension from H-solutions to H-solutions for TH, replacing the use of s_{Z_i}(z_i^0) ≡ e by Lemma 4.8's s_{Z^w_i}(z_i^0) ≡H e, and then iterate. As written, the main theorem that rH is a partial reduction, and hence the partial completeness/decidability corollary, is not fully proved.

minor comments (3)

[Theorem 4.10 proof] The proof refers to 'Lemma 3.15' for the extension to T*_H(X); this should be Lemma 4.9.
[Definition 4.4] For TH, the patching condition is stated using l_X(x_i) from the original automaton, but no analogue of Remark 3.8 is given. A brief remark that TH also patches all states simultaneously would prevent confusion.
[Lemma 3.12 / Lemma 4.6] The induction from the one-step inclusion H(l_X(x)) ⊆ l_{T0(X)}(x) to the iterated statement H*(l_X(x)) ⊆ l_{T*}(x) is only announced. It is routine (apply the one-step property to each automaton in the chain and use monotonicity of H), but spelling it out would make the appendix self-contained.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the reduction theorem is proved from external completeness/soundness results, not from its own conclusion.

full rationale

The central derivation is self-contained. r0/rH is defined by iterated automaton patching, and the two defining properties of a partial reduction are proved directly: Lemma 3.12 and Lemma 4.6 establish the closure inclusion by word-trace arguments, while Lemma 3.15 and Lemmas 4.8–4.9 establish r(g)≤H g using Kozen's completeness theorem, the least-solution machinery, and the hypothesis e≤w itself. None of these steps assumes JgKH = JhKH or the target equivalence g≡H h. Kozen's theorem and soundness of J·KH are cited as external literature facts; the self-citations that occur ([8], [9], [10]) appear in examples, 'similar proofs' remarks, and recovery of known reductions, and are not load-bearing for Theorem 4.10 or Corollary 4.11. The paper even explicitly identifies and rejects a would-be circular shortcut of saturating the hypothesis itself, instead performing saturation at the automaton level. The genuine weakness is a proof gap, not circularity: in Appendix B, Lemma 3.15, the proof says 'we can re-apply the result to each successive operation of T0', but the extension it constructs is only an H-solution, not a plain solution, so the induction as written is incomplete; the same issue transfers to Lemma 4.9. This is an omitted justification about iteration, not a dependence of the theorem on its own conclusion, so it is a correctness risk outside the circularity score.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No free parameters or invented entities. The central derivation is a theorem proof relying on standard automata/Kleene algebra background and the cited soundness of hypothesis-closure semantics.

assumptions (6)

standard math Kozen's completeness theorem for KA (Theorem 2.6): JeK=JfK iff e≡f.
Assumed as background; used in Lemma 2.15 and in the solution-lemma proofs to equate language equality with provability.
standard math Kleene's theorem (Theorem 2.4): regular languages coincide with languages of finite automata.
Used to move between expressions, automata, and least solutions.
standard math Existence and computability of least solutions for finite automata (Lemma 2.9).
Taken from Conway/Kozen; used to define r0(g) and rH(g) as the least solution at the initial state.
domain assumption KAH is sound with respect to hypothesis-closure semantics J−KH (from Doumane et al. [7]).
Assumed, cited; used in Lemma 2.15 to translate between provability and language inclusion.
domain assumption Hypothesis closure H* is well-defined as the smallest fixed point of the one-step closure H.
Definition 2.13; existence is taken from [7].
standard math Generalized Brzozowski derivatives w^{-1}L and M^{-1}L are computable on regular languages.
Used in the patching criterion (Lemma 3.6) and in Definition 3.7.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Partial Reductions for Kleene Algebra with Linear Hypotheses." pith.science (2026). https://pith.science/paper/WRQPCQC5

@misc{pith2026260114114,
  author       = {Pith},
  title        = {Pith review of: Partial Reductions for Kleene Algebra with Linear Hypotheses},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WRQPCQC5}},
  note         = {Machine review of arXiv:2601.14114}
}

read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 9 canonical work pages

[1]

In: CSL (2025)

de Amorim, A.A., Zhang, C., Gaboardi, M.: Kleene algebra with commutativity conditions is undecidable. In: CSL (2025). https://doi.org/10.4230/LIPICS.CSL. 2025.36

doi:10.4230/lipics.csl 2025
[2]

In: POPL (2014)

Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: POPL (2014). https: //doi.org/10.1145/2535838.2535862

arXiv 2014
[3]

Springer (1993)

Book, R.V., Otto, F.: String-Rewriting Systems. Springer (1993)

1993
[4]

Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. Sci.8(1) (2012). https://doi.org/10.2168/LMCS-8(1:16)2012

work page doi:10.2168/lmcs-8(1:16)2012 2012
[5]

Cohen, E.: Hypotheses in Kleene algebra. Tech. rep., Bellcore (1994)

1994
[6]

Chapman and Hall, London (1971)

Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)

1971
[7]

In: FoSSaCS (2019)

Doumane, A., Kuperberg, D., Pous, D., Pradic, C.: Kleene algebra with hypotheses. In: FoSSaCS (2019). https://doi.org/10.1007/978-3-030-17127-8_12

work page doi:10.1007/978-3-030-17127-8_12 2019
[8]

In: CONCUR (2019)

Kappé, T., Brunet, P., Rot, J., Silva, A., Wagemaker, J., Zanasi, F.: Kleene algebra with observations. In: CONCUR (2019). https://doi.org/10.4230/LIPIcs.CONCUR. 2019.41

work page doi:10.4230/lipics.concur 2019

Show all 24 references

[9]

FoSSaCS (2020)

Kappé, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: from hypotheses to completeness. FoSSaCS (2020). https://doi.org/10.1007/978-3-030-45231-5_20

2020 doi
[10]

In: ESOP

Kappé, T., Brunet, P., Silva, A., Zanasi, F.: Concurrent Kleene algebra: Free model and completeness. In: ESOP. pp. 856–882 (2018). https://doi.org/10.1007/ 978-3-319-89884-1_30

2018
[11]

Automata Studies pp

Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Studies pp. 3–41 (1956)

1956
[12]

Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput.110(2), 366–390 (1994)

1994
[13]

In: TACAS (1996)

Kozen, D.: Kleene algebra with tests and commutativity conditions. In: TACAS (1996). https://doi.org/10.1007/3-540-61042-1_35

1996 doi
[14]

In: ICALP (2014)

Kozen, D., Mamouras, K.: Kleene algebra with equations. In: ICALP (2014). https://doi.org/10.1007/978-3-662-43951-7_24

2014 doi
[15]

In: CSL (1996)

Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: CSL (1996). https://doi.org/10.1007/3-540-63172-0_43

1996 doi
[16]

In: ICTAC (2023)

Kuznetsov, S.L.: On the complexity of reasoning in Kleene algebra with commuta- tivity conditions. In: ICTAC (2023). https://doi.org/10.1007/978-3-031-47963-2_7

2023 doi
[17]

In: CONCUR (2019)

Maarand, H., Uustalu, T.: Reordering derivatives of trace closures of regular languages. In: CONCUR (2019). https://doi.org/10.4230/LIPICS.CONCUR.2019. 40

2019 doi
[18]

Pous, D., Rot, J., Wagemaker, J.: On tools for completeness of Kleene algebra with hypotheses. Log. Methods Comput. Sci.20(2) (2024). https://doi.org/10.46298/ LMCS-20(2:8)2024

2024
[19]

Thompson, K.: Regular expression search algorithm. Commun. ACM11(6), 419–422 (1968). https://doi.org/10.1145/363347.363387 20 L. Chung and T. Kappé A Proof of Example 2.10 Example 2.10.Program 3 and Program 4 are inequivalent in standard regular language semantics, but equival...

1968
[20]

Similarly, the states of Zi only have outgoing transitions to otherZi states (with the samei), except for thezi ⊕ which also has anε-transition back to allx′ i such thatxi w − →∗ x′ i. In total,s ′ :X∪Z 1 ∪ · · · ∪Zn →Eis anH-solution toT 0(X)if it satisfies: 1≦ H s′(x⊕) x a −...
[21]

By definition ofs ∗ andr i it suffices to show that, for anyiandx′ withx i w − →∗ X x′: sZi (zi 0)·s(x ′)≦ H s(xi)

≦H s∗(xi). By definition ofs ∗ andr i it suffices to show that, for anyiandx′ withx i w − →∗ X x′: sZi (zi 0)·s(x ′)≦ H s(xi). Now sinceZi is an automaton representingJeK and zi 0 is its initial state,sZi (zi
[22]

≡ e(by Theorem 2.6). Applying this fact and our hypothesise≤w, sZi (zi 0)·s(x ′)≦e·s(x ′)≦ H w·s(x ′)≦s(x i) where the final containment can be argued using the fact thats is a solution to X, by induction on the construction of the tracexi w − →∗ Z x′. Lemma 4.8. Suppose that ...
[23]

≡e , we instead use Lemma 4.8 to find thatsZ w i (zi
[24]

Theorem 4.10.r H is a partial reduction

≡H e; this also suffices to make the final derivation go through. Theorem 4.10.r H is a partial reduction. Proof. To show thatrH is a partial reduction, we must show for allg∈E on which it is defined the following two properties hold: JgKH ⊆Jr H (g)Kr H (g)≦ H g The former fol...

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.

[1] [1]

In: CSL (2025)

de Amorim, A.A., Zhang, C., Gaboardi, M.: Kleene algebra with commutativity conditions is undecidable. In: CSL (2025). https://doi.org/10.4230/LIPICS.CSL. 2025.36

doi:10.4230/lipics.csl 2025

[2] [2]

In: POPL (2014)

Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: POPL (2014). https: //doi.org/10.1145/2535838.2535862

arXiv 2014

[3] [3]

Springer (1993)

Book, R.V., Otto, F.: String-Rewriting Systems. Springer (1993)

1993

[4] [4]

Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Methods Comput. Sci.8(1) (2012). https://doi.org/10.2168/LMCS-8(1:16)2012

work page doi:10.2168/lmcs-8(1:16)2012 2012

[5] [5]

Cohen, E.: Hypotheses in Kleene algebra. Tech. rep., Bellcore (1994)

1994

[6] [6]

Chapman and Hall, London (1971)

Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)

1971

[7] [7]

In: FoSSaCS (2019)

Doumane, A., Kuperberg, D., Pous, D., Pradic, C.: Kleene algebra with hypotheses. In: FoSSaCS (2019). https://doi.org/10.1007/978-3-030-17127-8_12

work page doi:10.1007/978-3-030-17127-8_12 2019

[8] [8]

In: CONCUR (2019)

Kappé, T., Brunet, P., Rot, J., Silva, A., Wagemaker, J., Zanasi, F.: Kleene algebra with observations. In: CONCUR (2019). https://doi.org/10.4230/LIPIcs.CONCUR. 2019.41

work page doi:10.4230/lipics.concur 2019