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

The main result of this paper is a generalization of the Mezei-Wright theorem, a result on solutions of a system of fixed point equations. In the typical setting, one solves a system of fixed point equations in an algebra equipped with a suitable partial order; there is a least element, suprema of @w-chains exist, the operations preserve the ordering and least upper bounds of @w-chains. In this setting, one solution of this kind of system is provided by least fixed points. The Mezei-Wright theorem asserts that such a solution is preserved by a continuous, order preserving algebra homomorphism. In several settings such as (countable) words or synchronization trees there is no well-defined partial order but one can naturally introduce a category by considering morphisms between the elements. The generalization of this paper consists in replacing ordered algebras by ''categorical algebras''; the least element is replaced by an initial element, and suprema of @w-chains are replaced by colimits of @w-diagrams. Then the Mezei-Wright theorem for categorical algebras is that initial solutions are preserved by continuous morphisms. We establish this result for initial solutions of parametric fixed point equations. One use of the theorem is to characterize an ''algebraic'' element as one that can arise as a solution of some system of fixed point equations. In familiar examples, an algebraic element is one that is context-free, regular or rational. Then, if h:A->B is a continuous morphism of categorical algebras, the algebraic objects in B are those isomorphic to h-images of algebraic objects in A.

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Esik, and iteration algebras are a special case of the recently introduced Elgot algebras (which are the monadic algebras for the free iterative monad). Another special case of iteration algebras are the iterative algebras of E. Nelson and J. Tiuryn, which are algebras with unique solutions of all guarded systems. For each of the above classes of algebras an example is provided showing that the inclusion in a wider class is proper.

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 algebra of nonempty regular words on the set A, equipped with these operations, is freely generated by A in a variety which is axiomatizable by an infinite collection of some natural equations. We also show that this variety has no finite equational basis and that its equational theory is decidable in polynomial time.

The axioms of iteration 2-theories capture, up to isomorphism, the equational properties of iteration in conjunction with horizontal and vertical composition in all algebraically complete categories. We give a concrete representation of the free iteration 2-theory generated by a 2-signature.

A V-labelled poset P can induce an operation on the languages on any fixed alphabet, as well as an operation on labelled posets (as noticed by Pratt and Gischer (Pratt 1986; Gischer 1988)). For any collection X of V-labelled posets and any alphabet Σ we obtain an X-algebra ΣX of languages on Σ. We consider the variety Lang(X) generated by these algebras when X is a collection of nonempty ‘traceable posets’. The current paper contains several observations about this variety. First, we use one of the basic results in Bloom and Ésik (1996) to show that a concrete description of the A-generated free algebra in Lang(X) is the X-subalgebra generated by the singletons (labelled a∈A) in the X-algebra of all A-labelled posets. Equipped with an appropriate ordering, these same algebras are the free ordered algebras in the variety Lang(X)[les ] of ordered language X-algebras. Further, if one enriches the language algebras by adding either a binary or infinitary union operation, the free algebras in the resulting variety are described by certain ‘closed’ subsets of the original free algebras. Second, we show that for ‘reasonable sets’ X, the variety Lang(X) has the property that for each n[ges ]2, the n-generated free algebra is a subalgebra of the 1-generated free algebra. Third, knowing the free algebras enables us to show that these varieties are generated by the finite languages on a two-letter alphabet.

We consider the varietyLanggenerated by all language structures (PΣ, ·, ⊗ +, 0, 1), and the varietyLg⩽of ordered algebras generated by the structures (PΣ, ·, ⊗ 0, 1, ⊆), wherePΣis the powerset ofΣ*, and whereB·Cis the complex concatenation of the languagesB, C⊆Σ*,B⊗Cis their shuffle product, andB+Cis their union. We prove that for each finite setEof equations valid inLangthere is a (finite) modelSEofEin which some inequation valid inLg⩽fails. It follows that neither variety is finitely axiomatizable.

An algebraic linear ordering is a component of the initial solution of a first-order recursion scheme over the continuous categorical algebra of countable linear orderings equipped with the sum operation and the constant 1. Due to a general Mezei-Wright type result, algebraic linear orderings are exactly those isomorphic to the linear ordering of the leaves of an algebraic tree. Using Courcelle's characterization of algebraic trees, we obtain the fact that a linear ordering is algebraic if and only if it can be represented as the lexicographic ordering of a deterministic context-free language. When the algebraic linear ordering is a well-ordering, its order type is an algebraic ordinal. We prove that the Hausdorff rank of any scattered algebraic linear ordering is less than ωω. It follows that the algebraic ordinals are exactly those less than ωωω.

