Abstract Several fixed-point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed-point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed-point operation and binary supremum, but not involving residuals.

The axioms of iteration theories, or iteration categories, capture the equational properties of fixed point operations in several computationally significant categories. Iteration categories may be axiomatized by the Conway identities and identities associated with finite automata. We show that the Conway identities and the identities associated with the members of a subclass $\mathcal{Q}$ of finite automata is complete for iteration categories iff for every finite simple group G there is an automaton Q ∈ $\mathcal{Q}$ such that G is a quotient of a group in the monoid M(Q) of the automaton Q. We also prove a stronger result that concerns identities associated with finite automata with a distinguished initial state.

Journal Article Residuated Park theories Get access Z. Ésik Z. Ésik Dept. of Computer Science, University of Szeged, 6720 Szeged, Árpád tér 2, Hungary. Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 25, Issue 2, April 2015, Pages 453–471, https://doi.org/10.1093/logcom/ext001 Published: 05 February 2013 Article history Received: 22 September 2011 Published: 05 February 2013

Abstract Extensional higher-order logic programming has been introduced as a generalization of classical logic programming. An important characteristic of this paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we consider the semantics of negation in the context of the new paradigm. Using some recent results from non-monotonic fixed-point theory, we demonstrate that every higher-order logic program with negation has a unique minimum infinite-valued model. In this way we obtain the first purely model-theoretic semantics for negation in extensional higher-order logic programming. Using our approach, we resolve an old paradox that was introduced by W. W. Wadge in order to demonstrate the semantic difficulties of higher-order logic programming.

Partial iterative theories are algebraic theories such that for certain morphisms f the equation ξ = f ⋅ 〈ξ, 1p〉 has a unique solution. Iteration theories are algebraic theories satisfying a certain set of identities. We investigate some similarities between partial iterative theories and iteration theories. In our main result, we give a sufficient condition ensuring that the partially defined dagger operation of a partial iterative theory can be extended to a totally defined operation so that the resulting theory becomes an iteration theory. We show that this general extension theorem can be instantiated to prove that every Elgot iterative theory with at least one constant morphism 1 → 0 can be extended to an iteration theory. We also apply our main result to theories equipped with an additive structure.

An algebraic tree T is one determined by a finite system of fixed point equations. The frontier Fr(T ) of an algebraic tree T is linearly ordered by the lexicographic order <ℓ If (Fr(T) <ℓ) is well-ordered, its order type is an algebraic ordinal. We prove that the algebraic ordinals are exactly the ordinals less than ω $^{ω}$ $^{ω}$ .

The (in)equational properties of the least fixed point operation on (ω‐)continuous functions on (ω‐)complete partially ordered sets are captured by the axioms of (ordered) iteration algebras, or iteration theories. We show that the inequational laws of the sum operation in conjunction with the least fixed point operation in continuous additive algebras have a finite axiomatization over the inequations of ordered iteration algebras. As a byproduct of this relative axiomatizability result, we obtain complete infinite inequational and finite implicational axiomatizations. Along the way of proving these results, we give a concrete description of the free algebras in the corresponding variety of ordered iteration algebras. This description uses injective simulations of regular synchronization trees. Thus, our axioms are also sound and complete for the injective simulation (resource bounded simulation) of (regular) processes.

We show that, aside from the semiring equations, three equations and two equation schemes characterize the semiring of regular sets with the Kleene star operation.

What is special about the rules of Hoare logic?This paper shows that partial correctness logic can be viewed as a special case of the equational logic of iteration theories [6,7,24].It is shown how to formulate a partial correctness assertion {a} f { /3} as an equation between iteration theory terms.The guards (a, ~) that appear in partial correctness assertions are equationally axiomatized, and a new representation theorem for Boolean algebras is derived.The familiar rules for the structured programming constructs of composition, if-then-else and while-do are shown valid in all guarded iteration theories.A new system of partial correctness logic is described that applies to all flowchart programs.The invariant guard condition, weaker than the well-known condition of expressiveness.is found to be both necessary and sufficient for the completeness of these rules.The Cook completeness theorem [19] follows as an easy corollary.The role played by weakest liberal preconditions in connection with completeness is examined.

The equational properties of iteration, when combined with composition and pairing, are captured by the notion of “iteration theory,” which was introduced in [SIAM J. Comput., 9 (1980), pp. 26–45; 9 (1980), pp. 525–540]. We believe, although all of our evidence will not be exhibited here, that every iterative construction satisfies at least the properties of iteration theories. In this paper, axiomatizations are given for several varieties of iteration theories which occur naturally in the semantics of programming languages, i.e., those generated by theories of trees [J. Comput. Sys. Sci., 16 (1978), pp. 362–399], theories of sequacious functions [Proc. 1973 Colloquium, Vol. 80, Studies in Logic, North Holland, Amsterdam, 1975; pp. 175–230], theories of partial functions, and theories of both sequacious and partial functions with distinguished predicates. We show which additional equations must be added to the axioms for iteration theories [Comput. Ling. Comput. Lang., 14 (1980), pp. 183–207] in order to obtain a set of axioms for these subvarieties. Concrete descriptions of the free theories in each variety are given.