pith. sign in

arxiv: 2606.30337 · v1 · pith:PJASZKCWnew · submitted 2026-06-29 · 💻 cs.LO

GKAT with Hoare Hypotheses

Jurriaan Rot , Todd Schmid , Jana Wagemaker This is my paper

Pith reviewed 2026-06-30 03:37 UTC · model grok-4.3

classification 💻 cs.LO
keywords GKATHoare hypothesesword hypothesesprogram equivalenceKleene algebraautomata decision proceduresoundnesscompleteness
0
0 comments X

The pith

GKAT admits Hoare hypotheses on program pre- and post-conditions while keeping its axiomatization sound and complete and its equivalence check as fast as before.

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

The paper adds Hoare hypotheses to Guarded Kleene Algebra with Tests so that users can record basic domain knowledge about the pre- and post-conditions of basic programs. It proves the resulting set of axioms is sound and complete for the extended semantics. The authors then generalize the hypotheses to word hypotheses and give an automata construction that decides equivalence in the same near-linear time bound that holds for ordinary GKAT. A sympathetic reader therefore obtains a practical way to reason about programs under explicit assumptions without losing the original decision procedure.

Core claim

We develop Hoare hypotheses for GKAT that model basic domain knowledge on pre- and post-conditions of uninterpreted basic programs, prove the resulting axiomatisation sound and complete, extend the hypotheses to the more general form of word hypotheses, and show via an automata-theoretic construction that equivalence of GKAT terms under word hypotheses remains decidable in the same asymptotic time as for plain GKAT.

What carries the argument

Hoare hypotheses (and their generalization to word hypotheses) that record pre- and post-conditions on basic programs, together with the automata construction that decides equivalence while preserving the original complexity bound.

If this is right

  • Users can now encode basic pre- and post-condition assumptions inside GKAT derivations while retaining soundness and completeness.
  • Equivalence of programs under such assumptions can still be checked by the same automata method in near-linear time.
  • The decision procedure applies uniformly to both ordinary Hoare hypotheses and the more general word hypotheses.
  • Reasoning about imperative programs can incorporate domain knowledge without changing the complexity class of the equivalence check.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifting technique might let other Kleene-algebra variants absorb similar hypotheses while keeping fast decision procedures.
  • Tool builders could add a front-end that turns user-supplied invariants into word hypotheses and then invoke the existing GKAT checker.
  • The approach opens a route to verifying larger programs by successively adding and discharging word hypotheses.
  • Implementation experiments could test whether the automata size stays manageable on realistic program fragments that carry a few hypotheses.

Load-bearing premise

The automata construction used for plain GKAT equivalence can be lifted to word hypotheses without increasing asymptotic complexity.

What would settle it

A concrete pair of GKAT terms equipped with word hypotheses whose semantic equivalence is missed by the axiomatization, or whose decision procedure runs slower than the plain-GKAT bound.

read the original abstract

Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the current paper, we address the challenge of reasoning under assumptions about these programs. In particular, we develop a form of Hoare hypotheses, which allow modelling basic domain knowledge on pre- and post-conditions of uninterpreted basic programs, and which are well-developed for classical Kleene algebra but not yet for GKAT. We show that the resulting axiomatisation is sound and complete. We then extend Hoare hypotheses to the more general form of word hypotheses. Based on an automata-theoretic approach, we show that equivalence of GKAT under word hypotheses is as efficiently decidable as for plain GKAT.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper extends Guarded Kleene Algebra with Tests (GKAT) by adding Hoare hypotheses (modeling pre- and post-conditions on uninterpreted basic programs) and further generalizes them to word hypotheses. It claims to establish soundness and completeness of the resulting axiomatization, and, via an automata-theoretic construction, shows that equivalence checking under word hypotheses remains decidable in the same nearly-linear time as plain GKAT.

Significance. If the soundness, completeness, and complexity-preservation claims hold, the work fills a recognized gap in applying GKAT to programs under domain assumptions while retaining the framework's principal practical advantage (efficient decidability). The automata-theoretic lifting is a key technical contribution that would directly support verification applications.

