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 and 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 where 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 interpreted 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.
展开▼
机译:受 S. Kaplan 关于正/负条件重写的工作的启发,我们用 Gentzen 公式研究了代数规范的初始语义。由于标准初始方法仅限于条件方程(即正霍恩公式),因此引入了半初始和准初始代数的概念,并表明所有具有(正)根岑公式的规范都允许准初始模型。整个方法被推广到参数情况,其中准初始性推广到准自由性。由于准自由对象不一定是同构的,因此添加了持久性要求,以便为许多有趣的实际示例获得唯一的语义。如果参数类别的同态受到适当限制,则唯一持久的准自由语义可以被描述为自由构造。此外,事实证明,独特的持久性准无语义尤其适用于可以将 Gentzen 公式解释为分层正/负条件方程的规范。有限函数空间的数据类型构造函数用作一个示例,它不承认正确的初始语义,但允许正确的唯一持久准初始语义。该示例表明,本文中介绍的概念在实际应用中可能具有一定的重要性。
展开▼