BRICS RS-02-46 Ésik & Leiß: Greibach Normal Form in Algebraically Complete Semirings BRICS

Basic Research in Computer Science

Greibach Normal Form in Algebraically Complete Semirings

Zoltán Ésik Hans Leiß BRICS Report Series RS-02-46 ISSN 0909-0878 December 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Zoltán Ésik & Hans Leiß.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/46/

Greibach Normal Form in Algebraically Complete Semirings

Zoltán Ésik^{∗} Dept. of Computer Science

University of Szeged Szeged, Hungary

esik@inf.u-szeged.hu

Hans Leiß^{†} CIS University of Munich Munich, Germany

leiss@cis.uni-muenchen.de

Dec 28, 2002

Abstract

We give inequational and equational axioms for semirings with a fixed-point operator and formally develop a fragment of the theory of context-free languages. In particular, we show that Greibach’s normal form theorem depends only on a few equational properties of least pre-fixed-points in semirings, and elimination of chain- and deletion rules depend on their inequational properties (and the idempotency of addition). It follows that these normal form theorems also hold in non-continuous semirings having enough fixed-points.

Keywords: Greibach normal form, context-free languages, prefixed-point induction, equational theory, Conway semiring, Kleene algebra, algebraically complete semiring

1 Introduction

It is well-known that the equational theory of context-free languages is not recursively enumerable, i.e. the equivalence problem for context-free grammars is not semi-decidable. This may have been the reason why little work has been done to develop a formal theory for the rudiments of the theory of context-free languages.

∗Supported in part by BRICS, Denmark, and the National Foundation of Hungary for Scientific Research, grant T35163.

†Supported in part by the Alexander von Humboldt Foundation.

In contrast, the equational theory of regular languages is decidable, and several axiomatizations of it appeared, using regular expressions as a notation system. In the 1970s, axiomatizations by schemata of equations between regular expressions were conjectured by Conway[9]. Salomaa[26] gave a finite first-order axiomatization based on a version of the unique fixed-point rule. Redko[24] showed that the theory does not have a finite equational basis. Twenty years later, Pratt[23] showed that a finite equational axiomatization is possible if one extends the regular operations +, · and ^{∗} by the left- and right residuals / and \ of ·. The important new axiom was (a/a)^{∗} = (a/a), the axiom of ‘pure induction’. (For a recent extension of Pratt’s methods, see Santocanale[27].) Earlier, Krob[18] confirmed several conjectures of Conway including the completeness of Conway’s group identities. He also gave several finite axiomatizations, including a system having, in addition to a finite number of equational axioms, a Horn formula expressing that a^{∗}b is the least solution of ax + b ≤ x. See also Boffa[7, 8], Bloom and Ésik[6], Bernátsky e.a.[4]. Independently, Kozen[16] defined a Kleene algebra as an idempotent semiring equipped with a ^{∗} operation subject to the above Horn-formula and its dual asserting that b^{∗}a is the least solution of xa + b ≤ x. He gave a direct proof of the completeness of the Kleene algebra axioms with respect to the equational theory of the regular sets.

With a least-fixed-point operator μ, these axioms of KA can be expressed as a^{∗}b = μx(ax + b) and ba^{∗} = μx(xa + b). Hence it is natural to extend the regular expressions by a construction μx.r, which gives a notation system for context-free languages. Extensions of KA by μ have been suggested in [20] to axiomatize fragments of the theory of context-free languages.

In this paper we look at axioms for semirings with a least-fixed-point operator that are sufficient to prove some of the normal form theorems for context-free grammars. In particular, we derive the Greibach[12] normal form theorem using only equational properties of least fixed-points. Our proof gives the efficient algorithm of Rosenkrantz[25], but avoids the analytic method of power series of his proof. Our axioms also imply that context-free grammars have normal forms without chain rules or deletion rules. An important aspect is that we do not use the idempotency of +, except for the elimination of deletion rules, and so the classical theorems are extended to a wide class of semirings.

Recently, Parikh’s theorem, another classical result on context-free languages, has been treated in a similar spirit. Hopkins and Kozen[15] generalized this theorem to an equation schema valid in all commutative idempotent semirings with enough solutions for recursion equations, also replacing analytic methods by properties of least fixed-points. A purely equational proof is given in [1].

2 Park μ-semirings and Conway μ-semirings

We will consider terms, or μ-terms defined by the following syntax, where x ranges over a fixed countable set X of variables:

T ::= x | 0 | 1 | (T + T) | (T · T) | μx T

For example, μx(x + 1) is a term. To improve readability, we write μx.t instead of μx t when the term t is 0, 1, a variable or not concretely given. With μx.t[s/y] we mean μx(t[s/y]), not (μx.t)[s/y]. The variable x is bound in μx.t. The set free(t) of free variables of a term t is defined as usual. We call a term closed if it has no free variables and finite if it contains no subterm of the form μx.t. Below we will write t(x_{1}, …, x_{n}) or t(x⃗), where x⃗ = (x_{1}, …, x_{n}), to indicate that the free variables of term t belong to the set {x_{1}, …, x_{n}}. We identify any two terms that only differ in the names of the bound variables and write t ≡ s for syntactic identity of s and t, up to renaming of bound variables. Substitution t[t′/x] of t′ for x in t and simultaneous substitution t[(t_{1}, …, t_{n})/(x_{1}, …, x_{n})] are defined as usual.

We will be interested in interpretations where μx.t provides solutions to the fixed-point equation x = t.

Definition 2.1 A μ-semiring is a semiring (A, +, ·, 0, 1) with an interpretation (·)_{A} of the terms t as functions t_{A} : A^{X} → A, such that

1. for each environment ρ ∈ A^{X}, all variables x ∈ X and all terms t, t′:

(a) 0_{A}(ρ) = 0, 1_{A}(ρ) = 1, x_{A}(ρ) = ρ(x), (t + t′)_{A}(ρ) = t_{A}(ρ) + t′_{A}(ρ), (t · t′)_{A}(ρ) = t_{A}(ρ) · t′_{A}(ρ),

(b) the ‘substitution lemma’ holds, i.e. (t[t′/x])_{A}(ρ) = t_{A}(ρ[x ↦ t′_{A}(ρ)]), 2. for all terms t, t′ and variables x ∈ X, if t_{A} = t′_{A}, then (μx.t)_{A} =

(μx.t′)_{A}.

A weak ordered μ-semiring is a μ-semiring A equipped with a partial order ≤ such that all term functions t_{A} are monotone with respect to the pointwise order. An ordered μ-semiring is a weak ordered μ-semiring A such that for any two terms t, t′ and variable x, if t_{A} ≤ t′_{A} in the pointwise order, then (μx.t)_{A} ≤ (μx.t)_{A}.

In a μ-semiring A, the value t_{A}(ρ) does not depend on ρ(x) if x does not have a free occurrence in t. As usual, ρ[x ↦ a] is the same as ρ except that it maps x to a. A term equation t = t′ holds or is satisfied in a μ-semiring A, if t_{A} = t′_{A}. A term inequation t ≤ t′ holds in a μ-semiring A equipped with a partial order ≤, if t_{A} ≤ t′_{A} in the pointwise order on A^{X}. An implication t = t′ → s = s′ holds in A, if for all ρ ∈ A^{X}, whenever t_{A}(ρ) = t′_{A}(ρ), then also s_{A}(ρ) = s′_{A}(ρ). Likewise with inequations.

Definition 2.2 A strong μ-semiring is a μ-semiring A where ∀x(t = t′) → μx.t = μx.t′ holds, for all terms t, t′ and variables x ∈ X. A strong ordered μ-semiring is a weak ordered μ-semiring A where ∀x(t ≤ t′) → μx.t ≤ μx.t′ holds, for all terms t, t′ and variables x.

The validity of ∀x(t = t′) → μx.t = μx.t′ implies the second condition in Definition 2.1.

Definition 2.3 A Park μ-semiring is a weak ordered μ-semiring satisfying the fixed-point inequation (1) and the pre-fixed-point induction axiom (2), also referred to as the Park induction rule, for all terms t and x, y ∈ X:

t[μx.t/x] ≤ μx.t,  (1)
t[y/x] ≤ y → μx.t ≤ y.  (2)

Proposition 2.4 Any Park μ-semiring A is a strong ordered μ-semiring satisfying the composition identity (3) and the diagonal identity (4)

μx.t[t′/x] = t[μx.t′[t/x]/x]  (3)
μx.μy.t = μx.t[x/y],  (4)

for all terms t, t′ and all variables x, y.

Note that taking t′ to be x in (3) gives the fixed point equation for t,

μx.t = t[μx.t/x].  (5)

Proof. To prove that A is a strong ordered μ-semiring, suppose for terms t, t′ and ρ ∈ A^{X} that t_{A}(ρ[x ↦ a]) ≤ t′_{A}(ρ[x ↦ a]), for all a ∈ A. Since t_{A} is monotone, it follows that every pre-fixed-point of the map a ↦ t′_{A}(ρ[x ↦ a]) is a pre-fixed-point of the map a ↦ t_{A}(ρ[x ↦ a]). Hence, (μx.t)_{A}(ρ) ≤ (μx.t′)_{A}(ρ). Equations (3) and (4) are established in Niwinski [22]. □

Definition 2.5 A Conway μ-semiring is a μ-semiring satisfying the Conway identities (3) and (4), for all terms t, t′ and variables x, y.

In the following, when t(x⃗) is a term and a⃗ an appropriately sized tuple of elements of a μ-semiring A, we often write t(a⃗) instead of t_{A}([x⃗ ↦ a⃗]).

3 Algebraically complete semirings

An ordered semiring is a semiring (S, +, ·, 0, 1) equipped with a partial order ≤ such that the + and · operations are monotone in both arguments. If + is idempotent and 0 is the least element, then ≤ is the semilattice order x ≤ y : ⟺ x + y = y, because x ≤ y ⇒ x + y ≤ y + y = y = 0 + y ≤ x + y and x + y = y ⇒ x = x + 0 ≤ x + y = y. Note that each weak ordered μ-semiring is an ordered semiring.

For any term t, we introduce the left iteration t^{ℓ} and the right iteration t^{r} of t by

t^{ℓ} := μz(zt + 1)  and  t^{r} := μz(tz + 1),

where z is a variable not free in t.

Definition 3.1 An algebraically complete semiring is a Park μ-semiring which satisfies the inequations

x^{r}y ≤ μz(xz + y)  (6)
yx^{ℓ} ≤ μz(zx + y).  (7)

By Proposition 2.4, every algebraically complete semiring satisfies the composition (3) and diagonal identities (4), hence also the fixed-point identity (5).

Proposition 3.2 Any algebraically complete semiring S satisfies the following (in)equations:

0 ≤ x  (8)
x ≤ x + y  (9)
x^{r}y = μz(xz + y)  (10)
yx^{ℓ} = μz(zx + y)  (11)
x^{r} = x^{ℓ}.  (12)

Proof. As for (8), note that by (6)

0 = 1^{r} · 0 ≤ μx.x

holds in S. But by the Park induction rule, (μx.x)_{S} is the least element of S.

Inequation (9) follows from (8) using the fact that each Park μ-semiring is an ordered semiring, hence + is monotone.

To show (10), note that we have

xx^{r} + 1 ≤ x^{r}

by the fixed-point inequation (1), hence

x(x^{r}y) + y ≤ x^{r}y

by monotonicity. By the Park induction rule, this gives

μz(xz + y) ≤ x^{r}y.

The reverse inequation is (6). Dually, we have (11).

As for (12), applying the composition identity

μz.t[s/z] = t[μz.s[t/z]/z]

to t := xz + 1 and s := yz, we obtain

