The existence and construction of free iterative theories

In "Monadic Computation and Iterative Algebraic Theories" by Calvin C. Elgot,the notion "iterative theory" (more fully, "ideal theory closed under conditional iteration") is introduced and applied to the study of computational processes. The main point of the present paper is to show the existence (in a constructive sense) of free iterative theories. The main complication is the fact that in an iterative theory I the "iteration" operation is not defined for all elements of I. Were it not for this complication, the existence of free iterative theories would follow from general algebraic considerations (extended to many-sorted algebras). Actually we sketch two proofs of the existence of free iterative theories. One argument follows as much as possible general algebraic lines and is given a linguistic flavor in order to emphasize the concreteness of the ideas involved. The second argument depends upon "normal descriptions": a morphism in the free iterative theory being an equivalence class of normal descriptions. © 1976 Academic Press, Inc.