The paper considers partial iteration theories, which are Lawvere theories \(T\) [F. W. Lawvere, “Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories”, Repr. Theory Appl. Categ. 2004, No. 5, 1–121 (2004; Zbl 1062.18004)], equipped with a partial dagger operation, which is defined on a certain ideal \(D(T)\) of the set of morphisms of \(T\), and which additionally satisfies certain identities. In particular, if \(D(T)\) is the whole set of \(T\)-morphisms, then one obtains iteration theories of S. L. Bloom, C. C. Elgot and J. B. Wright [“Solutions of the iteration equation and extensions of the scalar iteration operation”, SIAM J. Comput. 9, 25–45 (1980; Zbl 0454.18011)] and Z. Esik [“Identities in iterative and rational algebraic theories”, Comput. Linguist. Comput. Lang. 14, 183–207 (1980; Zbl 0466.68010)]. Examples of iteration theories are the theories of order-preserving functions over complete partially ordered sets, which are equipped with the operation of least fixed-point as dagger.
A specific subclass of partial iteration theories make partial iterative theories, in which the condition on the existence of a dagger operation is replaced by the requirement of satisfaction of certain fixed-point equations. In the manuscript, the authors provide a sufficient condition, when a partial iterative theory gives rise to an iteration theory, i.e., when a partially defined dagger operation can be extended to a totally defined one, which, moreover, satisfies the identities of the induced operation. The obtained result incorporates several of the already existing extension theorems in the literature, e.g., the matrix extension theorem of S. Bloom and Z. Ésik [Iteration theories. The equational logic of iterative processes. EATCS Monographs on Theoretical Computer Science. Berlin: Springer- Verlag (1993; Zbl 0773.03033)] as well as the grove extension theorem of S. L. Bloom and Z. Ésik [“An extension theorem with an application to formal tree series”, J. Autom. Lang. Comb. 8, No. 2, 145–185 (2003; Zbl 1089.68051)], where grove theories are those Lawvere theories \(T\), which have an additive structure on their hom-sets (unlike the classical case of additive categories of, e.g., H. Herrlich and G. E. Strecker [Category theory. An introduction. 3rd ed., Sigma Series in Pure Mathematics 1. Lemgo: Heldermann Verlag (2007; Zbl 1125.18300)], composition distributes over sums on one side only).
The manuscript essentially consists of the proof of the above-mentioned dagger extension theorem (Theorem 4.4 on page 1044), its corollaries (in which the sufficient extension condition is restated in a different language), and several its applications, which eventually show the inclusion of the aforesaid two extension theorems in the current more general setting.
The language of the paper is quite technical. On the other hand, once the notations are got through, the rest is easy to follow, the paper being conveniently self-contained.