Parametric algebraic specifications with gentzen formulas - from quasi-freeness to free functor semantics

Inspired by the work of S. Kaplan on positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen formulas. Since the standard initial approach is limited to conditional equations(i.e. positive Horn formulas), the notion of semi-initial an quasi-initial algebras is introduced, and it is shown that all specifications with (positive) Gentzen formulas admit quasi-initial models. The whole approach is generalized to the parametric case wher quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction if the homomorphisms of the parameter category are suitably restricted. Furthermore, it turns out that unique persistent quasi-free semantics applies especially to specifications where the Gentzen formulas can be interpre ted as hierarchical positive/negative conditional equations. The data type constructor of finite function spaces is used as an example that does not admit a correct initial semantics, but does admit a correct unique persistent quasi-initial semantics. The example demonstrates that the concepts introduced in this paper might be of some importance in practical applications.