Continuous Algebras with Hypotheses

Damien Pous (PLUME; Jana Wagemaker; LIP); Lukas Mulder

arxiv: 2605.18450 · v1 · pith:EF7R7DGBnew · submitted 2026-05-18 · 💻 cs.LO

Continuous Algebras with Hypotheses

Lukas Mulder , Damien Pous (PLUME , LIP) , Jana Wagemaker This is my paper

Pith reviewed 2026-05-20 08:19 UTC · model grok-4.3

classification 💻 cs.LO

keywords Kleene algebrahypothesescontinuous algebrascomplete latticesleast fixpointssoundnesscompletenessaxiomatisation

0 comments

The pith

Closed languages form a sound and complete canonical model for a unifying framework of continuous algebras that covers Kleene algebra variants with hypotheses.

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

Variants of Kleene algebra such as those with tests, commutative versions, bi-Kleene algebra, concurrent versions, and regular tree languages have each been equipped with extra assumptions called hypotheses. The paper places all of them inside one framework consisting of algebras that are ordered by complete lattices and allow computation of least fixpoints. A canonical model built from closed languages is shown to be sound and complete for every continuous model in this framework. For the quasi-equational theories, a generic axiomatisation is given that is always sound, together with modular tools that can be used to establish completeness for any specific instance. These tools deliver new completeness results when applied to commutative Kleene algebra, bi-Kleene algebra, and regular tree languages, each extended by various hypotheses.

Core claim

We propose a unifying framework encompassing all the previous structures as well as regular tree languages by considering algebras ordered by complete lattices where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. We study quasi-equational axiomatisations by supplying a generic sound axiomatisation and modular tools that make it possible to obtain complete ones, and we apply these tools to prove new completeness results for commutative KA, bi-KA, and regular tree languages in each case extended with various hypotheses.

What carries the argument

The unifying framework of algebras ordered by complete lattices in which least fixpoints can be computed, with the canonical model of closed languages serving as the structure that establishes soundness and completeness for all continuous models.

If this is right

The equational theories of Kleene algebra with tests, commutative KA, bi-KA, concurrent KA, and regular tree languages can be studied uniformly inside the same framework.
A generic quasi-equational axiomatisation is sound for every instance of the framework.
Modular tools built on prior literature allow completeness to be established case by case for specific variants and hypotheses.
New completeness theorems hold for commutative KA, bi-KA, and regular tree languages when each is extended with various hypotheses.

Where Pith is reading between the lines

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

The same lattice-ordered fixpoint framework could be used to organise completeness proofs for other algebraic structures that involve iteration or recursion beyond the Kleene-algebra family.
The modular axiomatisation tools may shorten the work of checking completeness when new hypotheses are added to an existing variant.

Load-bearing premise

The structures under study are algebras ordered by complete lattices in which least fixpoints can be computed.

What would settle it

A continuous model in which an equation or quasi-equation holds that is false in the closed-languages model would falsify the claimed soundness and completeness.

read the original abstract

In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theories of some of these structures have then been studied in the presence of additional assumptions, called hypotheses. We propose a unifying framework encompassing all the previous structures, as well as regular tree languages. This is done by considering algebras ordered by complete lattices, where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. Then we study quasi-equational axiomatisations. It is illusory to hope for a generic axiomatisation which would be sound and complete for all instances. Instead, we provide a generic axiomatisation which we prove sound and we setup tools that make it possible to get complete ones in a modular way, building on previous works from the literature. We showcase these tools by proving new completeness results for commutative KA, bi-KA, and regular tree languages, in each case extended with various hypotheses.

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.

Desk Editor's Note private letter to a colleague

A continuous-algebra unification of Kleene variants and tree languages that supplies modular completeness tools, though verification awaits the full proofs.

read the letter

