
handle: 11573/40382 , 11573/192908
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.
recursive data types, dagger operation, regular trees, 2-categories; algebraic theories; equational logic; fixed point operation; initiality; iteration theories; rewriting, Semantics in the theory of computing, Theories (e.g., algebraic theories), structure, and semantics, recursive functorial equations, data type specifications, tree transformations, Categorical semantics of formal languages, Double categories, \(2\)-categories, bicategories and generalizations, algebraic theories, Equational logic, Mal'tsev conditions, Free algebras, iteration 2-theories; free iteration 2-theories, 2-theory, Grammars and rewriting systems, algebraically complete categories, Cartesian structure, iteration theories, 2-categories
recursive data types, dagger operation, regular trees, 2-categories; algebraic theories; equational logic; fixed point operation; initiality; iteration theories; rewriting, Semantics in the theory of computing, Theories (e.g., algebraic theories), structure, and semantics, recursive functorial equations, data type specifications, tree transformations, Categorical semantics of formal languages, Double categories, \(2\)-categories, bicategories and generalizations, algebraic theories, Equational logic, Mal'tsev conditions, Free algebras, iteration 2-theories; free iteration 2-theories, 2-theory, Grammars and rewriting systems, algebraically complete categories, Cartesian structure, iteration theories, 2-categories
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 6 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