Sabadini, Walters and others have developed a categorical, machine based theory of concurrency in which there are four essential aspects: a distributive category of data-types; a bicategory Mach whose objects are data types, and whose arrows are input-output machines built from data types; a semantic category (or categories) Sem, suitable to contain the behaviors of machines, and a functor, “behavior”: Mach→Sem. Suitable operations on machines and semantics are found so that the behavior functor preserves these operations. Then, if each machine is decomposable into primitive machines using these operations, the behavior of a general machine is deducible from the behavior of its parts. The theory of non-deterministic finite state automata provides an example of the paradigm and also throws some light on the classical theory of finite state automata. We describe a bicategory whose objects are natural numbers, in which an arrow M: n→p is a finite state automaton with n input states, p output states, and some additional internal states; we require that no transitions begin at output states or end at input states. A machine is represented by an q+n by q+p matrix. The bicategory supports additional operations: non-deterministic choice, parallel interleaving, and feedback. Enough operations are imposed on machines to show that each machine may be obtained from some atomic ones by means of the operations. The semantic category is the (Bloom-Esik) iteration theory Mat (X✶ whose objects are natural numbers and whose arrows from n to p are n×p matrices with entries in the semiring of languages. The behavior functor associates to a machine M: n→p a matrix |M| of languages, one language to each pair of input and output states. Behavior preserves composition, feedback, takes non-deterministic choice to union, and parallel-interleaving to shuffle. Thus, behavior gives a compositional semantics to a primitive notion of concurrent processes.

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 consider partial Conway semirings and partial iteration semirings, both introduced by Bloom, Esik, Kuich [2]. We develop a theory of cycle-free elements in partial iterative semirings that allows us to define cycle-free finite automata in partial iterative semirings and to prove a Kleene Theorem. We apply these results to power series over a graded monoid with discounting.

A result obtained in Ref. 2 for least prefixed points in order enriched cartesian closed categories is generalized to initiality in cartesian closed 2-categories. In brief, the result is that if a fixed point operation on a cartesian closed 2-category is defined by initiality, then under a mild condition, the operation satisfies the cartesian Conway identities and the abstraction identity. In addition, we show that the operation satisfies the power identities, and hence, except for the law a**=a*, the analogues of Conway’s classical identities for the regular sets.

We describe explicitly the free algebras in the equational class generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure and neutral elements 0 (empty relation) and 1 (identity relation). We show the corresponding equational theory is decidable by reducing the problem to a question about regular sets. Similar results are given for two related equational theories.

We solve fixed point equations over finite and infinite words by initiality. By considering equations without and with parameters, two families of words arise, the regular and the algebraic words. Regular words were introduced by Courcelle in the late 1970's. We provide a summary of results on regular words, some of which have been obtained very recently, and include some new results for algebraic words.

This paper extends Part 1 of the paper with the same title. Here, matricial iteration theories Matr(S; V) are characterized by identities involving theory operations, a star operation S → S and an omega operation S → V. The initial matricial iteration theory is described explicitly. One answer is given to the following question: If T0 is a submatricial theory of the matricial theory T which is an iteration theory, when can the star and omega operations on T0 be extended to T so that T becomes an iteration theory? Applications to program correctness logic and to finding equational axioms for the regular sets are indicated.

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

We assume the reader has some familiarity with theories and iteration theories. The main topic of the paper is properties of varieties of iteration algebras. After a preliminary section which contains all of the necessary definitions, we spend some time on a coproduct construction which is needed to prove a fundamental lemma: for each iteration theory T, any T-algebra is a retract of a T-iteration algebra. The proof of the lemma shows that only one property of iteration theories is used: the parameter identity. Hence, the lemma applies to any preiteration theory in which this identity is valid. It follows from this fact that the variety of all T-iteration algebras has “nice” properties only when every T-algebra is an iteration algebra. Some of the possible pathology in varieties of iteration algebras is demonstrated. It is shown that for each set Z of non-negative integers there is a variety of iteration algebras having an n-generated free algebra iff n∈Z. Also given is a theorem characterizing certain functors between varieties of iteration theories which are induced by iteration theory morphisms. We find an explicit description of all of the theory congruences on theories of partial functions. The last section is connected with the strong iteration algebras introduced in a paper by Ésik (1983).

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.

Algebras whose underlying set is a complete partial order and whose term-operations are continuous may be equipped with a least fixed point operation μx.t. The set of all equations involving the μ-operation which hold in all continuous algebras determines the variety of iteration algebras. A simple argument is given here reducing the axiomatization of iteration algebras to that of Wilke algebras. It is shown that Wilke algebras do not have a finite axiomatization. This fact implies that iteration algebras do not have a finite axiomatization, even by “hyperidentities”.

The axioms of iteration 2-theories capture the equational properties of iteration in conjunction with horizontal and vertical composition in all algebraically complete categories. We give a concrete representation of the free iteration 2-theory generated by a 2-signature.

There is some set of inequations t≤t∼ whose models are the algebras in the variety of ordered algebras generated by the algebras L ∑ =(P ∑ ,.,⊗,1) where P ∑ consists of all subsets of the free monoid ∑ *, B·C=uv∶u∈B, υ∈C, and B ⊗ C is the shuffle product of the two languages. We show that there is no finite set of such inequations.

All known structures involving a constructively obtainable fixed point (or iteration) operation satisfy the equational laws defining iteration theories. Hence, there seems to be a general equational theory of iteration. This paper provides evidence that there is no general implicational theory of iteration. In particular, the quasi-variety generated by the continuous ordered theories, in which fixed point equations have least solutions, is incomparable with the quasi-variety generated by the pointed iterative theories, in which fixed point equations have unique solutions.

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] $$ .

Recall the definition of matricial theories from Section 3.5.3. Since each matricial theory can be represented as a theory Matr(S; V) for some semiring module pair (S;V), we will be considering only matricial theories of this sort. A matricial iteration theory is a matricial theory which is simultaneously an iteration theory. We show that when T = Matr(S; V) is a matricial iteration theory, the dagger operation determines and is determined by a star operation on the semiring S and an omega operation ω: S → V from the semiring to the module.

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)

We will review briefly some of the main concepts of standard universal algebra in order to motivate the definition of one of our central concepts: algebraic theories. We will show how theories are related to equational classes of algebras. Most of the facts mentioned in this chapter are well-known in some form.

The analysis of partial correctness assertions given in [Bea] is specialized to matricial iteration theories. A system of rules for partial correctness is given and a completeness theorem is stated. It is shown how to formulate total correctness in all iteration theories as an equation, and some total correctness rules are considered.