(xy)^{r} = x · μz(y(xz + 1)) + 1
= x · μz((yx)z + y) + 1
= x(yx)^{r}y + 1,

using equation (10) in the last step. In particular,

y^{r} = y^{r}y + 1.

Thus, by the Park induction rule we have

y^{ℓ} = μz(zy + 1) ≤ y^{r}.

Similarly, using (11) we get y^{r} ≤ y^{ℓ}, so that y^{ℓ} = y^{r}. □

By (12), two possible definitions of iteration, left and right iteration, coincide in any algebraically complete semiring. With a variable z not free in t, we define the term

t^{∗} := μz(tz + 1).  (13)

On algebraically complete semirings A, we obtain a ^{∗}-operation with a^{∗} = a^{r} = a^{ℓ} for all a.

Remark 3.3 If we think of μ-terms as programs with + as non-deterministic choice, · as sequential composition, and μ as recursion, then (10) and (11) reduce tail- and head recursion to iteration ^{∗} and sequential composition (cf. [20]). Equation (10) is related to the parameter equation of [6].

We now give some examples of algebraically complete semirings.

Example 3.4 A continuous semiring is a semiring S = (S, +, ·, 0, 1) equipped with a complete partial order ≤ such that 0 is its least element and the + and · operations are continuous, i.e., they preserve in each argument the sup of any directed nonempty set. Any continuous semiring S gives rise to an algebraically complete semiring where μx.t provides the least solution to the fixed-point equation x = t (see [6]).

Let ℕ denote the set of nonnegative integers and let ℕ_{∞} = ℕ ∪ {∞}. Equipped with the usual order and + and · operations, ℕ_{∞} is a continuous semiring. Also, every finite ordered semiring having 0 as least element such as the boolean semiring 𝔹 = {0, 1} is continuous. Thus, ℕ_{∞} and 𝔹 are algebraically complete semirings.

Other prime examples of continuous semirings are the semiring L_{A} of all languages in A^{∗}, where A is a set, + is set union, · is concatenation and ≤ is set inclusion, and the semiring ℕ_{∞}⟨⟨A^{∗}⟩⟩ of power series over A with coefficients in ℕ_{∞}, equipped with the pointwise order.

The set R_{M} of all binary relations on the set M, where + is union, · the relation product, 0 the empty relation, 1 the diagonal on M and ≤ is inclusion, is a continuous semiring. In this example, r^{∗} is the reflexive transitive closure of r.

Example 3.5 The context-free languages in L_{A} form an algebraically complete semiring as do the algebraic power series in ℕ_{∞}⟨⟨A^{∗}⟩⟩. Unless A is empty, neither of these semirings is continuous. Given a set A of binary relations over the set M, let R_{M}(A) be the values in R_{M} of all μ-terms with parameters from A. Then R_{M}(A) is also an algebraically complete semiring, which is generally not continuous.

Example 3.6 By the completeness of first-order logic, the first-order theory, and in particular the equational theory of (idempotent) algebraically complete semirings is recursively enumerable. Now, the context free languages are free for the class of idempotent semirings that can be embedded in continuous idempotent semirings (cf. [20]). Thus the equational theory of idempotent continuous semirings is not recursively enumerable. It follows that there exist algebraically complete idempotent semirings that cannot be embedded in a continuous (idempotent) semiring. In fact, when the alphabet A has two or more letters, the free idempotent algebraically complete semiring on A does not embed in a continuous semiring. The same holds for the free algebraically complete semirings.

Using the fixed-point inequation and monotonicity, one easily gets:

Proposition 3.7 In any algebraically complete semiring, for all elements a and n ∈ ℕ

(∑_{i=0}^{n} a^{i}) ≤ a^{∗}.  (14)

We prove a few more basic equations. For any integer n ≥ 0, we will denote by n also the term which is the n-fold sum of 1 with itself. When n is 0, this is just the term 0.

Proposition 3.8 In any algebraically complete semiring, for any element a with a^{∗} + 1 ≤ a^{∗} we have

a^{∗} = a^{∗} + 1 = a^{∗} + a^{∗} = a^{∗} · a^{∗} = a^{∗∗}.  (15)

In particular, (15) holds for any a such that 1 ≤ a.

Proof. First, note that if 1 ≤ a, then also

a^{∗} + 1 ≤ aa^{∗} + 1
≤ a^{∗},

by the fixed-point inequation. Now suppose a^{∗} + 1 ≤ a^{∗}. By the fixed-point inequation,

aa^{∗} + 2 = aa^{∗} + 1 + 1
≤ a^{∗} + 1
≤ a^{∗},

so, by the induction rule, μz(az + 2) ≤ a^{∗}. It follows by (10) that

a^{∗} + a^{∗} = 2a^{∗}
= μz(az + 2)  (16)
≤ a^{∗}.

¿From (16) and the fixed-point inequation,

aa^{∗} + a^{∗} ≤ aa^{∗} + 1 + a^{∗}
≤ a^{∗} + a^{∗}
≤ a^{∗},

hence by the induction rule,

a^{∗}a^{∗} = μz(az + a^{∗})
≤ a^{∗}.  (17)

¿From (17) and the assumption, we get

a^{∗}a^{∗} + 1 ≤ a^{∗} + 1
≤ a^{∗},

so again by induction,

a^{∗∗} = μz(a^{∗}z + 1)
≤ a^{∗}.

For the converse inequations, note that

2 = 1 + 1
≤ a^{∗} + 1
≤ a^{∗},

so by monotonicity,

a^{∗} + a^{∗} = 2a^{∗}
≤ a^{∗}a^{∗}.

The remaining inequation a^{∗}a^{∗} ≤ a^{∗∗} follows from (14). □

Remark 3.9 An element x of an ordered semiring is reflexive if 1 ≤ x and transitive if xx ≤ x. In an ordered semiring which is a Park μ-semiring, we call x^{⊙} := μz(1 + zz + x) the reflexive transitive closure of x. We remark without proof that in an algebraically complete semiring, x^{∗} ≤ x^{⊙} and

x^{⊙} ≤ x^{∗} ⟺ x^{∗} + x^{∗} ≤ x^{∗}.

In particular, when + is idempotent as in R_{M} or L_{A}, then iteration x^{∗} coincides with reflexive transitive closure x^{⊙}, see also [21, 23, 4, 8]. By Propositions 3.7 and 3.8, we have x^{∗} = x^{⊙} for every reflexive element of an algebraically complete semiring.

Corollary 3.10 In any algebraically complete semiring, if 1 ≤ a then (a + 1)^{∗} = a^{∗}.

Proof. By (14), a+1 ≤ a^{∗}, hence by monotonicity and (15), a^{∗} ≤ (a+1)^{∗} ≤ (a^{∗})^{∗} = a^{∗}. □

Proposition 3.11 In any algebraically complete semiring, we have for n ∈ ℕ

0^{∗} = 1 and (n + 1)^{∗} = 1^{∗}.  (18)

Proof. Clearly,

0^{∗} = μx(0x + 1) = μx.1 = 1.

The second claim is clear for n = 0. If 1 ≤ n, then (n+1)^{∗} = n^{∗} by Corollary 3.10, and by induction hypothesis, n^{∗} = 1^{∗}. □

A morphism between μ-semirings is any function that commutes with the term functions. Thus, if h : A → B is a morphism between μ-semirings, its pointwise extension h^{X} : A^{X} → B^{X} satisfies t_{B} ^{∘} h^{X} = h ^{∘} t_{A} for all terms t. A morphism of Park μ-semirings, Conway μ-semirings and algebraically complete semirings is just a μ-semiring morphism. A μ-semiring A is initial in a class of μ-semirings if for every B in the class there is a unique morphism h : A → B.

Since 1^{∗} = ∞ in ℕ_{∞} by Proposition 3.8, any element of ℕ_{∞} can be considered as a closed term c. For algebraically complete semirings, the following converse also holds:

Theorem 3.12 If t is a closed term, then for some c ∈ ℕ_{∞}, equation t = c holds in all algebraically complete semirings.

The proof is deferred to section 7. An immediate consequence is:

Corollary 3.13 ℕ_{∞} is initial in the class of all algebraically complete semirings.

We remark that the symmetric inductive ^{∗}-semirings of [11] are right- and left-linear variants of algebraically complete semirings. An inductive ^{∗}- semiring is an ordered semiring equipped with a ^{∗}-operation, satisfying the inequation

xx^{∗} + 1 ≤ x^{∗}

and the following instance of the Park induction rule:

xz + y ≤ z → x^{∗}y ≤ z.  (19)

A symmetric inductive ^{∗}-semiring also satisfies

zx + y ≤ z → yx^{∗} ≤ z.  (20)

It follows that any inductive ^{∗}-semiring satisfies x^{∗}x + 1 = x^{∗} and has a monotone *-operation.

Note that (19) and (20) are instances of the pre-fixed-point axiom t[z/v] ≤ z → μv.t ≤ z for the terms t = xv + y and t = vx + y which are rightrespectively left-linear in the recursion variable v, and xx^{∗} + 1 ≤ x^{∗} resp. x^{∗}x + 1 ≤ x^{∗} are instances of the corresponding pre-fixed-point inequations t[μv.t/v] ≤ μv.t.

A Kozen semiring, called Kleene algebra in [16], is an idempotent symmetric inductive ^{∗}-semiring. Note that Propositions 3.7, 3.8 and 3.11 hold in all inductive ^{∗}-semirings. Via (13), any idempotent algebraically complete semiring is a Kozen semiring.

4 Algebraic Conway semirings

Next we turn to equational notions derived from algebraically complete semirings.

Definition 4.1 An algebraic Conway semiring is a Conway μ-semiring which satisfies (10), (11) and (12). A morphism of algebraic Conway semirings is a μ-semiring morphism.

Thus, any algebraically complete semiring is an algebraic Conway semiring.

In [6], a Conway semiring is defined to be a semiring S equipped with an operation ^{∗} : S → S subject to the equations

(x + y)^{∗} = (x^{∗}y)^{∗}x^{∗}
(xy)^{∗} = 1 + x(yx)^{∗}y.

It is known that also (x + y)^{∗} = x^{∗}(yx^{∗})^{∗} holds in any Conway semiring. By the following Proposition, any algebraic Conway semiring is a Conway semiring (using x^{r} = x^{ℓ} for x^{∗}).

Proposition 4.2 For any terms t and s and variable z which does not occur in t and s, the following equations hold in any algebraic Conway semiring:

μz(tz + s) = t^{∗}s  (21)
μz(zt + s) = st^{∗}  (22)
tt^{∗} + 1 = t^{∗}  (23)
t^{∗}t + 1 = t^{∗}  (24)
(t + s)^{∗} = (t^{∗}s)^{∗}t^{∗}  (25)
(t + s)^{∗} = t^{∗}(st^{∗})^{∗}  (26)
(ts)^{∗} = 1 + t(st)^{∗}s.  (27)

Proof. Equations (21) and (22) are (10) and (11), using (12) to identify t^{ℓ} = t^{∗} = t^{r}. Equations (23) and (24) are instances xx^{r} + 1 = x^{r} and x^{ℓ}x + 1 = x^{ℓ} of the fixed-point identity, which holds in any Conway μsemiring. For equation (25), we apply the diagonal identity

μz.t[z/v] = μz.μv.t

to the term t(x, y, z, v) := xv + yz + 1 and use equations (10) as follows:

(x + y)^{r} = μz((x + y)z + 1)
= μz.t[z/v]
= μz.μv(xv + yz + 1)
= μz(x^{r}(yz + 1))
= μz((x^{r}y)z + x^{r})
= (x^{r}y)^{r}x^{r}.

