On second-order iterative monads
Abstract and axiomatic computability and recursion theory (03D75) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Accessible and locally presentable categories (18C35) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)
The object of this work is a categorical generalization of results by \textit{B. Courcelle} on solutions of recursive program schemes [Theor. Comput. Sci. 25, 95--169 (1983; Zbl 0521.68013)]. The setting of the generalization is to replace algebraic signatures with finitary endofunctors on locally finitely presentable categories, and then study the property of such functors being second-order iterative monads, i.e., admitting unique solutions of all guarded recursive program schemes, the latter referring to a natural categorical abstraction of the classical concept. Specifically, the authors construct, given a finitary endofunctor \(H\) on a locally presentable category, two second-order iterative monads over \(H\), the second order rational monad \(S^H\) and the context-free monad \(C^H\), which arises as the image of \(S^H\) in the free completely iterative monad \(T^H\) over \(H\) [\textit{P.\ Aczel} and the authors, Theor. Comput. Sci. 300, No.1--3, 1--45 (2003; Zbl 1028.68077)]. The monad \(S^H\) is then shown to be the initial second-order iterative monad over \(H\); moreover, both \(S^H\) and \(C^H\) are shown to be ideal in the sense of \textit{C. C. Elgot} [Logic Colloq. '73, Proc., Bristol 1973, 175--230 (1975; Zbl 0327.02040)]. In the classical case, i.e., when \(H\) is a polynomial endofunctor on \(\mathsf{Set}\), \(S^H\) coincides with Courcelle's monad of algebraic trees, where a tree is called algebraic if it can be defined by a guarded recursive program scheme. Several open problems are stated, in particular whether \(C^H\) is iterative and closed under second-order substitution, and whether \(S^H=C^H\).
- A coalgebraic view of infinite trees and iteration
- A fixpoint theorem for complete categories
- A Perspective View of Discrete Automata and Their Design
- Algebraic semantics
- Algebras, coalgebras, monads and comonads
- Coequalizers and free triples
- Completely iterative algebras and completely iterative monads
- Coproducts of Ideal Monads
- DPDA's in 'Atomic normal form' and applications to equivalence problems
- Dualising initial algebras
- Fundamental properties of infinite trees
- scientific article; zbMATH DE number 3458870 (Why is no real title available?)
- scientific article; zbMATH DE number 575948 (Why is no real title available?)
- Infinite trees and completely iterative theories: A coalgebraic view
- Iterative algebras at work
- Iterative reflections of monads
- Monads of coalgebras: rational terms and term graphs
- On the monadicity of finitary monads
- Parametric corecursion
- Recursive program schemes and context-free monads
- Regular trees and the free iterative theory
- Solving Algebraic Equations Using Coalgebra
- Some remarks on finitary and iterative monads
- The category-theoretic solution of recursive program schemes
- Some remarks on finitary and iterative monads
- A new foundation for finitary corecursion and iterative algebras
- A new foundation for finitary corecursion. The locally finite fixpoint and its properties
- Recursive program schemes and context-free monads
- Iterative reflections of monads
- A Description of Iterative Reflections of Monads (Extended Abstract)
- Generalizing Substitution
- Proper functors and fixed points for finite behaviour
- Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories
- Equational properties of iterative monads
This page was built for publication: On second-order iterative monads
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q639639)
