Search

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.

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.

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

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.

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.

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 1978, Courcelle asked for a complete set of axioms and rules for the equational theory of (discrete regular) words equipped with the operations of product, omega power and omega-op power. In this paper we find a simple set of equations and prove they are complete. Moreover, we show that the equational theory is decidable in polynomial time.

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.

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.

The syntax and the semantics of flowchart algorithms may be conveniently separated. The syntax of a flowchart algorithm is the underlying flowchart scheme. The semantics is given by an interpretation of each symbol appear ing on the nodes of the scheme. One aspect of this theory is the determination of when two schemes have the same “behavior” under all interpretations. When “behavior” is interpreted in the strongest sense as “performing the same stepwise computations,” the collection of equivalence classes of schemes was shown by Elgot [E-MC] to have the structure of an “iterative theory.” The strong behavior of a scheme is precisely captured by the (labeled, locally ordered, locally finite) tree obtained by “unfolding” the scheme in the familiar way. (When the “behavior” of a scheme F is considered to be the partial input-output function computed by F in each interpretation, certain quotients of the trees are the appropriate interpretations.) The collection of labeled schemes and trees is equipped with the same structure, which is preserved by the map which takes a scheme F to its strong behavior [F]. This structure is simple to describe: starting from the atomic and “base” schemes, using just three operations (composition, tupling, and iteration), any scheme may be constructed. The operation of iteration (or “looping”) on schemes and trees was not defined in all cases in the setup of [E-MC]; for example, consider the scheme 1 -+ 1 consisting of only an exit (and the tree which forms its strong behavior). Thus the schemes and trees form a partial algebra. It was to remedy this situation on the semantic algebras of trees and other iterative theories that the notion of an “iteration” theory was introduced (in [BEW]). Iteration theories are (total) algebras with the same operations as iterative theories. The collection of trees which are strong behaviors of schemes may be given the structure of an iteration theory by completing the iteration operation in an almost arbitrary way. The collection of iteration theories is the class of all mode ls of the set of equations valid in all iteration theories of trees. (See [BEW] for details.)

The paper concerns the relationship between graph theoretic and algebraic properties of structured flowchart schemes. For each of ten classes of flowchart schemes defined algebraically, a graph theoretic property is given which characterizes this class. The classes include the Dijkstra schemes, Elgot's CACI and G -schemes, the reducible schemes and Kosaraju's BJn-schemes. For two classes of schemes defined by a graph theoretic property, an equivalent algebraic characterization is found.

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.

An abstract logic 〈A, C〉 consists of a finitary algebraA and a closure systemC onA. C induces two other closure systems onA, CP andCI, by projective and inductive generation respectively. The various relations amongC, CP andCI are determined. The special case thatC is the standard equational closure system on monadic terms is studied in detail. The behavior of Boolean logics with respect to projective and inductive generation is determined.

Two characterizations are given of those structural consequence operations on a propositional language which can be defined via proofs from a finite number of polynomial rules.

A pair (C,U) consisting of a category C with coequalizers and a functor U: C → Set is a weak quasi-variety if U has a left adjoint and U preserves and reflects regular epis. It is known that every weak quasi-variety is equivalent to a concrete quasi-variety, i.e. a category of Σ-algebras which has all free algebras and which is closed with respect to products and subalgebras. It is also known that if U preserves monic direct limits, C is equivalent to a concrete quasi-variety of Σ-algebras in which Σ contains no function symbols of infinite rank; and if U preserves all direct limits, C is equivalent to a concrete quasi-variety of Σ-algebras definable by a set of implications of the form (t1 = s1∧⋯∧tm = sm) ⇒ tm+1 = sm+1 where ti and si are Σ-terms and m is a nonnegative integer. This paper concerns several definitions of ‘finiteness’ in a category theoretic setting and some theorems on weak quasi-varieties. Two main theorems characterize those weak quasi-varieties (C, U) such that U preserves all direct limits.