Similarly, for equation (26) we obtain (x + y)^{ℓ} = x^{ℓ}(yx^{ℓ})^{ℓ} from (11). As for equation (27), note that in the proof of Proposition 3.2, we have already derived (xy)^{r} = x(yx)^{r}y + 1 from the composition identity and (10) only. □

Equations (21) and (22) can be generalized to the following ones, of which (29) will later be used to eliminate left- or head-recursion to obtain Greibach-Normal-Form.

Proposition 4.3 For any terms t and s which may have free occurrences of the variable z, the following equations hold in any algebraic Conway semiring:

μz(tz + s) = μz(t^{∗}s)  (28)
μz(zt + s) = μz(st^{∗}).  (29)

Proof. By the diagonal identity, with a variable x not free in z, s, t we have

μz(zt + s) = μz(μx(xt + s))
= μz(st^{ℓ}),

which is (29). Likewise, we get (28). □

Conway semirings may be seen as left- and right-linear versions of algebraic Conway semirings, in the sense that they satisfy the composition identity

μz.t[s/z] = t[μz.s[t/z]/z]

for the terms t = xz + 1 and s = yz which are right-linear in z (resp. t = zx + 1 and s = zy which are left-linear in z), and the diagonal identity

μz.t[z/v] = μz.μv.t

for the term t = xv + yz + 1 which is right-linear in v and z (resp. t = vx + zy + 1 which is left-linear in v and z). The basic fact which connects Conway semirings and inductive ^{∗}-semirings is:

Proposition 4.4 [11] Every inductive ^{∗}-semiring is a Conway semiring.

5 Term vectors and term matrices

Suppose that t_{i} is a term for each i ∈ {1, …, n}, n ≥ 1. We write t⃗ for the term vector (t_{1}, …, t_{n}). When x⃗ = (x_{1}, …, x_{n}) is a vector of different variables, we define the term vector μx⃗.t⃗ by induction on n:

• If n = 1, then μx⃗.t⃗ := (μx_{1}.t_{1}).

• If n = m + 1 with m > 0 and y⃗ = (x_{1}, …, x_{m}), z⃗ = (x_{n}), r⃗ = (t_{1}, …, t_{m}), s⃗ = (t_{n}) put

μx⃗.t⃗ := (μy⃗.r⃗[μz⃗.s⃗/z⃗], μz⃗.s⃗[μy⃗.r⃗/y⃗]).

This definition is motivated by the Bekić–De Bakker–Scott rule [3, 2]. If t⃗ = (t_{1}, …, t_{n}) and t⃗′ = (t′_{1}, …, t′_{n}) are two term vectors of dimension n ≥ 1, we say that the equation t⃗ = t⃗′ holds in a μ-semiring A if each equation t_{i} = t′_{i} does. Similarly for t⃗ ≤ t⃗′. We say that an implication t⃗ = t⃗′ → s⃗ = s⃗′ holds in A, if each implication t_{1} = t′_{1} ∧ … ∧ t_{n} = t′_{n} → s_{j} = s′_{j} holds in A, for each j. We say x⃗ ∉ free(t⃗) if no x_{i} occurs free in any t_{j}.

Proposition 5.1 Let t⃗ be a term-vector and x⃗ a vector of variables of the same size, such that x⃗ ∉ free(t⃗). Then t⃗ = μx⃗.t⃗ holds in any Conway μsemiring.

Proof. By induction on the length of t⃗, using the fixed-point equation for length 1. □

Proposition 5.2 Let t⃗, s⃗ and x⃗, y⃗ be vectors of terms and variables of the same size, such that x⃗ and y⃗ are distinct and x⃗ ∉ free(s⃗). Then

(μx⃗.t⃗)[s⃗/y⃗] = μx⃗.t⃗[s⃗/y⃗]  (30)

holds in any Conway μ-semiring.

Proof. By induction on the size of t⃗, using the definition of substitution in the base case. □

The following facts are proven in [6] in the more general context of Conway theories (Conway algebras). See Chapter 6, Section 2. Propositions 5.1 and 5.2 show the ‘left zero identity’ and the ‘parameter identity’ of [6], while the above definition of μx⃗.t⃗ is the ‘scalar symmetric pairing identity’ of [6].

By Theorem 6.2.20 of [6], a variation of this definition, the ‘(left) pairing identity’, together with the parameter identity and the unary composition and diagonal identities, gives a Conway theory. By Corollary 6.2.4, in a Conway theory the ‘symmetric paring identity’ (31) holds, a generalized form of the Bekić-De Bakker-Scott equations. Therefore, it does not matter which of the definitions of μx⃗.t⃗ is used.

Theorem 5.3 ([6], Corollary 6.2.4, 5.3.13) Suppose that A is a Conway μsemiring. Then for each term vector t⃗ and vector x⃗ of different variables as above, the equation

μx⃗.t⃗ = (μy⃗.r⃗[μz⃗.s⃗/z⃗], μz⃗.s⃗[μy⃗.r⃗/y⃗])  (31)

holds in A for each way of splitting x⃗ and t⃗ into two parts as x⃗ = (y⃗, z⃗) and t⃗ = (r⃗, s⃗) such that the dimension of y⃗ agrees with the dimension of r⃗.

Theorem 5.4 ([6], Corollary 6.2.4) The vector version of the composition identity holds in any Conway μ-semiring: For all term vectors t⃗(y⃗, z⃗), s⃗(x⃗, z⃗) and variable vectors x⃗, y⃗ of appropriate sizes, any Conway μ-semiring satisfies

μx⃗.t⃗[s⃗/y⃗] = t⃗[μy⃗.s⃗[t⃗/x⃗]/y⃗].  (32)

The vector version of the diagonal identity holds in any Conway μ-semiring: for each term vector t⃗(x⃗, y⃗, z⃗) with distinct x⃗, y⃗, z⃗ such that the dimensions of t⃗, x⃗, y⃗ agree, any Conway μ-semiring satisfies

μx⃗.μy⃗.t⃗ = μx⃗.t⃗[x⃗/y⃗].  (33)

In particular, any Conway μ-semiring satisfies the vector version of the fixed-point equation,

μx⃗.t⃗ = t⃗[μx⃗.t⃗/x⃗].  (34)

Moreover, writing μx⃗.t⃗ = (r_{1}, …, r_{n}), the permutation identity

μ(x_{1π}, …, x_{nπ}).(t_{1π}, …, t_{nπ}) = (r_{1π}, …, r_{nπ})

holds in all Conway μ-semirings, for all permutations π : {1, …, n} → {1, …, n}.

Proposition 5.5 Suppose that t⃗ and r⃗ are term vectors of dimension m, n, respectively. Moreover, suppose that the components of the vectors of variables x⃗, y⃗ of dimension m and n, respectively, are pairwise distinct. Then

μ(x⃗, y⃗).(t⃗, r⃗) = μ(x⃗, y⃗).(t⃗[r⃗/y⃗], r⃗)  (35)

holds in any Conway μ-semiring.

The following fact is essentially due to Bekić [3] and de Bakker and Scott [2]. See also [10].

Theorem 5.6 The following vector version of the Park induction rule holds in all Park μ-semirings:

t⃗[y⃗/x⃗] ≤ y⃗ → μx⃗.t⃗ ≤ y⃗,

for all vectors t⃗ of terms and x⃗, y⃗ of variables of the same size.

In addition to term vectors, we will also consider matrices whose entries are terms. A term matrix T = (t_{i,j}) of size n × m, where n, m ≥ 1, consists of a term vector t⃗ of length nm, listing the entries of T by rows, and the dimension (n, m).

We denote by 1_{n} the n × n matrix whose diagonal entries are 1 and whose other entries are 0, and by 0_{n,m} the n × m matrix whose entries are all 0. When S and T are term matrices of appropriate size, we define S + T and ST in the obvious way. Suppose that T is a term matrix and X is a variable matrix of the same size n × m, with pairwise distinct variables, and let t⃗ and x⃗ be obtained by listing their entries by rows. Then μX.T is the n × m term matrix that corresponds to the term vector μx⃗.t⃗.

For square matrices T, we can define the left- and right iterations T^{ℓ} and T^{r}, using μ. Independently of μ, we now define a matrix T^{∗} by induction on the dimension of T and then relate T^{∗} to T^{ℓ} and T^{r}.

Definition 5.7 For an n × n term matrix T, define a matrix T^{∗} by induction on n:

1. If n = 1, then T = ( t) for some term t. We define T^{∗} := ( t^{∗}).

2. If n = m + 1 > 1 and

T = ( \begin{matrix}R & S \\ U & V \end{matrix} )  (36)

where R is m × m and V is 1 × 1, we define

T^{∗} := ( \begin{matrix}\overline{R} & \overline{S} \\ \overline{U} & \overline{V} \end{matrix} )  (37)

where

\begin{aligned}\overline{R} & = & (R + SV^{∗}U)^{∗} & \overline{S} & = & \overline{R}SV^{∗} \\ \overline{U} & = & \overline{V} UR^{∗} & \overline{V} & = & (V + UR^{∗}S)^{∗}. \end{aligned}

Suppose that T = ( t_{ij} ) and S = ( s_{ij} ) are term matrices of the same size. We say that T = S holds in a μ-semiring A if each equation t_{ij} = s_{ij} holds in A.

The following result is proven in [6] using a different framework, cf. Chapter 9, Theorem 2.1.

Theorem 5.8 Let A be an algebraic Conway semiring. Suppose that T is an n × n term matrix, S is an n × m (resp. m × n) term matrix and let X denote an n × m (resp. m × n) matrix of new variables. Then the equations

μX(T X + S) = T^{∗}S  (38)
μX(XT + S) = ST^{∗}  (39)

hold in A. Moreover, (37) holds, if T splits like (36) for matrices R, U, V of appropriate dimensions.

In particular, the coincidence of left- and right iterations for square matrices holds in A,

T^{ℓ} := μX(XT + 1_{n}) = T^{∗} = μX(T X + 1_{n}) =: T^{r}.  (40)

The next results parallel with the fact that if A is a continuous semiring, then so is any matrix semiring Mat_{n×n}(A), for each n ≥ 1.

Lemma 5.9 Let A be a μ-semiring. For all vectors t⃗, t⃗′ of terms and x⃗ of variables of the same dimension, if t⃗_{A} = t⃗′_{A}, then (μx⃗.t⃗)_{A} = (μx⃗.t′)_{A}.

Proof. By induction on the dimension n of x⃗. For n = 1, the claim is true since A is a μ-semiring. For n > 1, consider a vector (x⃗, x) of distinct variables and term-vectors (t⃗, t) and (s⃗, s) of the same size. By the definition of μ(x⃗, x).(t⃗, t) and μ(x⃗, x).(s⃗, s), we have to show that (μx⃗.t⃗[μx.t/x])_{A} = (μx⃗.s⃗[μx.s/x])_{A} and (μx.t[μx⃗.t⃗/x⃗])_{A} = (μx.s[μx⃗.s⃗/x⃗])_{A}. But by induction, (μx.t)_{A} = (μx.s)_{A} and (μx⃗.t⃗)_{A} = (μx⃗.s⃗)_{A}, so for each ρ ∈ A^{X}

(μx⃗.t⃗[μx.t/x])_{A}(ρ) = (μx⃗.t⃗)_{A}(ρ[x ↦ (μx.t)_{A}(ρ)])
= (μx⃗.s⃗)_{A}(ρ[x ↦ (μx.s)_{A}(ρ)])
= (μx⃗.s⃗[μx.s/x])_{A}(ρ).

Hence (μx⃗.t⃗[μx.t/x])_{A} = (μx⃗.s⃗[μx.s/x])_{A}. The proof for (μx.t[μx⃗.t⃗/x⃗])_{A} = (μx.s[μx⃗.s⃗/x⃗])_{A} is symmetric. □

