The equational theory of the Weihrauch lattice with (iterated) composition
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915127548182528 |
|---|---|
| author | Pradic, Cécilia |
| author_facet | Pradic, Cécilia |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_14999 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The equational theory of the Weihrauch lattice with (iterated) composition Pradic, Cécilia Logic in Computer Science Logic 03D30, 68Q85 F.4.1 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. |
| title | The equational theory of the Weihrauch lattice with (iterated) composition |
| topic | Logic in Computer Science Logic 03D30, 68Q85 F.4.1 |
| url | https://arxiv.org/abs/2408.14999 |