Colleague, the key takeaway is that this work puts several Kleene algebra variants and regular tree languages into one continuous algebra framework and derives new completeness results for commutative KA, bi-KA, and tree languages when hypotheses are added. They start from algebras ordered by complete lattices that support least fixpoints. From there they construct a canonical model using closed languages and prove it sound and complete relative to all continuous models. On the axiomatic side they supply a generic quasi-equational theory that is sound for the whole class, but they correctly point out that a single complete axiomatization for every possible hypothesis set is not realistic. Instead they give modular tools that let you obtain completeness by building on existing results from the literature. The paper then demonstrates these tools by proving the new completeness theorems for the three cases mentioned. The strength is in the organization and the reusable machinery. If the canonical model holds up, it could shorten future completeness arguments in this area. The modular approach also respects the fact that different hypotheses need different treatments, which matches what we have seen in earlier work on these structures. The main limitation right now is that only the abstract is in front of us. Without the actual constructions and proof details I cannot tell whether the closed-language model really captures the continuity requirements across all the listed variants or whether some of the hypotheses introduce edge cases that break the generic soundness claim. The weakest assumption seems to be that the structures are always complete lattices with computable least fixpoints; if that does not line up with how people actually use commutative KA or bi-KA in practice, the unification might be narrower than it first appears. This paper is aimed at specialists in algebraic logic and automata theory who already know the basic Kleene algebra results. Someone looking for a way to organize or extend completeness proofs in this subfield would find it useful. I would recommend sending it out for peer review. The ideas are concrete enough that referees can check the technical claims directly.

Referee Report

0 major / 0 minor

Summary. The paper proposes a unifying framework for variants of Kleene algebra (including with tests, commutative, bi-KA, concurrent KA) and regular tree languages. The framework uses algebras ordered by complete lattices in which least fixpoints can be computed. It introduces a canonical model of closed languages, claimed to be sound and complete for all continuous models. The paper then develops quasi-equational axiomatisations: a generic axiomatisation proven sound, together with modular tools for obtaining completeness results by building on prior literature. These tools are applied to obtain new completeness results for commutative KA, bi-KA, and regular tree languages, each extended with various hypotheses.

Significance. If the soundness and completeness of the canonical model of closed languages hold, and if the modular tools successfully yield the claimed new completeness results, the work would provide a valuable unifying approach to equational theories of Kleene-algebra variants under hypotheses. The generic sound axiomatisation and the ability to derive completeness modularly could streamline future extensions in algebraic logic and automata theory.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their summary of our paper and for acknowledging its potential significance as a unifying framework for variants of Kleene algebra and regular tree languages under hypotheses, provided the key technical results hold. We appreciate the conditional recommendation and address the assessment below. Since the major comments section does not list specific technical objections, our response focuses on the conditional aspects raised in the significance and recommendation sections.

read point-by-point responses

Referee: If the soundness and completeness of the canonical model of closed languages hold, and if the modular tools successfully yield the claimed new completeness results, the work would provide a valuable unifying approach to equational theories of Kleene-algebra variants under hypotheses.

Authors: The manuscript contains detailed proofs establishing that the canonical model of closed languages is sound and complete for all continuous algebras. The generic quasi-equational axiomatisation is proven sound, and the modular tools are developed to derive completeness results by leveraging existing literature. These tools are then applied to obtain new completeness results for commutative KA, bi-KA, and regular tree languages, each extended with various hypotheses. We believe the proofs are complete and correct as presented; we would welcome any specific questions on particular steps to provide further clarification. revision: no

Circularity Check

0 steps flagged

No circularity detectable; derivation chain not inspectable from abstract

full rationale

The abstract outlines a unifying framework for continuous algebras with hypotheses, a canonical model of closed languages claimed sound and complete for all continuous models, and modular quasi-equational axiomatizations building on prior literature for specific cases like commutative KA and regular tree languages. No equations, definitions, or derivation steps are provided that reduce any result to its inputs by construction, self-citation, or fitted parameters. The claims are presented as independent proofs and extensions of external works, rendering the derivation self-contained on the basis of the available text.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on standard order-theoretic assumptions about complete lattices and least fixpoints; the canonical model of closed languages is introduced as a new construction whose independent evidence is the claimed soundness and completeness proof.

axioms (1)

domain assumption Algebras are ordered by complete lattices where least fixpoints can be computed.
Explicitly stated as the basis for the unifying framework in the abstract.

invented entities (1)

Canonical model of closed languages no independent evidence
purpose: To provide a sound and complete semantics for all continuous models.
Introduced in the abstract as the central model whose soundness and completeness are proved.

pith-pipeline@v0.9.0 · 5692 in / 1287 out tokens · 47798 ms · 2026-05-20T08:19:34.664181+00:00 · methodology

Continuous Algebras with Hypotheses

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)