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.
翻译:我们研究了带有合成与迭代的魏赫劳赫格的等式理论,即由变量、格运算 $\sqcup$、$\sqcap$、合成算子 $\star$ 及其迭代 $(-)^\diamond$ 构成的项之间,无论我们如何用(稍加推广的)魏赫劳赫度替换变量都成立的等式集合。我们利用有限图上的布希博弈刻画了这些等式,并给出了推导它们的完备公理化系统。项签名与公理化系统让人联想到克林代数,不同之处在于我们额外引入了交运算,且格运算并不完全对合成满足分配律。博弈刻画也意味着一个等式是否普遍有效是可判定的。我们给出了一些复杂性界;特别地,该问题在一般情况下是 Pspace 难的,我们推测它在 Pspace 内可解。