Search

We prove the following theorem. Suppose that M is a trim DFA. Then \(\mathcal{L}(M)\) is well-ordered by the lexicographic order < l iff whenever the non sink states q, q.0 are in the same strong component, then q.1 is a sink. It is easy to see that this property is sufficient. In order to show the necessity, we analyze the behavior of a < l-descending sequence of words. This property is used to obtain a polynomial time algorithm to determine, given a DFA M, whether \(\mathcal{L}(M)\) is well-ordered by the lexicographic order. Last, we apply an argument in Bloom and Esik (Fundam Inform 99:383–407, 2010, Int J Found Comput Sci, 2011) to give a proof that the least nonregular ordinal is ωω.

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.

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.

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.)

Courcelle introduced the study of regular words, i.e., words isomorphic to frontiers of regular trees. Heilbrunner showed that a nonempty word is regular iff it can be generated from the singletons by the operations of concatenation, omega power, omega-op power, and the infinite family of shuffle operations. We prove that the nonempty regular words, equipped with these operations, are the free algebras in a variety which is axiomatizable by an infinite collection of some natural equations.

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.

Suppose that f: Q → Q is a partial function on a set Q, where we might think of Q as a set of “states” of a machine. If α and β are predicates on Q, i.e. total maps Q → {TRUE, FALSE}, partial correctness assertion {α} f {β}, pca for short, means $$ \forall q \in Q\left[ {\alpha \left( q \right) = {\text{TRUE}}\, \wedge f\left( q \right){\text{defined}}\, \Rightarrow \beta \left( {f\left( q \right) = {\text{TRUE}}} \right)} \right] $$ .

Matrix theories were discussed in Section 3.5. We proved there that each matrix theory is isomorphic to a matrix theory Mat S , for some semiring S. Hence in this chapter we will consider only these theories. When the matrix theory T = Mat S is a preiteration theory, then one can define a star operation on each hom-set T(n, n) as follows. When A is n × n, the matrix [A 1 n ] is a morphism n→n + nin T, and we define A* by the equation $$ A* = \left[ {A\,1_n } \right]^\dag $$ (1)

In many studies of computation which make use of rooted labeled trees a partial ordering is usually imposed on the trees in the following way. A particular label, say $ \bot _0 $, is distinguished and identified with the atomic tree whose only vertex is a leaf labeled $ \bot _0 $. A tree f is then defined to be less than a tree A tree g if g can be obtained from f by attaching some new trees to leaves of f labeled $ \bot _0 $.This paper answers the following questions. What is the significance of the tree $ \bot _0 $ in this ordering? Can other nonatomic and perhaps infinite trees $ \bot $ be used to define a partial ordering on the trees in the same way? If so, what if anything distinguishes the partial ordering defined via the atomic tree $ \bot _0 $?

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.