Corollary 5.10 If A is a μ-semiring, so is Mat_{n×n}(A), for each n ≥ 1.

Proof. For each term t we define a term matrix t′ of size n × n inductively, using the addition and multiplication of matrices and different new variables x_{i,j} in the first case:

\begin{aligned}x′ & := & (x_{i,j}), \\ 0′ & := & 0_{n,n}, \\ 1′ & := & 1_{n}, \end{aligned}  \begin{aligned}(t_{1} + t_{2})′ & := & t′_{1} + t′_{2}, \\ (t_{1} · t_{2})′ & := & t′_{1} · t′_{2}, \\ (μx.t)′ & := & μx′.t′. \end{aligned}

Let M := Mat_{n×n}(A). Note that each ρ : X → M is obtained from some ρ̂ : X → A such that ρ(x) = (ρ̂(x_{i,j})) when x′ = (x_{i,j}). To define the interpretation t_{M} : M^{X} → M, we put

t_{M}(ρ) := t′_{A}(ρ̂).  (41)

To see that M is a μ-semiring, we check the conditions 1. – 3. of Definition 2.1. Let s, t be terms, x ∈ X and ρ : X → M.

1. By definition, x_{M}(ρ) = x′_{A}(ρ̂) = (ρ̂(x_{i,j})) = ρ(x). Likewise, 0_{M}(ρ) = 0′_{A}(ρ̂) = 0_{n,n} and (s+t)_{M}(ρ) = (s′+t′)_{A}(ρ̂) = s′_{A}(ρ̂)+t′_{A}(ρ̂) = s_{M}(ρ)+t_{M}(ρ), and similarly for 1 and (s · t).

2. We need to show

(t[s/x])_{M}(ρ) = (t[s/x])′_{A}(ρ̂) = t′_{A}({ \atop ρ[x ↦ s_{M}(ρ)]}) = t_{M}(ρ[x ↦ s_{M}(ρ)]).

By induction on t, one first shows that (t[s/x])′ = t′[s′/x′], where substitution for matrices of variables is done componentwise. This is clear when t is atomic, and immediate by induction when t is (t_{1} + t_{2}) or (t_{1} · t_{2}). If t is μx.r, then

(t[s/x])′ = (μx.r)′ = μx′.r′ = (μx′.r′)[s′/x′] = t′[s′/x′].

If t is μz.r where z ≢ x then, assuming z is not free in s, (μz.r)[s/x] = μz.r[s/x] and hence

(t[s/x])′ = (μz.r[s/x])′ = μz′(r[s/x])′ = μz′.r′[s′/x′] = (μz′.r′)[s′/x′] = t′[s′/x′]

by induction and using (30). Moreover,

t′_{A}({ \atop ρ[x ↦ s_{M}(ρ)]}) = t′_{A}(ρ̂[x′ ↦ s′_{A}(ρ̂)]) = (t′[s′/x′])_{A}(ρ̂).

3. Assume t_{M} = s_{M}. Then t′_{A} = s′_{A}, thus (μx′.t′)_{A} = (μx′.s′)_{A}. So for all ρ,

(μx.t)_{M}(ρ) = (μx′.t′)_{A}(ρ̂) = (μx′.s′)_{A}(ρ̂) = (μx.s)_{M}(ρ).

Hence (μx.t)_{M} = (μx.s)_{M}. □

Theorem 5.11 If A is an algebraic Conway semiring, then so is Mat_{n×n}(A), for each n ≥ 1.

Proof. Let M := Mat_{n×n}(A). By Corollary 5.10, M is a μ-semiring. By Theorem 5.4 it follows that M satisfies the Conway identities (3) and (4). By (38) – (40), M satisfies (10), (11) and (12). □

Corollary 5.12 Let A be an algebraic Conway semiring. For all term matrices S, T of appropriate size, the following equations hold in A:

T T^{∗} + 1_{n} = T^{∗}  (42)
T^{∗}T + 1_{n} = T^{∗}  (43)
(T + S)^{∗} = (T^{∗}S)^{∗}T^{∗}  (44)
(T + S)^{∗} = T^{∗}(ST^{∗})^{∗}  (45)
(T S)^{∗} = 1_{n} + T (ST)^{∗}S.  (46)

For an n × n matrix X of distinct variables and any n × n term matrices T and S, which may contain variables of X, the following equations hold in A:

μX(T X + S) = μX(T^{∗}S)  (47)
μX(XT + S) = μX(ST^{∗}).  (48)

Proof. By Theorem 5.11, Proposition 4.2 and Proposition 4.3. □

The equations (47) and (48) also hold when X is of size m × n and T and S have appropriate sizes. Indeed, with an m × n matrix Y of new variables, by (33) and (38) we get

μX(T X + S) = μXμY (T Y + S) = μX(T^{∗}S),

and similarly for (48).

Theorem 5.13 If A is a Park μ-semiring, or an algebraically complete semiring, so is Mat_{n×n}(A), for each n ≥ 1.

Proof. By Theorem 5.6, the vector version of the Park induction rule holds in A. □

6 Normal forms

In this section we present a Greibach normal form theorem applicable to all algebraically complete semirings. We also show that analogs of elimination of chain rules and deletion rules in context-free grammars hold in algebraically complete semirings, although we can prove the latter only when + is idempotent.

Let K be the set of terms {0, 1, …}∪{1^{∗}}, which, by Theorem 3.12, amount to all closed terms over algebraically complete semirings.

Proposition 6.1 For k ∈ K, the equation kx = xk holds in all algebraic Conway semirings.

Proof. This is obvious when k ≠ 1^{∗}. Moreover, we have

1^{r} · x = μz(1 · z + x)
= μz(z · 1 + x)
= x · 1^{ℓ}

in any algebraic Conway semiring, and 1^{∗} = 1^{r} = 1^{ℓ}. □

A monomial is a term of the form ku, where k ∈ K and u is a product of variables. When u is the empty product, the monomial ku is called constant. The leading factor of a monomial ku, where u = x_{1} ⋯ x_{n} is a nonempty product of variables, is the variable x_{1}. A polynomial is any finite sum of monomials. A finite polynomial is a polynomial which is also a finite term, i.e. a polynomial whose constants and leading factors belong to ℕ. In particular, 0 is a finite polynomial.

With respect to the semiring equations, any finite term is equivalent to a finite polynomial. The following normal form theorem is quite standard.

Theorem 6.2 (See, e.g., [6]) In algebraic Conway semirings, any μ-term is equivalent to the first component of a term vector of the form

μ(x_{1}, …, x_{n}).(p_{1}, …, p_{n}),

where each p_{i} is a finite polynomial.

Definition 6.3 A term vector μx⃗.t⃗, where t⃗ = (t_{1}(x⃗, y⃗), …, t_{n}(x⃗, y⃗)), is a context-free grammar if each t_{i} is a polynomial. The context-free grammar μx⃗.t⃗(x⃗, y⃗) has no chain rules, if no t_{i} has a monomial of the form kx where k ∈ K \ {0} and x is among the variables x⃗; it has no ϵ-rules if no t_{j} has a monomial of the form k where k ∈ K \ {0}.

A context-free grammar μx⃗.t⃗ is in Greibach normal form if each t_{i} is a polynomial which is a sum of non-constant monomials whose leading factors are among the parameters y_{1}, …, y_{m}.

The next theorem is a first version of Greibach’s normal form theorem. The algorithm in the proof is due to Rosenkrantz [25] (cf. [13], Algorithm 4.9.1). We use properties of least pre-fixed-points rather than power series to prove its correctness, and thus show that it is applicable to any algebraic Conway semiring.

If μx⃗.t⃗ has dimension n and m ≤ n, we denote by (μx⃗.t⃗)_{[m]} the vector whose components are the first m components of μx⃗.t⃗. We simply write (μx⃗.t⃗)_{1} for (μx⃗.t⃗)_{[1]}.

Theorem 6.4 Let x⃗ = (x_{1}, …, x_{m}) and z⃗ = (z_{1}, …, z_{p}) be different variables, and suppose that μx⃗.t⃗(x⃗, z⃗) is a context-free grammar that has no chain-rules and no ϵ-rules. Then there is a context-free grammar

μ(x_{1}, …, x_{n}).(s_{1}, …, s_{n})(x_{1}, …, x_{n}, z_{1}, …, z_{p})

in Greibach normal form, such that m ≤ n ≤ m + m^{2} and the equation

μx⃗.t⃗ = (μ(x_{1}, …, x_{n}).(s_{1}, …, s_{n}))_{[m]}

holds in any algebraic Conway semiring.

Proof. By distributivity, we can write

t_{j}(x⃗, z⃗) = ∑_{k=1}^{m}(x_{k} · t_{kj}(x⃗, z⃗)) + r_{j}(x⃗, z⃗),

where r_{j} is 0 or a sum of non-constant monomials whose leading factors are parameters; constant monomials ≠ 0 do not occur since μx⃗.t⃗ has no ϵ-rules. So we can write μx⃗.t⃗ as

μx⃗(x⃗ · T (x⃗, z⃗) + r⃗(x⃗, z⃗)),

using

T = ( \begin{matrix}t_{11} & … & t_{1m} \\ ⋮ & ... & ⋮ \\ t_{m1} & … & t_{mm} \end{matrix} ) and r⃗ = (r_{1}, …, r_{m}).

With an m × m matrix Y = ( y_{ij} ) of new variables, consider the term

μ(x⃗, Y).(r⃗Y + r⃗, T Y + T).  (49)

Claim The equation

μx⃗.t⃗ = (μ(x⃗, Y).(r⃗Y + r⃗, T Y + T))_{[m]}

holds in all algebraic Conway semirings.

Indeed, by Corollary 5.12, equation (48),

μx⃗.t⃗ = μx⃗(x⃗T + r⃗)
= μx⃗(r⃗T^{∗}).

On the other hand, by Theorem 5.3, equation (31), and Theorem 5.8, equation (38) and Corollary 5.12, equation (42), we have that

(μ(x⃗, Y).(r⃗Y + r⃗, T Y + T))_{[m]} = μx⃗(r⃗T^{∗}T + r⃗)
= μx⃗(r⃗(T^{∗}T + 1_{m}))
= μx⃗(r⃗T^{∗}).

It remains to be shown that (49) contains no essential left recursion. First, each component of r⃗Y + r⃗ is of the form

(r⃗Y)_{j} + r_{j} = ∑_{k=1}^{m}(r_{k} · y_{kj}) + r_{j},

which is 0 or can be written as a sum of non-constant monomials whose leading factors are parameters. Second, each component of the term T Y +T is of the form

∑_{k=1}^{m} t_{ik} · y_{kj} + t_{ij}.  (50)

By Proposition 5.5 leading factors x_{u} in summands of t_{ik} and t_{ij} can be replaced by (r⃗Y)_{u} + r_{u}. Since μx⃗.t⃗ has no chain-rules, none of the t_{ik} or t_{ij} is a constant k ∈ K \ {0}, so y_{kj} is not a leading factor of t_{ik} · y_{kj} and no monomial in the new polynomials is a constant ≠ 0. □

Example 6.5 Let G be the context-free grammar

\begin{aligned}A & = & BC & + & a \\ B & = & Ab & + & CA \\ C & = & AB & + & CC \end{aligned}

over the alphabet {a, b}. In matrix notation, this is

(A, B, C) = (A, B, C) · T + (a, 0, 0)  where T = ( \begin{matrix}0 & b & B \\ C & 0 & 0 \\ 0 & A & C \end{matrix} ) . (51)

