Stephen L. Bloom

I&C Journal 2005 Journal Article

The equational theory of regular words

• Stephen L. Bloom
• Zoltán Ésik

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.

TCS Journal 2001 Journal Article

Long words: the theory of concatenation and ω-power

• Stephen L. Bloom
• Christian Choffrut

It is shown that for any set A, the algebra of ordinal words on the alphabet A equipped with the operations of concatenation and ω-power is axiomatized by the equations x·(y·z)=(x·y)·z, (x·y)ω=x·(y·x)ω, (xn)ω=xω, n⩾1. Indeed, the algebra freely generated by A in the variety determined by these equations is the algebra of tail-finite ordinal words of length <ωω on the alphabet A. It is further shown that this collection of identities cannot be replaced by any finite set. Last, a polynomial algorithm is given for recognizing when two terms denote the same tail-finite ordinal word.

TCS Journal 1997 Journal Article

The equational logic of fixed points

• Stephen L. Bloom
• Zoltán Ésik

TCS Journal 1996 Journal Article

Fixed-point operations on ccc's. Part I

• Stephen L. Bloom
• Zoltán Ésik

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.

TCS Journal 1996 Journal Article

Free shuffle algebras in language varieties

• Stephen L. Bloom
• Zoltán Ésik

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.

MFCS Conference 1994 Invited Paper

Solving Polynomial Fixed Point Equations

• Stephen L. Bloom
• Zoltán Ésik

TCS Journal 1990 Journal Article

A note on guarded theories

• Stephen L. Bloom

TCS Journal 1989 Journal Article

Equational logic of circular data type specification

• Stephen L. Bloom
• Zoltan Esik

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.

TCS Journal 1985 Journal Article

A logical characterization of observation equivalence

• Stephen L. Bloom
• Douglas R. Troeger

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.

TCS Journal 1979 Journal Article

Algebraic and graph theoretic characterizations of structured flowchart schemes

• Stephen L. Bloom
• Ralph Tindell

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.