Free SFP-algebras for truncation-closed sets of inequations

Based upon the idea that the syntax of a context free language can be described as an initial algebra and that the unique homomorphism to another algebra in that algebraic variety provides a semantic interpretation for programs in the language, it is of fundamental importance to know if a semantic category has free algebras. There are many categories of dcpo's for which the adjoint functor theorem serves to show the existence of free ordered S-E-DCPO-algebras for arbitrary presentations S-E. Jung showed that for the categories CONT (continuous dcpo's) and ALG (algebraic dcpo's), free S-E-algebras exist for finitary signatures, S, even though the adjoint functor theorem is not applicable in these cases. The category SFP is important for assigning semantics to parallel and nondeterministic programming language constructs and, for some time, it has been known that SFP has absolutely free algebras, that is, with no (in)equations imposed. The existence of free SFP-algebras for nonempty presentations, however, has been an open problem and the proof herein shows that for sets of inequations satisfying a condition named ‘truncation-closedness'’, free SFP-algebras exist.