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

Abstract

We study the equational theory of the Weihrauch lattice with composition and iteration, meaning the collection of equations between terms built from variables, the lattice operations $\bigsqcup ,\sqcap$, the composition operator $\star$ and its iteration $(-{)}^{\diamond }$, which are true however we substitute (partial) 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 distribute over composition. The game characterization gives a variant of the notion of simulation for alternating automata. It 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. We expect that the axiomatizations and games can also be applicable as-is to characterize the existence of strong natural transformation between polynomial functor expressions.

49 pages - major revision, consisting in the addition of informal explanations, examples, related work and bugfixes. Section 3 was extensively revised for clarity and results therein generalized to alternating automata. Sections 1, 2, 5 and 6 were also substantially revised. Some of the terminology was changed, including using "partial" rather than overloading "extended"