By the proof, the least solution of (51) is the same as the least solution of the (essentially) right-recursive system

\begin{aligned}(A, B, C) & = & (a, 0, 0) · Y + (a, 0, 0) \\ Y & = & T · Y + T \end{aligned} where Y = ( \begin{matrix}Y_{1,1} & Y_{1,2} & Y_{1,3} \\ Y_{2,1} & Y_{2,2} & Y_{2,3} \\ Y_{3,1} & Y_{3,2} & Y_{3,3} \end{matrix} ) . (52)

Multiplying out gives

\begin{aligned}A & = & aY_{1,1} + a \\ B & = & aY_{1,2} \\ C & = & aY_{1,3} \\ Y_{2,1} & = & CY_{1,1} + C \\ Y_{2,2} & = & CY_{1,2} \\ Y_{2,3} & = & CY_{1,3} \end{aligned}  \begin{aligned}Y_{1,1} & = & bY_{2,1} + BY_{3,1} \\ Y_{1,2} & = & bY_{2,2} + BY_{3,2} + b \\ Y_{1,3} & = & bY_{2,3} + BY_{3,3} + B \\ Y_{3,1} & = & AY_{2,1} + CY_{3,1} \\ Y_{3,2} & = & AY_{2,2} + CY_{3,2} + A \\ Y_{3,3} & = & AY_{2,3} + CY_{3,3} + C \end{aligned}

Plugging in the right hand sides for A, B, C in the Y -equations gives 28 rules in GNF. Standard textbooks like Hopcroft and Ullman [14] give an exponential algorithm, producing 119 rules for this example.

For algebraically complete semirings, we obtain a slightly more general version of the Greibach normal form theorem, based on the following

Lemma 6.6 (Elimination of chain rules) For every context-free grammar μx⃗.t⃗(x⃗, z⃗) there is a context-free grammar μx⃗.s⃗ that has no chain rules, such that

μx⃗.t⃗ = μx⃗.s⃗

holds in all algebraically complete semirings. If μx⃗.t⃗ has no ϵ-rules, then μx⃗.s⃗ has no ϵ-rules.

Proof. By distributivity, we can write

t_{j}(x⃗, z⃗) = ∑_{i=1}^{m} x_{i}k_{ij} + r_{j}(x⃗, z⃗)

where k_{ij} ∈ K and the polynomials r_{j} have no monomials of the form kx, with k ∈ K \ {0} and x is one of the variables x⃗. Let E = ( k_{ij} ). By (48),

μx⃗.t⃗ = μx⃗(x⃗E + r⃗)
= μx⃗(r⃗E^{∗}).

By Proposition 3.8 and the definition of E^{∗}, we obtain that E^{∗} has entries in K only, so the terms s⃗ := r⃗E^{∗} are polynomials. By the choice of r⃗, the polynomials s⃗ have no monomials of the form kx with k ∈ K \ {0} and x a variable from x⃗. If the polynomials t⃗ have no monomials k with k ∈ K \{0}, then those of r⃗ and hence those of r⃗E^{∗} have no such monomials. □

Corollary 6.7 For each context-free grammar μx⃗.t⃗(x⃗, z⃗) that has no ϵrules, there is a context-free grammar μ(x⃗, y⃗).s⃗(x⃗, y⃗, z⃗) in Greibach normal form such that

μx⃗.t⃗ = (μ(x⃗, y⃗).s⃗)_{[m]}

holds in all algebraically complete semirings, where x⃗ = (x_{1}, …, x_{m}).

Proof. By Lemma 6.6, we may assume that μx⃗.t⃗ has no chain-rules and no ϵ-rules. Hence, we can apply Theorem 6.4. □

Finally, we give a version of the Greibach normal form theorem that applies to all context-free grammars. Additional effort is needed to get rid of ϵ-rules:

Lemma 6.8 (Elimination of ϵ-rules) Let t⃗(x⃗, z⃗) be a vector of m polynomials in x⃗ = (x_{1}, …, x_{m}) with parameters z⃗. There are constants k⃗ ∈ K^{m} and polynomials s⃗(x⃗, z⃗) without non-zero constant monomials such that

1. in all algebraically complete semirings S,

μx⃗.t⃗ ≤ k⃗ + μx⃗.s⃗,  (53)

2. in all continuous semirings and all idempotent algebraically complete semirings S,

μx⃗.t⃗ ≥ k⃗ + μx⃗.s⃗.  (54)

Proof. We will simplify the notation by suppressing the parameters z⃗.

Claim 1: There is k⃗ ∈ K^{m} and a vector s⃗(x⃗) of m polynomials such that (i) k⃗ ≤ μ⃗x⃗.t⃗ holds in all algebraically complete semirings S,

(ii) the polynomials s⃗(x⃗) have no constant monomials ≠ 0, and

(iii) t⃗[x⃗ + k⃗/x⃗] = s⃗(x⃗) + k⃗ with respect to the semiring equations.

Proof. First, we determine k⃗ from t⃗. Call a monomial m(x⃗) pure if it has no parameters and is not a constant. Using the semiring equations, we can write t⃗ in the form

t⃗(x⃗) = q⃗(x⃗) + p⃗(x⃗) + c⃗  (55)

where, in the i-th component, p_{i}(x⃗) is 0 or the sum of the pure monomials of t_{i}(x⃗) and c_{i} is 0 or the sum of the constant monomials of t_{i}(x⃗). Put

k⃗ := μx⃗(p⃗(x⃗) + c⃗),

and note that k⃗ ∈ K^{m} = ℕ_{∞}^{m} by Theorem 3.12. ¿From 0 ≤ q⃗(x⃗) and monotonicity, we obtain that k⃗ ≤ μx⃗.t⃗ holds in all algebraically complete semirings S, showing (i).

By the semiring equations, the polynomials t⃗[x⃗ + k⃗/x⃗] can be written as

t⃗[x⃗ + k⃗/x⃗] = s⃗(x⃗) + d⃗,

where, by Proposition 3.8, d⃗ ∈ K^{m} and the polynomials s⃗(x⃗) contain no non-zero constant monomials. Part (ii) is clear by the choice of s⃗(x⃗). For (iii), note that d⃗ is the sum of the constant monomials of

t⃗[x⃗ + k⃗/x⃗] = q⃗[x⃗ + k⃗/x⃗] + p⃗[x⃗ + k⃗/x⃗] + c⃗,

so d⃗ = p⃗[k⃗/x⃗]+c⃗. But in algebraically complete semirings, the vector version of the fixed-point equation holds, so k⃗ = p⃗[k⃗/x⃗] + c⃗ = d⃗.

Claim 2: For all algebraically complete semirings S and b⃗ ∈ S, if s⃗(b⃗) ≤ b⃗, then μx⃗.t⃗ ≤ b⃗ + k⃗.

Proof. ¿From Claim 1, (iii), and the assumption on b⃗ we have

t⃗(b⃗ + k⃗) = s⃗(b⃗) + k⃗ ≤ b⃗ + k⃗,

which implies μx⃗.t⃗ ≤ b⃗ + k⃗ by fixed-point induction.

Claim 3: If S is a continuous semiring or an algebraically complete idempotent semiring and a⃗ ∈ S, then if t⃗(a⃗) ≤ a⃗, then k⃗ + μx⃗.s⃗ ≤ a⃗.

Proof. If S is continuous, for b⃗_{0} := 0 and b⃗_{n+1} := s⃗(b⃗_{n}) we have

μx⃗.s⃗ = ⨆_{n∈ℕ} b⃗_{n}.  (56)

Note that by the choice of k⃗ and Claim 1, (i), b⃗_{0} + k⃗ = k⃗ ≤ a⃗. Assuming b⃗_{n} + k⃗ ≤ a⃗, we obtain from the monotonicity of t⃗ and the choice of s⃗ that

b⃗_{n+1} + k⃗ = s⃗(b⃗_{n}) + k⃗
= t⃗(b⃗_{n} + k⃗)
≤ t⃗(a⃗)
≤ a⃗.

Hence, by induction, (56) and continuity of +,

μx⃗.s⃗ + k⃗ = ⨆_{n∈ℕ} b⃗_{n} + k⃗ ≤ a⃗.

If S is algebraically complete and idempotent, then from 0 ≤ k⃗ ≤ μx⃗.t⃗ ≤ a⃗ we obtain

s⃗(a⃗) ≤ k⃗ + s⃗(a⃗)
= t⃗(a⃗ + k⃗)
≤ t⃗(a⃗ + a⃗)
= t⃗(a⃗)
≤ a⃗,

hence μx⃗.s⃗ ≤ a⃗. Using idempotency once more, we have k⃗ + μx⃗.s⃗ ≤ a⃗ + a⃗ = a⃗.

¿From Claims 1–3 we obtain μx⃗.t⃗ = k⃗ + μx⃗.s⃗ holds, completing the proof of Lemma 6.8. □

Example 6.9 Let t(x) = xx + c with c > 1. Splitting t into its non-pure, pure and constant monomials, we obtain

t(x, z) ≡ q(x, z) + p(x) + c

where q ≡ 0 and p ≡ xx. Therefore,

k := μx(p(x) + c) = 1^{∗}

and hence

t(x + k) ≡ (x + 1^{∗})^{2} ≡ x^{2} + 2x1^{∗} + (1^{∗})^{2} + c ≡ x^{2} + x1^{∗} + 1^{∗} + c ≡ s(x) + k

for s(x) := x^{2} + 1^{∗}x. Hence

μx.t = μx(xx + c) = 1^{∗},
μx.s = μx(xx + x1^{∗}) = 0,

and indeed k + μx.s = 1^{∗} + 0 = 1^{∗} = μx.t.

We don’t know if Lemma 6.8 holds for algebraically complete semirings in general, although some further cases are given in the appendix. Hence, of the version of Greibach’s normal form theorem involving elimination of ϵ-rules we only have:

Theorem 6.10 For each context-free grammar μx⃗.t⃗ of length m there is k⃗ ∈ K^{m} and a context-free grammar μx⃗.r⃗ in Greibach normal form such that μx⃗.t⃗ = k⃗ + (μx⃗.r⃗)_{[m]} holds in all continuous semirings and in all idempotent algebraically complete semirings.

Proof. By Lemma 6.8, there are k⃗ ∈ K^{m} and a context-free grammar μx⃗.s⃗ without ϵ-rules such that

μx⃗.t⃗ = k⃗ + μx⃗.s⃗

holds in all continuous semirings and in all idempotent algebraically complete semirings. By Lemma 6.6, we may assume that μx⃗.s⃗ does not have chain-rules. Hence, by Theorem 6.4, there is a context-free grammar μ(x⃗, y⃗).r⃗ such that

μx⃗.s⃗ = (μ(x⃗, y⃗).r⃗)_{[m]}

holds in all algebraic Conway semirings, hence in all algebraically complete semirings. □

For continuous semirings, the Greibach normal form theorem including ϵelimination also can be shown using formal power series, cf. [19].

Since the set of context-free languages over the alphabet A form an idempotent algebraically complete semiring, Theorem 6.10 implies the classical Greibach normal form theorem.

By Theorem 6.2, for every term t there are finite terms t⃗ such that t = (μx⃗.t⃗)_{1} holds in all algebraic Conway semirings. Therefore, we obtain:

Corollary 6.11 For each term t either t is closed and there is some k ∈ K such that t = k holds in all algebraically complete semirings, or t is not closed and there is a k ∈ K and a term μx⃗.s⃗ in Greibach normal form such that equation t = k + (μx⃗.s⃗)_{1} holds in all continuous semirings and in all idempotent algebraically complete semirings.

7 The initial algebraically complete semiring

