Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The equational theory of the Weihrauch lattice with multiplication

Eike Neumann, Arno Pauly, Cécilia Pradic

TL;DR

The paper investigates the equational theory of the Weihrauch lattice $\mathfrak{W}$ endowed with the operations $\sqcap$, $\sqcup$, $\times$, and $(-)^*$ (and its pointed sublattice $\mathfrak{W}_\bullet$). It introduces a novel combinatorial, graph-based description of term inequalities via reductions between finite graphs and shows that universal validity of $\sqcap$- and $\times$-based inequalities corresponds to the existence of such combinatorial reductions, yielding a $\Sigma^p_2$-complete decision problem in the join-free case. The framework is extended to the full signature including $\sqcup$ and $(-)^*$, introducing slices and parallelization-annotated graphs, and it is shown that the validity problem becomes $\Pi^p_3$-complete, with a precise account of the quantifier structure. The results bridge Weihrauch degree structure with graph-theoretic reducibility, establish equivalences between pointed and non-pointed completeness notions, and outline a program toward a complete axiomatization for the full language. These findings clarify the algebraic and computational aspects of Weihrauch degrees and illuminate their connections to constructive logic and graph combinatorics.

Abstract

We study the equational theory of the Weihrauch lattice with multiplication, meaning the collection of equations between terms built from variables, the lattice operations $\sqcup$, $\sqcap$, the product $\times$, and the finite parallelization $(-)^*$ which are true however we substitute Weihrauch degrees for the variables. We provide a combinatorial description of these in terms of a reducibility between finite graphs, and moreover, show that deciding which equations are true in this sense is complete for the third level of the polynomial hierarchy.

The equational theory of the Weihrauch lattice with multiplication

TL;DR

The paper investigates the equational theory of the Weihrauch lattice endowed with the operations , , , and (and its pointed sublattice ). It introduces a novel combinatorial, graph-based description of term inequalities via reductions between finite graphs and shows that universal validity of - and -based inequalities corresponds to the existence of such combinatorial reductions, yielding a -complete decision problem in the join-free case. The framework is extended to the full signature including and , introducing slices and parallelization-annotated graphs, and it is shown that the validity problem becomes -complete, with a precise account of the quantifier structure. The results bridge Weihrauch degree structure with graph-theoretic reducibility, establish equivalences between pointed and non-pointed completeness notions, and outline a program toward a complete axiomatization for the full language. These findings clarify the algebraic and computational aspects of Weihrauch degrees and illuminate their connections to constructive logic and graph combinatorics.

Abstract

We study the equational theory of the Weihrauch lattice with multiplication, meaning the collection of equations between terms built from variables, the lattice operations , , the product , and the finite parallelization which are true however we substitute Weihrauch degrees for the variables. We provide a combinatorial description of these in terms of a reducibility between finite graphs, and moreover, show that deciding which equations are true in this sense is complete for the third level of the polynomial hierarchy.
Paper Structure (7 sections, 16 theorems, 14 equations, 2 figures)

This paper contains 7 sections, 16 theorems, 14 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Introducing the operations
  3. A combinatorial notion of reducibility for terms
  4. Completeness does not depend on pointedness
  5. Introducing joins and parallelization
  6. Complexity of deciding validity
  7. Towards a proof of completeness

Key Result

Theorem 9

Let $t$ and $u$ be terms constructed from variables and the binary connectives $\sqcap, \times$. Then inequalities $t \leq u$ and $t \le_\bullet u$ are universally valid if and only if they are combinatorially valid.

Figures (2)

  • Figure 1: Our set of axioms for the systems under consideration, where we implicitly assume that equality is an equivalence relation, that all operators are monotone in each of their arguments and that inequalities are transitive. Every axiom we state holds when substituting $\le_\bullet$ for $\le$ everywhere, and we take this as axioms for $\le_\bullet$ alongside the specific $\le_\bullet$ axioms.
  • Figure 2: Axioms for $\sqcup$ and $(-)^*$

Theorems & Definitions (40)

  • Definition 1
  • Definition 2
  • Definition 3
  • Conjecture 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Theorem 9
  • Definition 10
  • ...and 30 more