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

TL;DR

This paper explores the algebraic structure of the Weihrauch lattice with composition and iteration, providing a complete axiomatization, a game-based characterization, and complexity bounds for equation validity.

Contribution

It introduces a novel axiomatization and game-theoretic characterization of the Weihrauch lattice's equational theory, extending Kleene algebra concepts.

Findings

Complete axiomatization of the equational theory.

Game characterization using B"uchi games on finite graphs.

Decidability and complexity bounds for equation validity.

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\"uchi 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.