Recall from section 3 that a morphism between μ-semirings or algebraically complete semirings is any function that commutes with the term functions. A morphism of continuous semirings is a semiring morphism which is a continuous function.

It is not difficult to prove that for any set A, the power series semiring ℕ_{∞}⟨⟨A^{∗}⟩⟩, equipped with the pointwise order is the free continuous semiring generated by A: For any continuous semiring S and function h : A → S, there is a unique morphism of continuous semirings ℕ_{∞}⟨⟨A^{∗}⟩⟩ → S extending h. (As usual, we identify each letter in A with the corresponding series.) In particular, ℕ_{∞} from Example 3.4 is the initial continuous semiring.

Recall that since ℕ_{∞} is a continuous semiring, it is also an algebraically complete semiring and a symmetric inductive ^{∗}-semiring. In [11], it has been shown:

Theorem 7.1 ℕ_{∞} is initial in the category of (symmetric) inductive ^{∗}- semirings.

In this section we prove Theorem 3.12 and its Corollary 3.13, which we recall as

Theorem 7.2 If t is a closed term, then for some c ∈ ℕ_{∞}, equation t = c holds in all algebraically complete semirings.

Corollary 7.3 ℕ_{∞} is initial in the class of all algebraically complete semirings.

Recall from Propositions 3.8 and 3.11 that in all algebraically complete semirings,

1^{∗} = 2^{∗} = … = n^{∗} = … = 1^{∗} + 1^{∗} = 1^{∗}1^{∗} = 1^{∗∗}.

By Theorem 6.2, any closed μ-term is equivalent to a term of the form μ(x_{1}, …, x_{n}).(p_{1}, …, p_{n}) where each p_{i} is a finite polynomial in x_{1}, …, x_{n}. We may assume that the words appearing in the monomials of a polynomial are pairwise different and each monomial has a nonzero coefficient.

Let p⃗ = (p_{1}, …, p_{n}) be a vector of finite polynomials, containing at most the variables x_{1}, …, x_{n}. We call an integer i ∈ [n] := {1, …, n} eventually nonzero in p⃗ if p_{i} has a nonzero constant monomial, or a monomial of the form cu with c ≠ 0 such that for each variable x_{j} appearing in u it holds that j is eventually nonzero in p⃗. If i is not eventually nonzero in p⃗, we call i eventually zero in p⃗.

The above definition is recursive. We may give an alternative inductive definition. Let C_{0} consist of those integers i ∈ [n] such that p_{i} contains a nonzero constant monomial. Given C_{m}, define C_{m+1} to be the union of C_{m} with the set of all i ∈ [n] such that p_{i} contains a monomial cu with c ≠ 0 such that j ∈ C_{m} holds for each variable x_{j} occurring in u. Then let C denote the union of the C_{m}. An integer i ∈ [n] is eventually nonzero in p⃗ iff i ∈ C.

Proposition 7.4 For the vector p⃗ as above and each i ∈ [n], equation

(μx⃗.p⃗)_{i} = 0  (57)

holds in all algebraically complete semirings iff i is eventually zero in p⃗.

Proof. Let i be eventually nonzero in p⃗, so that i ∈ C_{m}, for some m. We argue by induction on m to show that (μx⃗.p⃗)_{i} = 1 in the Boolean semiring 𝔹 = {0, 1}, which is algebraically complete. When m = 0, p_{i} contains a nonzero constant monomial c, so that by the fixed point equation,

(μx⃗.p⃗)_{i} ≥ c

holds in all algebraically complete semirings. In particular, (μx⃗.p⃗)_{i} = 1 in 𝔹. Suppose now that m > 0 and that our claim holds for all integers in C_{m−1}. Since i ∈ C_{m}, either i ∈ C_{m−1} in which case the result is immediate from the induction hypothesis, or p_{i} contains a monomial cu with c ≠ 0 such that j ∈ C_{m−1} holds for all variables x_{j} appearing in u. By induction, (μx⃗.p⃗)_{j} = 1 in 𝔹 for all such j, so that by the fixed point equation, (μx⃗.p⃗)_{i} evaluates in 𝔹 to an element greater than or equal to c times the product of the (μx⃗.p⃗)_{j}, for all occurrences of the variables x_{j} in u, i.e., (μx⃗.p⃗)_{i} = 1 holds in 𝔹 as claimed.

For the converse, suppose that i is eventually zero in p⃗. Then for each monomial cu of p_{i} with c ≠ 0 it holds that u contains at least one occurrence of a variable x_{j} with j eventually zero in p⃗. Thus, if in p_{i} we substitute 0 for all the variables that are eventually zero in p⃗, then we obtain 0 using just the semiring equations. In the rest of the argument, assume without loss of generality (by the permutation identity) that the eventually zero integers in [n] are the last n−m ones. Let A be an algebraically complete semiring and denote a⃗ = (a_{1}, …, a_{n}) = (μx⃗.p⃗)_{A}. We want to prove that the last n − m components of a⃗ are all 0. For each i ∈ [n], let q_{i} denote the polynomial which results from p_{i} by substituting 0 for all the x_{j} with j > m, and let b⃗ = (b_{1}, …, b_{n}) = (μx⃗.q⃗)_{A}. By the preceding observation,

b⃗ = (b_{1}, …, b_{m}, 0, …, 0)
= q⃗_{A}(b_{1}, …, b_{m}, 0, …, 0)
= p⃗_{A}(b_{1}, …, b_{m}, 0, …, 0),

since all the q_{j} with j > m are 0. But since A is algebraically complete,

a⃗ ≤ (b_{1}, …, b_{m}, 0, …, 0),

yielding that a_{j} = 0 for all j > m. □

Corollary 7.5 Equation (57) holds in all algebraic Conway semirings iff it holds in all continuous semirings iff it holds in ℕ_{∞} iff it holds in the boolean semiring 𝔹.

Let p⃗ = (p_{1}, …, p_{n}) be as above. For i, j ∈ [n], we say that i directly depends on j in p⃗ if the variable x_{j} occurs in some monomial cu of p_{i}, where c ≠ 0. We say that i depends on j if there is a chain of integers i_{0}, …, i_{k} in [n] such that i_{0} = i, i_{k} = j and each i_{m} directly depends on i_{m+1}.

We say that an integer i ∈ [n] is eventually finite in p⃗ if there is no infinite chain i = i_{0}, i_{1}, … of integers in [n] such that for each m, integer i_{m} directly depends on i_{m+1}. Alternatively, i is eventually finite in p⃗ if it belongs to one of the following sets F_{m}. The set F_{0} consists of all those j ∈ [n] such that p_{j} is constant, and F_{m+1} is the union of F_{m} with the set of all j ∈ [n] such that k ∈ F_{m} for all k ∈ [n] on which j directly depends.

If i ∈ [n] is eventually finite in p⃗, we define the value v_{i} of i as follows: if i ∈ F_{0}, the value v_{i} is the constant p_{i}. If i ∈ F_{m+1} − F_{m}, then p_{i} is a sum of monomials cx_{j_{1}} ⋯ x_{j_{k}} such that c ≠ 0 and j_{1}, …, j_{k} ∈ F_{m}; the value v_{i} is the corresponding sum of the cv_{j_{1}} ⋯ v_{j_{k}}.

Proposition 7.6 If i is eventually finite in p⃗, then v_{i} ∈ ℕ and

(μx⃗.p⃗)_{i} = v_{i}

holds in all algebraic Conway semirings.

Proof. This is based on the vector form of the fixed point identity that holds in all algebraic Conway semirings. The details are routine. □

Lemma 7.7 For every k ≥ 0,

μx.(x^{k})^{∗} = 1^{∗}  (58)

holds in any algebraically complete semiring.

Proof. This is clear when k = 0, since μx.1^{∗} = 1^{∗} by the fixed point identity. Suppose that k ≥ 1. Since (1^{∗})^{k} = 1^{∗} and 1^{∗∗} = 1^{∗} hold, it follows that ((1^{∗})^{k})^{∗} = 1^{∗}. Thus, by the least pre-fixed point rule, μx.(x^{k})^{∗} ≤ 1^{∗}. In order to prove the reverse inequation, suppose that S is an algebraically complete semiring. Let f denote the function S → S which maps any x ∈ S to (x^{k})^{∗}. Then f(0) = 1^{∗}, hence the least pre-fixed point of f is ≥ 1^{∗}. Thus, in all algebraically complete semirings, it holds that 1^{∗} ≤ μx.(x^{k})^{∗}. □

Lemma 7.8 For every k ≥ 1, the equation

μx(x^{k} + 1) = 1^{∗}  (59)

holds in any algebraically complete semiring.

Proof. Using (58) and the diagonal identity,

μx(x^{k} + 1) = μx.μy(x^{k−1}y + 1)
= μx.(x^{k−1})^{∗}
= 1^{∗}. □

Lemma 7.9 For every non-constant polynomial p = p(x) in the variable x, if the constant term of p is not zero (i.e., p(x) = q(x) + c for some q(x) and c ≠ 0), then

μx.p = 1^{∗}  (60)

holds in all algebraically complete semirings.

Proof. First, note that p(1^{∗}) = 1^{∗} holds in all algebraically complete semirings, so that μx.p ≤ 1^{∗}. We can write p(x) = x^{k} + 1 + q(x) for some polynomial q(x) and some k ≥ 1. Thus, x^{k} + 1 ≤ p(x) holds, and thus also μx(x^{k} + 1) ≤ μx.p. But μx(x^{k} + 1) = 1^{∗}. □

Lemma 7.10 For each μ-term t(x_{1}, …, x_{n}), either

t(0, …, 0) = 0

holds in all algebraically complete semirings, or

t(0, …, 0) ≥ 1

holds in all algebraically complete semirings.

Proof. We argue by induction on the structure of t. Our claim is clear when t is a variable or one of the constants 0, 1, as is the induction step when t is the sum or product of two terms. Suppose finally that t = μx.t′, where t′ = t′(x_{1}, …, x_{n}, x). By the induction hypothesis, we have that either t′(0, …, 0) = 0 in all algebraically complete semirings, or else t′(0, …, 0) ≥ 1 in all algebraically complete semirings. In the first case, clearly 0 is the least pre-fixed point of the map a ↦ t′_{A}(0, …, 0, a), over all algebraically complete semirings A, so that t(0, …, 0) = 0 holds in all such semirings. In the second case, the least pre-fixed point of the above map is at least 1 in each A, since t′_{A}(0, …, 0) ≥ 1. Thus, t(0, …, 0) ≥ 1 holds. □

Proposition 7.11 Suppose that p⃗ = (p_{1}, …, p_{n}) is a vector of polynomials in the variables x⃗ = (x_{1}, …, x_{n}) such that no i ∈ [n] is eventually zero or finite in p⃗. Then

μx⃗.p⃗ = (1^{∗}, …, 1^{∗})

holds in all algebraically complete semirings.

Proof. It is clear that (1^{∗}, …, 1^{∗}) is a solution to the fixed point equation x⃗ = p⃗, in all algebraically complete semirings, since no i ∈ [n] is eventually zero or finite in p⃗. Hence, μx⃗.p⃗ ≤ (1^{∗}, …, 1^{∗}) holds. Below we show that μx⃗.p⃗ ≥ (1^{∗}, …, 1^{∗}) holds.

Consider the direct dependency graph on the set of integers [n] determined by p⃗, which has a directed edge from i to j iff i directly depends on j (in p⃗.)

Let H_{1}, …, H_{k} denote all the maximal strongly connected subgraphs of the dependency graph with the property that whenever they contain a vertex i, they contain each vertex j on which i depends. Clearly, from every vertex there is a directed path to at least one of the subgraphs H_{1}, …, H_{k}, i.e., each vertex depends on at least one vertex in H_{1} ∪ … ∪ H_{k}.

