The equational theory of the Weihrauch lattice with (iterated) composition

TL;DR

The paper tackles the equational theory of the Weihrauch lattice under composition and iterations by introducing extended Weihrauch problems and a simulation game based on Büchi automata. It provides a complete axiomatization, $ ext{RSKA}_{digsqcap}$, mirroring right-skewed Kleene-algebra style while handling distributive meets and non-distributivity of $igsqcup$ over $ hd$, and proves soundness and completeness via a novel game-theoretic framework. A key result is that universal validity of inequations in the extended Weihrauch degrees coincides with the existence of winning strategies in the simulation game, yielding decidability; the paper also establishes complexity bounds, proving PSPACE-hardness and offering PSPACE-membership conjectures. The approach connects automata-theoretic methods with algebraic proof systems, providing a foundation for both further theoretical exploration and potential extensions to related Weihrauch degree settings.

Abstract

We study the equational theory of the Weihrauch lattice with composition and iterations, meaning the collection of equations between terms built from variables, the lattice operations $\sqcup$, $\sqcap$, the composition operator $\star$ and its iteration $(-)^\diamond$ , which are true however we substitute (slightly extended) Weihrauch degrees for the variables. We characterize them using Büchi games on finite graphs and give a complete axiomatization that derives them. The term signature and the axiomatization are reminiscent of Kleene algebras, except that we additionally have meets and the lattice operations do not fully distributes over composition. The game characterization also implies that it is decidable whether an equation is universally valid. We give some complexity bounds; in particular, the problem is Pspace-hard in general and we conjecture that it is solvable in Pspace.

Figures (6)

• Figure 1: Some complexity bounds for deciding "is $t \le u$ valid" in substructures of Weihrauch degrees with the operators we discuss.
• Figure 2: Axioms of right-skewed Kleene algebras with distributive meets ($\mathrm{RSKA}_{d\sqcap}$). If we want to regard it as an equational theory, we can take $a \le b$ to be a notation for $a = a \sqcap b$.
• Figure 3: Operators on extended Weihrauch problems and assorted constants, assuming $P$ and $Q$ are extended Weihrauch problems. $\operatorname{dom}(P^\diamond)$ should be the smalled subset of ${\mathbb{N}^\mathbb{N}}$ satisfying the advertised conditions; the sets of valid outputs of $P^\diamond$ are then computed by well-founded recursion on the inputs.
• Figure 4: Definitions of $\to$ and polarities.
• Figure 5: Moves in the arena $\mathcal{SG}$ (this is part of \ref{['def:simgame']}).

Theorems & Definitions (57)

• Example 1.1
• Example 1.2
• Example 1.3
• Theorem 1.4
• Definition 2.1
• Remark 2.2
• Definition 2.3
• Lemma 2.4
• proof
• Lemma 2.5