Iterative theories were introduced by Elgot in order to formalize potentially infinite computations as unique solutions of recursive equations. The original proof that a free iterative theory can be described as the theory of all rational trees was extremely complicated; in this paper, an much simpler proof is provided.
Firstly, it is proved that all finitary endofunctors \(H\) generate a free iterative monad \(R\); the only assumption needed is that the base category is locally finitely presentable. The key point in the proof was to recall that iterative algebras are more basic that Elgot’s iterative theories, as noted by E. Nelson [Theor. Comput. Sci. 25, 67–94 (1983; Zbl 0533.03014)] and J. Tiuryn [Theor. Comput. Sci. 12, 229-254 (1980; Zbl 0439.68026)].
The main technical result is a description of an initial iterative algebra as a colimit of all \(H\)-coalgebras carried by finitely presentable objects. From this result, the algebraic theory formed by all free iterative \(H\)-algebras was proved to be iterative in Elgot’s sense.