First we show that (μx⃗.p⃗)_{i} ≥ 1^{∗} holds in all algebraically complete semirings for each i ∈ H_{1} ∪ … ∪ H_{k}, say in H_{1}. Without loss of generality we may assume that H_{1} = [m], for some m ∈ [n]. Since H_{1} contains each vertex accessible from the vertices of H_{1} by a directed path, each p_{j} with j ∈ [m] contains only variables in the set {x_{1}, …, x_{m}}. Thus, by Theorem 5.3,

μ(x_{1}, …, x_{m}).(p_{1}, …, p_{m}) = (μx⃗.p⃗)_{[m]}

holds in all algebraically complete semirings, in fact in all algebraic Conway semirings. It cannot be the case that each p_{j} with j ∈ [m] has a zero constant term, since otherwise the integers in [m] would all be eventually zero in p⃗. Let i denote an integer in [m] such that p_{i} has a nonzero constant term. Now, since H_{1} is strongly connected, by repeated substitutions of components p_{j} for the variables x_{j} starting from p_{i}, we obtain a polynomial q_{i} which contains x_{i} (in a monomial with nonzero coefficient) and has a nonzero constant term. Proposition 5.5 and the permutation identity guarantee that

μ(x_{1}, …, x_{m}).(p_{1}, …, p_{i}, …, p_{m}) = μ(x_{1}, …, x_{m}).(p_{1}, …, q_{i}, …, p_{m}).

Also, by Proposition 7.4, no component of μ(x_{1}, …, x_{m}).(p_{1}, …, q_{i}, …, p_{m}) is 0 in all algebraically complete semirings, so that by Lemma 7.10 each is at least 1 in each algebraically complete semiring. Thus, by the fixed point equation and monotonicity,

(μ(x_{1}, …, x_{m}).(p_{1}, …, q_{i}, …, p_{m}))_{i} ≥ μx_{i}.q_{i}(1, …, 1, x_{i}, 1, …, 1)

which is 1^{∗} in all algebraically complete semirings, by Lemma 7.9. Now, using the fact that each integer in [m] depends on i, it follows by the fixed point identity that all other components of μ(x_{1}, …, x_{m}).(p_{1}, …, q_{i}, …, p_{m}) and hence of μ(x_{1}, …, x_{m}).(p_{1}, …, p_{m}) are also ≥ 1^{∗}, in all algebraically complete semirings. Thus, for all i ∈ H_{1}∪…∪H_{k} we have (μ(x_{1}, …, x_{n}).(p_{1}, …, p_{n}))_{i} ≥ 1^{∗} in all algebraically complete semirings.

Finally, since any other component depends on some component in the union of the H_{j}, the same applies to any component of μ(x_{1}, …, x_{n}).(p_{1}, …, p_{n}). □

Proof of Theorem 7.2. We know that in algebraically complete semirings, t is equivalent to the first component of μx⃗.p⃗, for some vector p⃗ of finite polynomials in the variables x⃗. If 1 is eventually 0 or finite with value v, then t = 0 or t = v holds in all algebraically complete semirings, respectively. Otherwise t = 1^{∗} holds. To see this, substitute 0 for all variables x_{j} in p⃗ such that j is eventually 0 and the constant v for all variables x_{j} eventually finite with value v, and apply the previous proposition. □

8 Open problems

By general arguments, free algebraically complete (idempotent) semirings exist.

Problem 8.1 Find concrete representations of the free algebraically complete (idempotent) semirings.

We conjecture that the one-generated free algebraically complete (idempotent) semiring consists of the algebraic series in ℕ_{∞}⟨⟨a^{∗}⟩⟩ (regular = context-free languages in {a}^{∗}, respectively), where a is a single letter. When |A| ≥ 2, it is not true that the free algebraically complete semiring on A is the semiring of algebraic series in ℕ_{∞}⟨⟨A^{∗}⟩⟩. Also, when |A| ≥ 2, the free algebraically complete idempotent semiring on A is not the semiring of context-free languages in A^{∗}.

We have established ϵ-elimination in algebraically complete idempotent semirings.

Problem 8.2 Does ϵ-elimination hold in all algebraically complete semirings? Does it hold in all algebraic Conway semirings satisfying 1^{∗} = 1^{∗∗}?

It is known that ℕ_{∞} is initial in the class of all Conway semirings satisfying 1^{∗} = 1^{∗∗}.

Problem 8.3 Is ℕ_{∞} initial in the class of all algebraic Conway semirings satisfying 1^{∗} = 1^{∗∗}?

Problem 8.4 To what extent do the normal form theorems hold when, as in process algebra, we only have one-sided distributivity of multiplication over sum?

Problem 8.5 Is every Kleene algebra embeddable in an idempotent algebraically complete semiring? Is every symmetric inductive ^{∗}-semiring embeddable in an algebraically complete semiring?

If so, then the Horn theory of Kleene algebras, which is undecidable (by a result of E. Cohen, cf. [17]), is the same as the rational Horn theory of idempotent algebraically closed semirings.

References

[1] L. Aceto, Z. Ésik and A. Ingólfsdóttir. A fully equational proof of Parikh’s theorem. Theoretical Informatics and Applications, 36 (2002), 129–154.

[2] J. W. de Bakker and D. Scott. A theory of programs. IBM Seminar, August, 1969.

[3] H. Bekić. Definable operations in general algebra, and the theory of automata and flowcharts. Technical Report, IBM Laboratory, Vienna, 1969.

[4] L. Bernátsky, S.L. Bloom, Z. Ésik, and Gh. Stefanescu. Equational theories of relations and regular sets, extended abstract. In Proc. of the Conf. on Words, Combinatorics and Semigroups, Kyoto, 1992, pages 40–48. World Scientific Publishing Co. Pte. Ltd., 1994.

[5] S. L. Bloom and Z. Ésik. Iteration algebras, Int. J. Foundations of Computer Science, 3 (1991), 245–302.

[6] S. L. Bloom and Z. Ésik. Iteration Theories, Springer, 1993.

[7] M. Boffa. Une remarque sur les systmes complets d’identités rationnelles. RAIRO Inform. Théor. Appl., 24 (1990), 419–423.

[8] M. Boffa: Une condition impliquant toutes les identits rationnelles. RAIRO Inform. Thor. Appl., 29 (1995), 515–518.

[9] J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

[10] Z. Ésik. Completeness of Park induction, Theoretical Computer Science, 177 (1997), 217–283.

[11] Z. Ésik and W. Kuich. Inductive ∗-semirings. To appear in Theoretical Computer Science.

[12] S. A. Greibach. A new normal-form theorem for context-free, phrasestructure grammars. Journal of the Association for Computing Machinery, 12 (1965), 42–52.

[13] M. Harrison. Introduction to Formal Languages. Addison Wesley, Reading, Mass., 1978.

[14] J. Hopcroft and J. D. Ullman. Formal Languages and their Relation to Automata. Addison Wesley, Reading, Mass., 1979.

[15] M. W. Hopkins and D. Kozen. Parikh’s theorem in commutative Kleene algebra. In Proc. IEEE Conf. Logic in Computer Science (LICS’99), IEEE Press, 1999, 394–401.

[16] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In 6th Ann. Symp. on Logic in Computer Science, LICS’91. Computer Society Press, 1991, 214–225.

[17] D. Kozen. On the complexity of reasoning in Kleene algebra. In Proc. 12th Symp. Logic in Computer Science, IEEE Press, 1997, 195–202.

[18] D. Krob. Complete systems of B-rational identities. Theoret. Comput. Sci., 89 (1991), 207–343.

[19] W. Kuich. Semirings and formal power series. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 1, pages 609–678. Springer, 1997.

[20] H. Leiß. Towards Kleene Algebra with Recursion. In Proc. 5th Workshop on Computer Science Logic, CSL ’91. Springer LNCS 626, 242– 256, 1991.

[21] K. C. Ng and A. Tarski. Relation algebras with transitive closure. Notices of the American Math. Society, 24:A29–A30, 1977

[22] D. Niwinski. Equational μ-calculus. In Computation Theory (Zaborow, 1984), pages 169–176, Springer LNCS 208, 1984.

[23] V. R. Pratt. Action Logic and Pure Induction. In Logics in AI: European Workshop JELIA ’90. Springer LNCS 478, 97–120, 1990.

[24] V. N. Redko. On the determining totality of relations for the algebra of regular events. (Russian) Ukrain. Mat. Ž., 16 (1964), 120–126.

[25] D. J. Rosenkrantz. Matrix equations and normal forms for context-free grammars. Journal of the Association for Computing Machinery, 14 (1967), 501–507.

[26] A. Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the Association for Computing Machinery, 13 (1966), 158–169.

[27] L. Santocanale. On the equational definition of the least prefixed point. In MFCS 2001, pages 645-656, Springer LNCS 2136, 2001.

9 Appendix

We mention some partial results concerning ϵ-elimination in algebraically complete semirings that extend Lemma 6.8. For a grammar μx⃗.t⃗(x⃗, z⃗), let k⃗ be the constant terms and s⃗(x⃗, z⃗) the polynomials defined in the proof of Lemma 6.8. We want to prove

k⃗ + μx⃗.s⃗ ≤ μx⃗.t⃗  (61)

without continuity or idempotency. This is possible if there are no parameters z⃗:

Proposition 9.1 Suppose the decomposition t⃗(x⃗, z⃗) = q⃗(x⃗, z⃗) + p⃗(x⃗) + c⃗ of Lemma 6.8 satisfies q⃗(x⃗, z⃗) ≡ 0. Then (61) and hence ϵ-elimination holds in all algebraically complete semirings.

Proof. By the assumption, k⃗ = μx⃗(p⃗(x⃗) + c⃗) = μx⃗.t⃗. Hence it is sufficient to show that μx⃗.s⃗ = 0. Recall that s⃗(x⃗) consists of the non-constant monomials of t⃗[x⃗ + k⃗/x⃗] = p⃗[x⃗ + k⃗/x⃗] + c⃗. Using the distribution laws of the semiring, with fresh variables y⃗ we can write

p⃗(x⃗ + y⃗) = r⃗(u⃗, x⃗, y⃗)[x⃗ + y⃗/u⃗] + p(y⃗),

where p⃗(y⃗) collects all monomials of p(x⃗ + y⃗) in y⃗ alone, and r⃗(u⃗, x⃗, y⃗) are polynomials in u⃗, x⃗, y⃗. By the construction, no monomial of r⃗ contains only variables from y⃗. Also, no monomial of r⃗ contains only variables from u⃗, since otherwise r⃗[x⃗ + y⃗/u⃗] contained a monomial in the variables y⃗ alone. Hence for all elements u⃗, y⃗ we have μx⃗.r⃗(u⃗, x⃗, y⃗) = 0. But since

t(x⃗ + k⃗) = p⃗(x⃗ + k⃗) + c⃗ = r⃗(x⃗ + k⃗, x⃗, k⃗) + p⃗(k⃗) + c⃗,

we have s⃗(x⃗) = r⃗(x⃗+k⃗, x⃗, k⃗) and hence μx⃗.s⃗ = μz⃗μx⃗.r(z⃗+k⃗, x⃗, k⃗) = μz⃗. 0 = 0. □

A sufficient condition for (61) is the following:

Proposition 9.2 Let s⃗(x⃗, z⃗) and k⃗ be obtained from t⃗(x⃗, z⃗) as in Lemma 6.8. Then

k⃗ + μx⃗.t⃗ ≤ μx⃗.t⃗ ⇒ k⃗ + μx⃗.s⃗ ≤ μx⃗.t⃗  (62)

holds in any algebraically complete semiring.

