Search

We give simple concrete descriptions of the free algebras in the varieties generated by the “shuffle semirings” LΣ := (P(Σ∗),+,., ⊗, 0,1), or the semirings RΣ := (R(Σ∗),+,., ⊗,∗,0,1), where P(Σ∗) is the collection of all subsets of the free monoid Σ∗, and R(Σ∗) is the collection of all regular subsets. The operation x ⊗ y is the shuffle product.

Let Σ be a ranked set. A categorical Σ-algebra, cΣa for short, is a small category C equipped with a functor σC: C n →C, for each σ ∈ Σn, n ≥ 0. A continuous categorical Σ-algebra is a cΣa which has an initial object and all colimits of ω-chains, i.e., functors ℕ≥C; each functor σc preserves colimits of ω-chains. (ℕ is the linearly ordered set of the nonnegative integers considered as a category as usual.)

In the late 1970's, Courcelle introduced the class of ``arrangements'', or labeled linear ordered sets, here called just ``words''. He singled out those words which are solutions of finite systems of fixed point equations involving finite words, which we call the ``regular words''. The current paper contains some new descriptions of this class of words related to properties of regular sets of binary strings, and uses finite automata to decide various natural questions concerning these words. In particular we show that a countable word is regular iff it can be defined on an ordinary regular language (which can be chosen to be a prefix code) ordered by the lexicographical order such that the labeling function satisfies a regularity condition. Those regular words whose underlying order is ``discrete'' or ``scattered'' are characterized in several ways.

This paper is concerned mainly with classes (categories) of ordered algebras which in some signature are axiomatizable by a set of inequations between terms (‘varieties’ of ordered algebras) and also classes which are axiomatizable by implications between inequations (‘quasi varieties’ of ordered algebras). For example, if the signature contains a binary operation symbol (for the monoid operation) and a constant symbol (for the identity) the class of ordered monoids M can be axiomatized by a set of inequations (i.e. expressions of the form t ≤ t' . However, if the signature contains only the binary operation symbol, the same class M cannot be so axiomatized (since it is not now closed under subalgebras). Thus, there is a need to find structural, signature independent conditions on a class of ordered algebras which are necessary and sufficient to guarantee the existence of a signature in which the class is axiomatizable by a set of inequations (between terms in this signature). In this paper such conditions are found by utilizing the notion of ‘P-categories’. A P-category C is a category such that each ‘Hom-set’ C ( a,b ) is equipped with a distiguished partial order which is preserved by composition. Aside from proving the characterization theorem, it is also the purpose of the paper to begin the investigation of P-categories.

A variety of ordered algebras is a class K of ordered algebras satisfying satisfying a set of inequalities [email protected]?t'. It is shown that a class K of ordered algebras is a variety if K is closed under subalgebras, products, and certain homomorphic images. The process of obtaining a ''canonical'' @w-completion of an ordered algebra is analyzed and it is shown that varieties of ordered algebras are closed with respect to @w-completion. The concluding sections concern (i) a connection between ordered algebras and ordered algebraic theories, and (ii) a logic of inequalities, analogous to equational logic. A completeness theorem for this logic is proved.

Brookes and Rounds (1983) showed that a finitary formal language (‘regular trace language’, or Reg-TL, for short) which allowed a certain kind of quantification using regular subsets of Σ∗ was not strong enough to distinguish all pairs of observationally inequivalent synchronization trees. In the present paper we extend this result to show that there is no class C of subsets of Σ∗ such that C-TL can distinguish all pairs of observationally inequivalent synchronization trees. We then give a characterization of observation equivalence in terms of an infinitary formal language S-TL(ω). This language is obtained as an extension of the language S-TL (‘singleton trace language’) of Hennessy and Milner by the addition of a connective of ω-conjunctions of formulas of finite bounded deoth.

Most studies of fixed points involve their existence or construction. Our interest is in their equational properties. We study certain equational properties of the fixed-point operation in computationally interesting cartesian closed categories. We prove that in most of the poset categories that have been used in semantics, the least fixed-point operation satisfies four identities we call the Conway identities. We show that if %plane1D;49E; 0 is a sub-ccc of any ccc %plane1D;49E; with a fixed-point operation satisfying these identities, then there is a simple normal form for the morphisms in the least sub-ccc of %plane1D;49E; containing %plane1D;49E; 0 closed under the fixed-point operation. In addition, the standard functional completeness theorem is extended to Conway ccc's.

Iteration theories, introduced by Bloom, Elgot and Wright in (1980), formalize the equational properties of the strong behaviors of flowchart algorithms. We show that the same equational properties are shared by the functors used to specify circular data types. Lehmann and Smyth (1981) have shown how to specify circular data types, such as stacks, as fixed points of certain functors (the-called gw -functors). For example, the set of stacks of elements in the set A is a solution to the equation in the variable X , X = F ( A , X ) where F ( X , X ) ≔ = 1 + A × X is the functor on SET taking the pair ( A , X ) to the disjoint union of the singleton set 1 and the product A × X . Such equations have initial solutions, F † ( A ), which in turn determine a ‘solution functor’ F † . The equational properties of the operation F ↦ F † are precisely captured by the axioms for iteration theories. More precisely, we show how the structure Th ω ( C ) of all ω-functors C n → C p , n , p ⩾ 0, on the ω-category C , forms an iteration theory and, conversely, any identity valid in all such structures is valid in the class of all iteration theories.

Iteration semi-rings are Conway semi-rings satisfying Conway's group identities. We show that the semi-rings N^r^a^t > of rational power series with coefficients in the semi-ring N of natural numbers are the free partial iteration semi-rings. Moreover, we characterize the semi-rings N"~"^"r"^"a"^"t > as the free semi-rings in the variety of iteration semi-rings defined by three additional simple identities, where N"~ is the completion of N obtained by adding a point of infinity. We also show that this latter variety coincides with the variety generated by the complete, or continuous semirings. As a consequence of these results, we obtain that the semi-rings N"~^r^a^t >, equipped with the sum order, are free in the class of symmetric inductive ^*-semi-rings. This characterization corresponds to Kozen's axiomatization of regular languages.