A signed ∑-equation is an expression of the form t ≈ t′ or t ≉t′, where t and t′ are ∑-terms (for some ranked set ∑). We characterize those classes of ∑-algebras which are models of a set of signed ∑-equations. Further we consider the problem of finding a complete deductive system analogous to equational logic for the logical consequence operation restricted to signed equations.

A system Σ of recursion equations is a finite set of equations ϕi = ti i = 1,…, n, where the expressions ti denote terms built from individual variables, “function constants,” and the “function variables” ϕ1,…,ϕn. An interpretation of such a system assigns a meaning to each function constant and a possible meaning to each individual and function variable. Standard interpretations have imposed an ordering on the class of possible “solutions” of Σ and only the least (or greatest) solution is found. In this paper contraction theories are defined and used as interpretations for Σ. Several known kinds of interpretations are shown to be contraction theories, including the collection of rooted labeled trees. No ordering is imposed on solutions in a contraction theory, but a metric is involved. All solutions of Σ in any contraction theory are described.

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.

1. The SCI (Sentential Calculus with Identity) is obtained from the classical sentential calculus by the addition of (1) a new binary connective, the identity con? nective (denoted by"=") and (2) axioms which 'say5 that "p == q" means ccp is identical to q" (also: "the situation p is the same as the situation q"). The new axioms are the weakest possible; no presuppositious about the meaning of "is identical to35 are in? cluded (other than "p = p"). We do not attempt to say what the range of the sentential variables p,q,r, ... is. (In the classical propositional calculus, they are intended to range over a two element set.) In this paper, a number of results about the semantics of the SCI are given without proof. The proofs of these and other results are contained in the much longer "In? vestigations into the Sentential Calculus with Identity53 [1].

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.

Matrix iteration theories are characterized by identities using theory operations as well as a star operation on T(n, n), for each n ⩾ 0. The initial matrix iteration theory is described explicitly. An extension theorem is proved which implies that if MatS is a matrix iteration theory, so is MatR where R is a semiring of formal power series over S. In Part II these results are extended to Elgot's matricial theories.

In “Monadic Computation and Iterative Algebraic Theories” Elgot [3] introduced the notion of a vector iterative theory and showed that vector iterative theories have a close connection with several aspects of the theory of computation. In private conversations Elgot formulated the notion of a scalar iterative theory and raised the question whether scalar and vector iterative theories coincide. We answer this question in the affirmative.

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.

In ''Monadic Computation and Iterative Algebraic Theories'' by Calvin C. Elgot,the notion ''iterative theory'' (more fully, ''ideal theory closed under conditional iteration'') is introduced and applied to the study of computational processes. The main point of the present paper is to show the existence (in a constructive sense) of free iterative theories. The main complication is the fact that in an iterative theory I the ''iteration'' operation is not defined for all elements of I. Were it not for this complication, the existence of free iterative theories would follow from general algebraic considerations (extended to many-sorted algebras). Actually we sketch two proofs of the existence of free iterative theories. One argument follows as much as possible general algebraic lines and is given a linguistic flavor in order to emphasize the concreteness of the ideas involved. The second argument depends upon ''normal descriptions'': a morphism in the free iterative theory being an equivalence class of normal descriptions.

Synchronization trees are shown to form an iteration theory in a natural way. The class of grove iteration theories is introduced. The regular synchronization trees are shown to be the free theories in the subclass of synchronization theories. Moreover, the bisimulation equivalence classes of regular synchronization trees are shown to be the free synchronization theories satisfying an ‘infinite’ idempotency law.

Consider how one might describe the sequences of atomic actions IF] performable by a s tandard deterministic flowchart scheme F . One can exhibit F as a finite directed graph whose vertices are labeled with letters in a ranked alphabet ~2 (if the vertex v has outdegree k, then the letter labeling v is in the set ~k ). Then we say that the set [F] is the set of all labels of paths in F from the 'begin vertex' to the exit. If one wants to refine this notion further, one can associate a labeled tree with F, the so called 'unfolding' of F , and define [F] as this tree. To describe the tree in great detail, one can show how to associate a tree of depth at most one with each node in the underlying graph of F . This association takes the form of a system of equations. For example, suppose that F is the flowchart scheme