Proof. We assume k⃗ + μx⃗.t⃗ ≤ μx⃗.t⃗ and suppress the parameters z⃗ in the following. By the choice of s⃗, we have ∀x⃗(s⃗(x⃗) ≤ t⃗(x⃗ + k⃗)), hence

μx⃗.s⃗ ≤ μx⃗.t⃗(x⃗ + k⃗)
≤ k⃗ + μx⃗.t⃗(x⃗ + k⃗)
= μx⃗(k⃗ + t⃗(x⃗)),

using the composition identity in the last step. But μx⃗(k⃗ + t⃗(x⃗)) ≤ μx⃗.t⃗ by the induction rule, because from the fixed-point inequation and the assumption, we get

k⃗ + t⃗(μx⃗.t⃗) ≤ k⃗ + μx⃗.t⃗
≤ μx⃗.t⃗.

Thus, μx⃗.s⃗ ≤ μx⃗.t⃗, and using the assumption again, the claim k⃗ + μx⃗.s⃗ ≤ k⃗ + μx⃗.t⃗ ≤ μx⃗.t⃗ follows from the monotonicity of +. □

Recall that k⃗ ≤ μx⃗.t⃗ always holds, which in the idempotent case is equivalent to k⃗ + μx⃗.t⃗ = μx⃗.t⃗. Hence Propostion 9.2 provides another proof of ϵelimination for idempotent algebraically closed semirings. It also yields a further case of ϵ-elimination:

Corollary 9.3 Suppose A is an algebraically complete semiring satisfying x ≤ y ⟺ ∃z(x + z = y), and that t⃗(x⃗, z⃗), s⃗(x⃗, z⃗) and k⃗ are as in Lemma 6.8. If each component of k⃗ is 0 or 1^{∗}, then k⃗ + μx⃗.s⃗ ≤ μx⃗.t⃗ holds in A.

Proof. By (62), it is sufficient to show k⃗ + μx⃗.t⃗ ≤ μx⃗.t⃗. From the definition of k⃗, we know that k⃗ ≤ μx⃗.t⃗ holds, so for given elements z⃗ there exists some b⃗ such that k⃗ + b⃗ = μx⃗.t⃗. By the assumption on k⃗, we have k⃗ + k⃗ = k⃗, and hence k⃗ + μx⃗.t⃗ = μx⃗.t⃗. □

Lemma 9.4 For every polynomial t(x, z⃗) in a single variable x and parameters z⃗ there is a constant k ∈ K and a polynomial s(x, z⃗) without non-zero constant monomials such that

μx.t = k + μx.s

holds in all algebraically complete semirings.

Proof. We can write t(x, z⃗) = q(x, z⃗) + p(x) + c where c is the sum of constant, p(x) the sum of pure and q(x, z⃗) that of the remaining monomials of t. If c = 0 or p = 0, then k := μx(p(x) + c) = c, and the claim follows by Proposition 9.7 below. Otherwise, 1 ≤ c and p has a monomial x^{m} for some m ≥ 1. Then k = μx(p(x) + c) = 1^{∗} by Lemma 7.9. Next, we show that

k + μx.t ≤ μx.t.  (63)

We distinguish two cases. If m > 1, then from 1 ≤ 1^{∗} = k ≤ μx.t we get

k + μx.t ≤ μx.t + μx.t
= 2(μx.t)
≤ (μx.t)(μx.t)
≤ p(μx.t)
≤ t(μx.t)
= μx.t.

Otherwise, if m = 1 for all monomials x^{m} of p, then p(x) = dx for some constant d ∈ K − {0}. Using equation (28) and d^{∗}c = k = k + k, we obtain

μx.t = μx(q(x, z⃗) + dx + c)
= μx(d^{∗}q(x, z⃗) + d^{∗}c)
= μx(q̃ + k)
= q̃[μx(q̃ + k)/x] + k
= q̃[μx(q̃ + k)/x] + k + k
= μx.t + k,

where q̃(x, z⃗) = d^{∗}q(x, z⃗). Having (63), the claim follows by (62) and Lemma 6.8. □

Example 9.5 Let t(x, z) ≡ xxz + xx + 2x + 1^{∗}. Separating the pure and constant monomials, we get t(x, y) ≡ q(x, z) + p(x) + c for q(x, z) := xxz, p(x) := xx + 2x, and c := 1^{∗}. From p(c) + c = 1^{∗} · 1^{∗} + 2 · 1^{∗} + 1^{∗} = 1^{∗} = c we obtain k := μx(p(x) + c) = 1^{∗} and hence

t(x + k, z) = (x + k)(x + k)z + (x + k)(x + k) + 2(x + k) + 1
= (x + k)(x + k)z + 2x(x + k) + kk + 2x + 2k + 1

So t(x + k, z) = s(x, z) + k for

s(x, z) := (x + k)^{2}z + 2x(x + k + 1)
= x^{2}z + 1^{∗}xz + 1^{∗}z + 2x^{2} + 1^{∗}x.

Therefore, elimination of ϵ-rules leads to

μx.t(x, z) = 1^{∗} + μx.s(x, z)

The next example demonstrates that (63) does not hold for term vectors μx⃗.t⃗ of length > 1, and hence is not a necessary condition for (61).

Example 9.6 Let x⃗ = (x, y, z) and t⃗(x⃗) = (x + 1, 1, xy). We obtain

c⃗ = (1, 1, 0),
p⃗(x⃗) = (x, 0, xy),
k⃗ = μx⃗(p⃗(x⃗) + c⃗)
= μx⃗.t⃗
= (1^{∗}, 1, 1^{∗}).

In particular, note that k⃗ + c⃗ = (1^{∗}, 2, 1^{∗}) ≰ (1^{∗}, 1, 1^{∗}) = k⃗, hence also k⃗ + k⃗ ≰ k⃗ and so we don’t have

k⃗ + μx⃗.t⃗ ≤ μx.t⃗.

We also don’t have μx⃗.t⃗(x⃗ + c⃗) ≤ μx⃗.t⃗. But by Proposition 9.1, k⃗ + μx⃗.s⃗ ≤ μx⃗.t⃗ still holds.

Proposition 9.7 Suppose the decomposition t⃗(x⃗, z⃗) = q⃗(x⃗, z⃗) + p⃗(x⃗) + c⃗ of Lemma 6.8 satisfies c⃗ = k⃗ where k⃗ := μx⃗(p⃗(x⃗) + c⃗). Then (61) and hence ϵ-elimination holds.

In particular, we have c⃗ = k⃗ whenever p⃗(x⃗) = 0 or c⃗ = 1^{∗} or c⃗ = 0.

Proof. The polynomials s⃗(x⃗, z⃗) as defined in Lemma 6.8 satisfy

s⃗(x⃗, z⃗) ≤ q⃗(x⃗ + k⃗, z⃗) + p⃗(x⃗ + k⃗).

Using monotonicity, the composition identity and k⃗ ≤ c⃗ we get

k⃗ + μx⃗.s⃗ ≤ k⃗ + μx⃗(q⃗(x⃗ + k⃗) + p⃗(x⃗ + k⃗))
= μx⃗(q⃗(x⃗) + p⃗(x⃗) + k⃗)
≤ μx⃗(q⃗(x⃗) + p⃗(x⃗) + c⃗)
= μx⃗.t⃗.

Note that

μx⃗(q⃗(x⃗, z⃗) + p⃗(x⃗) + k⃗) ≤ μx⃗(q⃗(x⃗, z⃗) + p⃗(x⃗) + c⃗).  (64)

is sufficient for the proof. □

Example 9.8 Let t⃗(x, y, a, b) = (ax + 1, bx^{2}y + 1), where x⃗ = (x, y) and z⃗ = (a, b). We have p⃗ = 0 and so k⃗ = c⃗ = (1, 1). By the definition of μx⃗.t⃗ we obtain

μx⃗.t⃗ = μ(x, y)(ax + 1, bx^{2}y + 1)
= (μx.(ax + 1)[μy(bxy+)/y], μy.(bx^{2}y + 1)[μx(ax + 1)/x])
= (a^{∗}, μy(ba^{∗}a^{∗}y + 1))
= (a^{∗}, (ba^{∗}a^{∗})^{∗}).

Since p⃗ = 0, the non-constant part of t⃗(x⃗ + k⃗) is s⃗(x⃗) = (a(x + 1), b(x + 1)^{2}(y + 1)). Hence, writing a^{+} for a^{∗}a,

μx⃗.s⃗ = μ(x, y)(ax + a, b(x + 1)^{2}(y + 1))
= (μx.(ax + a), μy.(b(x + 1)^{2}(y + 1))[μx(ax + a)/x])
= (a^{+}, μy.(b(a^{+} + 1)^{2}(y + 1)))
= (a^{+}, (ba^{∗}a^{∗})^{+}),

and indeed, k⃗ + μx⃗.s⃗ = (1, 1) + (a^{+}, (ba^{∗}a^{∗})^{+}) = (a^{∗}, (ba^{∗}a^{∗})^{∗}) = μx⃗.t⃗.

In Example 9.6, we do have (64) with k⃗ ≠ c⃗, because q⃗ = 0 and

μx⃗(p⃗ + k⃗) = μx⃗.(x + 1^{∗}, 1, xy + 1^{∗}) = (1^{∗}1^{∗}, 1, 1^{∗}1 + 1^{∗}) = k⃗ = μx⃗(p⃗ + c⃗).

The next Example 9.9 shows that (64) is also not a neccessary condition for (61).

Example 9.9 Let t⃗(x⃗) := (0, 0, xy) + (1, 1, 0) = p⃗(x⃗) + c⃗. Then k⃗ = μx⃗(p⃗ + c⃗) = μ(x, y, z).(1, 1, xy) = (1, 1, 1), but

μx⃗(p⃗ + k⃗) = μ(x, y, z)(0 + 1, 0 + 1, xy + 1)
= (1, 1, 2)
≰ (1, 1, 1)
= μx⃗(p⃗ + c⃗).

By Proposition 9.1, k⃗ + μx⃗.s⃗ = μx⃗.t⃗ still holds.

Recent BRICS Report Series Publications

RS-02-46 Zoltán Ésik and Hans Leiß. Greibach Normal Form in Algebraically Complete Semirings. December 2002. 43 pp. An extended abstract appears in Bradfield, editor, European Association for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O(2.4023^{n}) Using Maximal Independent Sets. December 2002. 6 pp.

RS-02-44 Zoltán Ésik and Zoltán L. Németh. Higher Dimensional Automata. November 2002. 32 pp. A preliminary version appears under the title Automata on Series-Parallel Biposets in Kuich, Rozenberg and Salomaa, editors, 5th International Conference, Developments in Language Theory, DLT ’01 Revised Papers, LNCS 2295, 2001, pages 217–227. This report supersedes the earlier BRICS report RS-01-24.

RS-02-43 Mikkel Christiansen and Emmanuel Fleury. Using IDDs for Packet Filtering. October 2002. 25 pp.

RS-02-42 Luca Aceto, Jens A. Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. Checking Consistency of Pedigree Information is NP-complete (Preliminary Report). October 2002. 16 pp.

RS-02-41 Stephen L. Bloom and Zoltán Ésik. Axiomatizing Omega and Omega-op Powers of Words. October 2002. 16 pp.

RS-02-40 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Note on an Expressiveness Hierarchy for Multi-exit Iteration. September 2002. 8 pp.

RS-02-39 Stephen L. Bloom and Zoltán Ésik. Some Remarks on Regular Words. September 2002. 27 pp.

RS-02-38 Daniele Varacca. The Powerdomain of Indexed Valuations. September 2002. 54 pp. Short version appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, LICS ’02 Proceedings, 2002, pages 299–308.