Iteration 2-theories
Algebraically complete categories are important for computer science. Actually, they are exactly those categories in which one may define recursive data types in a canonical way as initial solutions of recursive functorial equations corresponding to data type specifications. An algebraically complete category \({\mathcal C}\) with a collection \({\mathcal F}\) of functors \({\mathcal C}^{n+p} \rightarrow {\mathcal C}^{n}, n, p \geq 0\), implicitly specifies a dagger operation \(F \longmapsto F^{\dagger}\) on the functors in \({\mathcal F}\). This operation can be extended to natural transformations \(\tau : F \rightarrow G\) between functors \(F\), \(G\) in \({\mathcal F}\). Viewing the functors in \({\mathcal F}\) and their natural transformations as a 2-theory, i.e., a 2-category with Cartesian structure, one obtains a dagger operation defined on all 2-cells. This dagger operation, defined both on functors and on natural transformations, or more generally, on horizontal and vertical morphisms, interacts smoothly with the categorical and Cartesian structure. The study of this interaction is the topic of the present paper. The authors give an axiomatic treatment. Then they introduce a new concept, iteration 2-theories, that generalizes (ordered) iteration theories. By describing explicitly the structure of the free iteration 2-theories, they show that the axioms of iteration 2-theories capture, up to isomorphism, the dagger operation in algebraically complete categories. Their description involves regular trees and they consider some applications of the axioms of iteration 2-theories for manipulating tree transformations.
- Equational properties of iteration in algebraically complete categories
- Categories with sums and right distributive tensor product
- Relative full completeness for bicategorical Cartesian closed structure
- Axiomatizing weighted synchronization trees and weighted bisimilarity
- Bisimulation relations for weighted automata
- Graph automata
- Equational properties of fixed point operations in Cartesian categories: an overview
- Dagger extension theorem
- Simulation relations for pattern matching in directed graphs
- scientific article; zbMATH DE number 1107618 (Why is no real title available?)
- μ-Bicomplete Categories and Parity Games
- Inversion, iteration, and the art of dual wielding
- Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories
- Equational properties of fixed-point operations in Cartesian categories: an overview
This page was built for publication: Iteration 2-theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5930757)