minor comments (2)
  1. [Abstract] Abstract: a one-sentence outline of the automata construction (e.g., how hypotheses are encoded into the automaton states or transitions) would help readers immediately see why the complexity bound is preserved.
  2. The paper would benefit from an explicit statement of the complexity class (e.g., O(n log n) or linear) achieved by the new decision procedure, even if it matches the plain-GKAT bound.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. We are pleased that the contribution of extending GKAT with Hoare and word hypotheses, while preserving soundness, completeness, and nearly-linear-time decidability, is recognized as filling an important gap.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper introduces Hoare hypotheses and word hypotheses as extensions to GKAT, then proves soundness and completeness of the resulting axiomatization and shows an automata construction preserves decision complexity. These steps rely on standard algebraic proofs and automata theory rather than any self-definitional reduction, fitted input renamed as prediction, or load-bearing self-citation chain. The provided abstract and description contain no equations or claims that collapse to their own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The central claim rests on the standard GKAT axioms plus newly introduced Hoare and word hypotheses axioms; no free parameters or invented entities are indicated.

axioms (3)
  • standard math Standard GKAT axioms
    Background axioms of Guarded Kleene Algebra with Tests from prior literature.
  • ad hoc to paper Hoare hypotheses axioms
    New axioms introduced to model pre- and post-conditions of uninterpreted programs.
  • ad hoc to paper Word hypotheses axioms
    Generalization of Hoare hypotheses to word-level assumptions.

pith-pipeline@v0.9.1-grok · 5660 in / 1290 out tokens · 51662 ms · 2026-06-30T03:37:29.482793+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

