On second-order iterative monads (Q639639)

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\).