On the algebraic specification of infinite objects - ordered and continuous models of algebraic types (Q1057642)

The concept of algebraic types is adapted to allow axiomatic characterizations of ordered and continuous algebras; infinite objects are then limit points in the carriers of certain continuous algebras. We mainly study implicative types, i.e., types the axioms of which are conditional inequations describing partial orders. The isomorphism classes of term-generated ordered models of an implicative type are shown to form a complete lattice under the homomorphism ordering; this includes the well-known initiality results for equational and conditional types as special cases. For types whose axioms specify strictness of the operations, the initial models are shown to correspond to flat domains. As a special kind of continuous algebras we consider inductively generated algebras, viz. the ideal completions of term-generated ordered algebras. For an inequational type, i.e., an implicative type where all axiom premises are empty, the completion of models always yields models again, whereas for implicative types this holds only in restricted cases. One such case is provided by hierarchic types which are complete and consistent relative to their primitive parts, and which satisfy certain conditions about limit points. Examples of algebras that can be specified by such types include those of finite and infinite streams, of sets of atoms under the Egli-Milner ordering, Milner's synchronisation trees, and that of a simple functional language over the natural numbers.