34 extracted references · 16 canonical work pages

  1. [1]

    5 Emily Clement, Enzo Erlich, and Jérémy Ledent

    Yoshiki Nakamura , title =. RAMiCS , series =. doi:10.1007/978-3-031-68279-7\_13 , pages =

    work page doi:10.1007/978-3-031-68279-7

  2. [2]

    1997 , doi =

    Dexter Kozen , title =. 1997 , doi =

    1997

  3. [3]

    doi:10.1145/343369.343378 , pages =

    Dexter Kozen , title =. doi:10.1145/343369.343378 , pages =

    work page doi:10.1145/343369.343378

  4. [4]

    CoRR , volume =

    Yoshiki Nakamura , title =. CoRR , volume =

  5. [5]

    Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories , journal =

    Jack Liell. Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories , journal =. 2025 , doi =

    2025

  6. [6]

    Jan J. M. M. Rutten , title =. Theor. Comput. Sci. , volume =. 2000 , doi =

    2000

  7. [7]

    Todd Schmid and Tobias Kapp. Guarded. doi:10.4230/LIPICS.ICALP.2021.142 , pages =

    work page doi:10.4230/lipics.icalp.2021.142 2021

  8. [8]

    Steffen Smolka and Nate Foster and Justin Hsu and Tobias Kapp. Guarded. Proc. 2020 , url =. doi:10.1145/3371129 , timestamp =

    work page doi:10.1145/3371129 2020

  9. [9]

    Cheng Zhang and Tobias Kapp. Proc. 2025 , url =. doi:10.1145/3704857 , timestamp =

    work page doi:10.1145/3704857 2025

  10. [10]

    doi:10.4230/LIPICS.ICALP.2025.172 , pages =

    Spencer Van Koevering and Wojciech Rozowski and Alexandra Silva , title =. doi:10.4230/LIPICS.ICALP.2025.172 , pages =

    work page doi:10.4230/lipics.icalp.2025.172 2025

  11. [11]

    Probabilistic Guarded

    Wojciech Rozowski and Tobias Kapp. Probabilistic Guarded. doi:10.4230/LIPICS.ICALP.2023.136 , year =

    work page doi:10.4230/lipics.icalp.2023.136 2023

  12. [12]

    1975 , issue_date =

    Tarjan, Robert Endre , title =. 1975 , issue_date =. doi:10.1145/321879.321884 , journal =

    work page doi:10.1145/321879.321884 1975

  13. [13]

    Kleene Algebra with Hypotheses , booktitle =

    Amina Doumane and Denis Kuperberg and Damien Pous and C. Kleene Algebra with Hypotheses , booktitle =. 2019 , doi =

    2019

  14. [14]

    Damien Pous and Jurriaan Rot and Jana Wagemaker , title =. Log. Methods Comput. Sci. , volume =. 2024 , doi =

    2024

  15. [15]

    2014 , doi =

    Dexter Kozen and Konstantinos Mamouras , title =. 2014 , doi =

    2014

  16. [16]

    , institution =

    Cohen, E. , institution =. Hypotheses in

  17. [17]

    Arthur Azevedo de Amorim and Cheng Zhang and Marco Gaboardi , editor =. 33rd. 2025 , doi =

    2025

  18. [18]

    , title =

    Paige, Robert and Tarjan, Robert E. , title =. SIAM Journal on Computing , volume =. 1987 , publisher =

    1987

  19. [19]

    and Karp, Richard M

    Hopcroft, John E. and Karp, Richard M. , title =. 1971 , number =

    1971

  20. [20]

    1996 , doi =

    Dexter Kozen and Frederick Smith , title =. 1996 , doi =

    1996

  21. [21]

    Cormen and Charles E

    Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein , title =. 2009 , url =

    2009

  22. [22]

    Arto Salomaa , title =. J. doi:10.1145/321312.321326 , pages =

    work page doi:10.1145/321312.321326

  23. [23]

    Stark and Scott A

    Eugene W. Stark and Scott A. Smolka , editor =. A complete axiom system for finite-state probabilistic processes , booktitle =. 2000 , timestamp =

    2000

  24. [24]

    doi:10.4230/LIPICS.ICALP.2022.132 , pages =

    Todd Schmid and Wojciech Rozowski and Alexandra Silva and Jurriaan Rot , title =. doi:10.4230/LIPICS.ICALP.2022.132 , pages =

    work page doi:10.4230/lipics.icalp.2022.132 2022

  25. [25]

    A Cyclic Proof System for Guarded

    Jan Rooduijn and Dexter Kozen and Alexandra Silva , editor =. A Cyclic Proof System for Guarded. Automated Reasoning - 12th International Joint Conference,. 2024 , doi =

    2024

  26. [26]

    doi:10.4230/LIPICS.CSL.2025.35 , series =

    Leandro Gomes and Patrick Baillot and Marco Gaboardi , title =. doi:10.4230/LIPICS.CSL.2025.35 , series =

    work page doi:10.4230/lipics.csl.2025.35 2025

  27. [27]

    doi:10.1145/2535838.2535862 , pages =

    Carolyn Jane Anderson and Nate Foster and Arjun Guha and Jean. doi:10.1145/2535838.2535862 , pages =

    work page doi:10.1145/2535838.2535862

  28. [28]

    Wasserstein, Jacob , institution =. Guarded

  29. [29]

    Cohen, Ernie and Kozen, Dexter and Smith, Frederick , title =

  30. [30]

    A Complete Inference System for Skip-free Guarded

    Todd Schmid and Tobias Kapp. A Complete Inference System for Skip-free Guarded. doi:10.1007/978-3-031-30044-8\_12 , year =

    work page doi:10.1007/978-3-031-30044-8

  31. [31]

    doi:10.1007/978-3-032-22723-2\_14 , series =

    Cheng Zhang and Qiancheng Fu and Hang Ji and Ines Santacruz Del Valle and Alexandra Silva and Marco Gaboardi , title =. doi:10.1007/978-3-032-22723-2\_14 , series =

    work page doi:10.1007/978-3-032-22723-2

  32. [32]

    doi:10.1145/2676726.2677007 , pages =

    Damien Pous , title =. doi:10.1145/2676726.2677007 , pages =

    work page doi:10.1145/2676726.2677007

  33. [33]

    Hoare, C. A. R. , title =. 1969 , issue_date =. doi:10.1145/363235.363259 , journal =

    work page doi:10.1145/363235.363259 1969

  34. [34]

    Jurriaan Rot, Todd Schmid, Jana Wagemaker , howpublished =