BRICS RS-01-22 Z. Ésik: The Equational Theory of Fixed Points with Applications BRICS

Basic Research in Computer Science

The Equational Theory of Fixed Points with Applications to Generalized Language Theory

Zoltán Ésik

BRICS Report Series RS-01-22 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Zoltán Ésik.

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/01/22/

The Equational Theory of Fixed Points with Applications to Generalized Language

Theory^{∗}

Dedicated to Prof. Werner Kuich on the occasion of his 60th birthday

Z. Ésik^{†}

Dept. of Computer Science University of Szeged P.O.B. 652, 6720 Szeged Hungary

esik@inf.u-szeged.hu

Abstract

We review the rudiments of the equational logic of (least) fixed points and provide some of its applications for axiomatization problems with respect to regular languages, tree languages, and synchronization trees.

1 Introduction

A classic result of the theory of context-free languages is Parikh’s theorem [32] that asserts that the letter occurrence vectors (Parikh vectors) corresponding to the words of a context-free language on a k-letter alphabet form a semilinear subset of N^{k}, the free commutative monoid of k-dimensional vectors over the naturals. The theorem is usually proved by combinatorial arguments on the derivation trees of the context-free grammar. However, as Pilling [35] observed, Parikh’s theorem may be formulated as an assertion about “rational functions” on the (free) commutative idempotent continuous semiring of all subsets of N^{k}. Subsequently, Kuich [28] generalized Parikh’s result to all commutative idempotent continuous semirings (l-semirings). (See also [27] for a related treatment.) In fact, by introducing rational terms that denote rational functions, or more generally, recursion terms or μ-terms denoting functions that arise as least solutions of systems of polynomial fixed point equations, Parikh’s theorem can be translated into a statement about the equational theory of commutative idempotent continuous semirings: For every μ-term t there exists a rational term r such that the equation t = r holds in all commutative idempotent continuous semirings. Alternatively, one may just consider rational terms and prove that for each rational term t(x, y_{1}, …, y_{n}) in the variables x, y_{1}, …, y_{n} there is a rational term r(y_{1}, …, y_{n}) containing no occurrence of x that provides least solution to the fixed point equation x = t(x, y_{1}, …, y_{n}) over all commutative idempotent continuous semirings. This approach has been pursued by Hopkins and Kozen in [23], in their argument lifting Parikh’s theorem to all commutative idempotent semirings with enough least fixed points to provide solutions to recursion equations. By proving this more general result, Hopkins and Kozen have shown how to replace the analytic arguments of Pilling and Kuich by arguments based only on the the least (pre-)fixed point rule (also known as the Park induction rule [33]), the fixed point equation, and the algebraic laws of the sum and product operations. But since Parikh’s theorem is a claim about equational theories, one would eventually like to have a purely equational proof of it. This question has been addressed recently in [1]. In this paper, Parikh’s theorem is derived from a small set of purely equational axioms involving fixed points.

∗To appear in the proceedings of Developments in Language Theory, Vienna, 2001.

†Partially supported by grant No. T22423 from the National Foundation of Hungary for Scientific Research and the Austrian-Hungarian Cooperative Research grant OMFB A-4/99.

Parikh’s theorem is not the only result of automata and language theory that can be derived by simple equational reasoning from the algebraic properties of fixed points. Other applications of the equational logic of fixed points include Kleene’s theorem and its generalizations [7], see also [28, 29, 9], where the presentation is not fully based on equational reasoning, and Greibach’s theorem [19]. The methods employed in the papers [26, 17] even indicate that one can embed the Krohn-Rhodes decomposition theorem [21] for finite automata and semigroups within equational logic. Further applications of fixed point theory include an algebraic proof of the soundness and relative completeness of Hoare’s logic [5, 6]. See also [25].

The aim of this paper is to provide an introduction to the basics of the equational theory of fixed points and to show some of its applications in the solution of axiomatization problems for “generalized languages”. In his book, Conway formulated several conjectures regarding the equational theory of the regular sets. Some of his conjectures have since been confirmed (e.g., the completeness of the group-identities, settled by Krob in [26]), but some are still open. In particular, Conway’s “letter reduction” conjecture is still open. In this paper, we generalize both Conway’s group-identities and his letter reduction conjecture to continuous algebras over any signature. Just as in the classical setting of regular languages, the group-identities are complete, in conjunction with the classical identities. The generalized letter reduction conjecture remains open.

2 Preiteration algebras

Terms, or μ-terms, over the signature Σ are defined by the syntax

T ::= x | σ(\overbrace{T, …, T}^{n−times}) | μx.T,

where x ranges over a countably infinite set V of variables, and for each n ≥ 0, σ ranges over Σ_{n}, the set of n-ary function symbols in Σ. Free and bound occurrences of variables in a term are defined as usual. We identify any two μ-terms that differ only in the bound variables. Moreover, for any μ-terms t, t_{1}, …, t_{n} and distinct variables x_{1}, …, x_{n}, we write t[t_{1}/x_{1}, …, t_{n}/x_{n}] or t[(t_{1}, …, t_{n})/(x_{1}, …, x_{n})] for the term obtained by simultaneously substituting t_{i} for x_{i}, for each i ∈ [n] = {1, …, n}. Since we may assume that the bound variables in t are different from the variables that have a free occurrence in the terms t_{i}, no free variable in any t_{i} may become bound as the result of the substitution. Below, we will write t(x_{1}, …, x_{n}) or t(x⃗), where x⃗ = (x_{1}, …, x_{n}) to denote that t is a term with free variables in the set {x_{1}, …, x_{n}}. When writing μ-terms, we assume that the scope of a prefix μx extends to the right as far as possible.

We will be interested in interpretations where μx.t provides a “canonical solution” to the fixed point equation x = t.

A preiteration Σ-algebra is a nonempty set A together with an interpretation of the terms t as functions t_{A} : A^{V} → A such that the following hold:

1. When t is a variable x ∈ V, then t_{A} is the corresponding projection A^{V} → A, i.e., t_{A}(ρ) = ρ(x), for all ρ : V → A.

2. For any terms t, t_{1}, …, t_{n} and different variables x_{1}, …, x_{n},

(t[(t_{1}, …, t_{n})/(x_{1}, …, x_{n})])_{A}(ρ) = t_{A}(ρ[x_{i} ↦ (t_{i})_{A}(ρ) : i ∈ [n]]),

for all ρ : V → A, where for any (a_{1}, …, a_{n}) ∈ A^{n}, the function ρ[x_{i} ↦ a_{i} : i ∈ [n]] is the same as ρ except that it maps each x_{i} to a_{i}.

3. If t, t′ are terms with t_{A} = t′_{A}, then for all variables x, also (μx.t)_{A} = (μx.t′)_{A}.

4. For any t and variable x which has no free occurrence in t, the function t_{A} does not depend on its argument corresponding to x, i.e., (μx.t)_{A}(ρ) = (μx.t)_{A}(ρ[x ↦ b]), for all ρ : X → A and b ∈ A.

A strong preiteration algebra is a preiteration algebra that satisfies the following strengthened version of the third condition above: For all terms t, t′ and for all ρ : V → A and x ∈ V, if t_{A}(ρ[x ↦ a]) = t′_{A}(ρ[x ↦ a]), for all a ∈ A, then (μx.t)_{A}(ρ) = (μx.t′)_{A}(ρ).

We will also consider ordered preiteration Σ-algebras which are preiteration Σ-algebras A equipped with a partial order ≤ such that each term function t_{A} is monotonic with respect to the pointwise order on A^{V}, and such that the following stronger version of the third condition above is satisfied: If t, t′ are terms over Σ with t_{A} ≤ t′_{A} in the pointwise order, then for all variables x, also (μx.t)_{A} ≤ (μx.t′)_{A}. The “ordered notion” corresponding to strong preiteration Σ-algebras is the notion of strong ordered preiteration Σ-algebra which is defined in the obvious way.

Below, if t = t(x_{1}, …, x_{n}) and if A is an (ordered) preiteration Σalgebra with a_{1}, …, a_{n} ∈ A, we write t_{A}(a_{1}, …, a_{n}) for t_{A}(ρ), where ρ : V → A maps each x_{i} to a_{i}, i ∈ [n].

A morphism of (strong) preiteration Σ-algebras A and B is a function h : A → B such that

h(t_{A}(a_{1}, …, a_{n})) = t_{B}((h(a_{1}), …, h(a_{n})),

for all terms t(x_{1}, …, x_{n}), and for all (a_{1}, …, a_{n}) ∈ A^{n}. A morphism of (strong) ordered preiteration Σ-algebras also preserves the partial order.

Note that any preiteration Σ-algebra A determines a Σ-algebra: For each σ ∈ Σ_{n} and (a_{1}, …, a_{n}), we define σ_{A}(a_{1}, …, a_{n}) = t_{A}(a_{1}, …, a_{n}), where t is the term σ(x_{1}, …, x_{n}) for some sequence of different variables x_{1}, …, x_{n}. Also, any preiteration algebra morphism is a Σ-algebra homomorphism.

First-order formulas involving μ-terms over Σ are constructed form atomic formulas t = t′, where t and t′ are μ-terms, in the expected way. In the ordered setting, expressions t ≤ t′ are also atomic formulas. Free and bound occurrences of variables in a formula and substitution are defined as usual. A formula with no free variables is called a sentence. The semantic notion of satisfaction is defined in the usual Tarskian style. Suppose that A is an (ordered) preiteration algebra, ρ is a function V → A and φ is a formula. We write (A, ρ) ⊧ φ to denote that A satisfies φ under the given evaluation of the variables. When ϕ is a sentence, we say that A satisfies φ, or that φ holds in A, notation A ⊧ φ, if (A, ρ) ⊧ φ for all, or for some ρ. (Note that a preiteration algebra is not empty.)

Most sentences that we will encounter in this paper fall into three categories. First of all, we will have equations and inequations that are sentences of the form ∀x_{1} … ∀x_{n}(t = t′) and ∀x_{1} … ∀x_{n}(t ≤ t′), respectively, also denoted as ∀x⃗(t = t′) and ∀x⃗(t ≤ t′). An equation is also called an identity. Second, we will consider implications of the form ∀x⃗(t_{1} = t′_{1}∧…∧t_{k} = t′_{k} ⇒ t = t′) and ∀x⃗(t_{1} ≤ t′_{1}∧…∧t_{k} ≤ t′_{k} ⇒ t ≤ t′). Finally, we will also have implications between equations (or inequations) that are of the form ∀x⃗(t_{1} = t′_{1} ∧ … ∧ t_{k} = t′_{k}) ⇒ ∀y⃗(s = s′). As usual, we will abbreviate an equation as t = t′, an inequation as t ≤ t′, and an implication as t_{1} = t′_{1} ∧ … ∧ t_{k} = t′_{k} ⇒ t = t′, etc.

Example 2.1 Every preiteration Σ-algebra satisfies the implication between equations

∀x∀y⃗(t = t′) ⇒ ∀y⃗(μx.t = μx.t′),

for all terms t(x, y⃗), t′(x, y⃗) over Σ. A preiteration algebra is strong iff it satisfies all sentences

∀y⃗(∀x(t = t′) ⇒ μx.t = μx.t′).

3 Continuous algebras

Recall that a cpo is a poset (A, ≤) which has a least element, denoted ⊥_{A}, and such that each directed set^{1} D ⊆ A has a supremum ⋁ D. Note that when A is a cpo, so is any direct power of A equipped with the pointwise ordering, as is the direct product of any number of cpo’s.

1A set D ⊆ A is called directed if it is not empty and each pair of elements in D has an upper bound in D.

Suppose that A and B are cpo’s and f is a function A → B. We call f monotonic if f(a) ≤ f(b) whenever a ≤ b in A. Moreover, we call f continuous if f is monotonic and f(⋁ D) = ⋁ f(D) holds for all directed sets D ⊆ A. Finally, we call f strict if f(⊥_{A}) = ⊥_{B}.

Below we will make use of the following well-known properties of continuous functions.

Proposition 3.1 Each projection function ∏_{i∈I} A_{i} → A_{j} from a direct product of cpo’s A_{i}, i ∈ I to a cpo A_{j} is continuous. Moreover, if f : A_{1} × … × A_{n} → A and g_{1} : B → A_{1}, …, g_{n} : B → A_{n} are continuous, where A, B, A_{1}, …, A_{n} are all cpo’s, then so is the function h : B → A defined by h(b) = f(g_{1}(b), …, g_{n}(b)), for all b ∈ B.

When f : A × B → A and b is a fixed element of B, let f_{b} denote the function A → A defined by f_{b}(a) = f(a, b).

Proposition 3.2 Suppose that A and B are cpo’s and f is a continuous function A × B → A. Then for each b ∈ B there is a least a = f^{†}(b) which is a pre-fixed point of f_{b}, i.e., such that f(a, b) ≤ a. Moreover, f^{†} : B → A, as a function of b, is continuous.

The least pre-fixed point a is in fact a fixed point of f_{b}, i.e., f(a, b) = a. Indeed, since f(a, b) ≤ a and f is monotonic, also f(f(a, b), b) ≤ f(a, b), showing that f(a, b) is a pre-fixed point. But since a is the least pre-fixed point, we have that a ≤ f(a, b), which, together with f(a, b) ≤ a gives f(a, b) = a.

A continuous Σ-algebra consists of a cpo (A, ≤) and a Σ-algebra (A, Σ) such that each operation σ_{A} : A^{n} → A, σ ∈ Σ_{n} is continuous. A morphism of continuous Σ-algebras is a strict continuous Σ-algebra homomorphism.

Each continuous Σ-algebra A gives rise to a strong ordered preiteration Σ-algebra. We define t_{A} by induction on the structure of the term t. Suppose that ρ : V → A.

1. When t is the variable x, we define t_{A}(ρ) = ρ(x).

2. When t is a term of the form σ(t_{1}, …, t_{n}), we let t_{A}(ρ) = σ_{A}((t_{1})_{A}(ρ), …, (t_{n})_{A}(ρ)).

3. When t is of the form μx.t′, then we define t_{A}(ρ) to be the least a ∈ A with t_{A}(ρ[x ↦ a]) ≤ a, in fact t_{A}(ρ[x ↦ a]) = a.

The fact that t_{A} is a well-defined continuous function A^{V} → A follows from Propositions 3.1 and 3.2. Since strict continuous functions preserve least pre-fixed points, it follows that each strict continuous morphism A → B, where A and B are continuous Σ-algebras, is a (strong) preiteration algebra morphism.

Since in continuous algebras, μ-terms are interpreted by least prefixed points, we have:

Proposition 3.3 Each continuous Σ-algebra satisfies the fixed point equation

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

and the implication

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

for all terms t over Σ, and all variables x, y.

Note that the fixed point equation (1) is not a single equation, but in fact an equation scheme. Nevertheless, following standard practice, we will call such schemes just equations.

The above implication (2) is sometimes referred to as the Park induction rule [33], or the least pre-fixed point rule. It is an instance of a more general induction principle attributed to Scott. See also [2]. The Park induction rule has a weak version, which is an implication between inequations: For all terms t(x, y⃗) and t′(y⃗)

∀y⃗(t[t′/x] ≤ t′) ⇒ ∀y⃗(μx.t ≤ t′).

4 Conway algebras

A (strong) Conway Σ-algebra [7] is a (strong) preiteration algebra satisfying the following diagonal (3) and rolling equations (4) for all terms t, t′ over Σ and for all variables x, y:

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

The above equations are by now classic, see [22, 2, 31], to mention a few early references. A morphism of Conway Σ-algebras is a preiteration Σ-algebra morphism. Note that when t′ is the variable x, (4) reduces to the fixed point equation defined above. Thus, in Conway algebras, μx.t provides a canonical solution to the fixed point equation x = t. A strong Conway algebra is also a strong preiteration algebra. Strong Conway Σalgebras satisfy the same equations as Conway Σ-algebras.^{2} Morphisms of (strong) Conway algebras are preiteration algebra morphisms.

It turns out that in Conway algebras it is also possible to solve systems of fixed point equations. Below we will often consider term vectors t⃗ = (t_{1}, …, t_{n}), where n is any positive integer. We say that a variable has a free occurrence in t⃗ if it has a free occurrence in one of the t_{i}. Bound occurrences are defined in the same way. Substitution into a term vector is defined component-wise. When t⃗ = (t_{1}, …, t_{n}) and A is a preiteration algebra, t⃗_{A} : A^{V} → A^{n} is the function ρ ↦ ((t_{1})^{A}(ρ), …, (t_{n})_{A}(ρ)). We identify any vector of dimension 1 with its unique component. A formula t⃗ = s⃗, where t⃗ = (t_{1}, …, t_{n}) and s⃗ = (s_{1}, …, s_{n}), is viewed as an abbreviation for the formula t_{1} = s_{1} ∧ … ∧ t_{n} = s_{n}. Formulas t⃗ ≤ s⃗ are abbreviations in the same way.

Suppose that t⃗ = (t_{1}, …, t_{n}) is a vector of terms and x⃗ = (x_{1}, …, x_{n}) is a vector of different variables of the same dimension n ≥ 1. We define the term vector μx⃗.t⃗ by induction on n. When n = 1, we define μx⃗.t⃗ = (μx_{1}.t_{1}). When n > 1, we let

μx⃗.t⃗ = (μ(x_{1}, …, x_{n−1}).(t_{1}, …, t_{n−1})[μx_{n}.t_{n}/x_{n}],
μx_{n}.t_{n}[μ(x_{1}, …, x_{n−1}).(t_{1}, …, t_{n−1})/(x_{1}, …, x_{n−1})]).

The above definition is motivated by the Bekić–De Bakker–Scott rule [3, 2]. See also Pilling [35].

Proposition 4.1 Suppose that t⃗(x⃗, y⃗) and s⃗(x⃗, y⃗) are n-dimensional term vectors where x⃗ and y⃗ are vectors of distinct variables such that the dimension of x⃗ is n.

1. If A is a preiteration algebra then

A ⊧ ∀x⃗, y⃗(t⃗ = s⃗) ⇒ ∀y⃗(μx⃗.t⃗ = μx⃗.s⃗).

2. If A is a strong preiteration algebra then

A ⊧ ∀y⃗(∀x⃗(t⃗ = s⃗) ⇒ ∀y⃗(μx⃗.t⃗ = μx⃗.s⃗)).

2An equation holds in a “variety” of preiteration algebras iff it holds in the strong preiteration algebras belonging to that variety. See [7].

Theorem 4.2 [7] If A is a Conway algebra, then the “vector forms” of (3) and (4) hold in A: For all term vectors t⃗(x⃗, y⃗, z⃗), where t⃗, x⃗ and y⃗ have the same dimension,

A ⊧ μx⃗.t⃗[x⃗/y⃗] = μx⃗.μy⃗.t⃗.  (5)

Moreover, for all term vectors t⃗(y⃗, z⃗) and s⃗(x⃗, z⃗), where the dimension of t⃗ agrees with that of x⃗ and the dimension of s⃗ with that of y⃗,

A ⊧ μx⃗.t⃗[s⃗/y⃗] = t⃗[μx⃗.s⃗[t⃗/x⃗]/y⃗].  (6)

Corollary 4.3 For each term vector t⃗ and vector of distinct variables x⃗ of the same dimension, the equation

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

holds in all Conway algebras.

Equation (7) is the vector form of the fixed point equation (1). Since by Theorem 4.2, the vector forms of (3) and (4) hold in any Conway Σ-algebra, so does the vector form of any other equation that holds in these algebras.

Corollary 4.4 If an equation holds in all Conway Σ-algebras, then so does its vector form.

For a full characterization of the equations of Conway Σ-algebras we refer to [4]. It is shown in op. cit. that when Σ contains a symbol of rank > 1 then it is PSPACE-complete to decide whether an equation holds in all Conway Σ-algebras, whereas the problem easily lies in P if each symbol in Σ has rank at most 1.

We now give a characterization of Conway algebras based on the vector form of the fixed point identity.

Theorem 4.5 The following three conditions are equivalent for a preiteration Σ-algebra A.

1. A is a Conway Σ-algebra.

2. The vector form of the fixed point equation holds in A.

3. A satisfies the fixed point equation for binary vectors.

Below we will abbreviate the term μx.x as ⊥. Suppose that X and Y are finite disjoint sets of variables. We call a term t over Σ primitive with respect to (X, Y) if it is either ⊥, or a variable in Y, or a term σ(x_{1}, …, x_{k}), where σ ∈ Σ_{k} and the not necessarily different variables x_{1}, …, x_{k} are all in X. The following fact is a version of Salomaa’s equational characterization of regular languages [36], see also [12, 30]. In [14, 7], the result is derived only from the equational axioms of Conway algebras.

Theorem 4.6 Normal forms [14, 7] For each term t(y⃗) in the free variables y⃗ = (y_{1}, …, y_{m}) there exists an integer n ≥ 1, a vector x⃗ = (x_{1}, …, x_{n}) of fresh variables and terms s_{1}, …, s_{n}, all primitive with respect to (X, Y), where X = {x_{1}, …, x_{n}} and Y = {y_{1}, …, y_{m}}, such that equation

t = (μ(x_{1}, …, x_{n}).(s_{1}, …, s_{n}))_{1}

holds in all Conway algebras, where the right side of the equation is the first component of the term vector μ(x_{1}, …, x_{n}).(s_{1}, …, s_{n}).

The following result is essentially due to Bekić and De Bakker and Scott.

Theorem 4.7 [2, 3] Suppose that A is an ordered preiteration Σ-algebra satisfying the fixed point equation (1) and the Park induction principle (2). Then A is a strong preiteration algebra. Moreover, the vector form of the fixed point equation (7) and the vector form of the Park induction rule (8) hold in A:

t⃗[y⃗/x⃗] ≤ y⃗ ⇒ μx⃗.t⃗ ≤ y⃗,  (8)

for all term vectors t⃗ over Σ of dimension n, and all vectors of distinct variables x⃗, y⃗ of dimension n.

We call such algebras Park Σ-algebras. Morphisms of Park Σ-algebras are order preserving preiteration algebra morphisms. Any such morphism is strict.

Remark 4.8 Each ordered preiteration Σ-algebra satisfying the fixed point equation and the weak version of the Park induction rule satisfies the vector forms of these axioms.

5 Iteration algebras

In his book [10], John H. Conway associated an equation of regular sets with every finite group and conjectured that a finite set of classical identities together with the equations associated with the finite (simple) groups form a complete set of equations for the regular sets. Conway’s equations can be generalized.

Suppose that G is a finite group with elements {g_{1}, …, g_{n}}, and let t(x⃗, y⃗) denote a term over some signature Σ, where x⃗ = (x_{1}, …, x_{n}) and y⃗ = (y_{1}, …, y_{m}), so that the dimension of x⃗ agrees with the order of G. For each i ∈ [n], let π_{i} : [n] → [n] denote the function j ↦ k iff g_{i} · g_{j} = g_{k}. Define

s_{i} = t[(x_{π_{i}(1)}, …, x_{π_{i}(n)})/(x_{1}, …, x_{n})], i ∈ [n].

Let x denote a fresh variable. The group-equation or group-identity [17] associated with G is:

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

(The definition of the equation associated with G also depends on the ordering of the group elements g_{1}, …, g_{n}. However, with respect to the Conway identities, different orderings result in equivalent equations.) A (strong) iteration Σ-algebra is a (strong) Conway Σ-algebra satisfying the group-equations associated with the finite groups. Strong iteration Σ-algebras and iteration Σ-algebras satisfy the same equations. A morphism of (strong) iteration algebras is a preiteration algebra morphism.

Theorem 5.1 [17] If an equation holds in iteration Σ-algebras, then so does its vector form.

Theorem 5.2 [17] An equation holds in all iteration Σ-algebras iff it holds in all continuous Σ-algebras.

For the axiomatization of iteration algebras based on variants of the Conway identities and the commutative identity, the above result was established in [14]. See [7] for a thorough treatment of the earlier results.

Suppose that A is a set disjoint from Σ and does not contain the special symbol ⊥. A partial (Σ, A)-tree [22, 12] is an at most countable, ordered rooted tree whose nodes are labeled by the elements of Σ∪A∪{⊥} such that nodes labeled in Σ_{n} have n descendants and all the nodes labeled in A ∪ {⊥} are leaves. Say that T ≤ T′, for trees T and T′, if T′ can be constructed from T by attaching non-uniformly (Σ, A)-trees to the leaves of T labeled ⊥. Equipped with this partial order, the set (Σ, A)T of (Σ, A)-trees is a cpo whose bottom element is the one-node tree labeled ⊥. Moreover, equipped with the usual Σ-operations, (Σ, A)T is a continuous Σ-algebra, in fact, the free continuous Σ-algebra on A.

Theorem 5.3 [22] For each set A, the algebra (Σ, A)T is freely generated by A in the class of all continuous Σ-algebras.

Corollary 5.4 An equation holds in all iteration Σ-algebras iff it holds in continuous Σ-algebras (Σ, A)T.

Call a tree (Σ, A) total if it has no leaves labeled ⊥. Moreover, call a tree (Σ, A)-tree regular if it has a finite number of (nonisomorphic) subtrees. Note that every finite tree is regular. It turns out that the free iteration Σ-algebras may also be represented by trees.

Theorem 5.5 [14] The free iteration Σ-algebra on a set A can be represented as the algebra (Σ, A)R of regular (Σ, A)-trees.

Remark 5.6 The algebra of regular (Σ, A)-trees is also free in the class of regular Σ-algebras [22, 37], and the algebra of total regular trees is free in the class of iterative Σ-algebras [12].

Corollary 5.7 [11] There is a polynomial time algorithm to decide for an equation between terms over Σ whether it holds in all iteration Σalgebras.

For later use we recall:

Theorem 5.8 [15] Every Park Σ-algebra, or ordered iteration algebra satisfying the fixed point equation and the weak version of the Park induction rule, is an iteration algebra. An equation between terms over Σ holds in all Park Σ-algebras iff it holds in all iteration Σ-algebras.

Corollary 5.9 For each set A, the algebra of regular trees (Σ, A)R, equipped with the partial order inherited from (Σ, A)R, is freely generated by A in the class of all Park Σ-algebras.

Theorem 5.8 is a hidden completeness result. It follows that an equation between μ-terms over Σ holds in all continuous Σ-algebras iff it can be derived from (instances of) the fixed point equation using the usual rules of (in)equational logic and a non-standard rule corresponding to the weak version of the Park induction principle. This logic was proposed in [31].

5.1 A conjecture

In addition to the completeness of the group-identities and the classical identities for the equational theory of the regular sets, Conway [10] conjectured that the system consisting of the classical identities and an equation derived for each n ≥ 3 from the n-state automaton with an input letter inducing a transposition and a letter inducing a cyclic permutation is also complete. As a consequence of the conjecture, it would follow that the regular identities in at most three variables form a complete system, whereas no upper bound on the number of variables is known to date.

In this section, we formulate a related conjecture for continuous Σalgebras (or equivalently, by Theorem 5.2, for iteration Σ-algebras).

For each n ≥ 3 and term t over Σ, consider the equation

μz.t[(z, z)/(x, y)] = μx.t[(t[t′/y], t[t′/y])/(x, y)],  (10)

where t′ is the term (μy.t)^{n−2} obtained by substituting (n − 3)-times the term μy.t for x in μy.t. (Thus, e.g., (μy.t)^{2} = (μy.t)[μy.t/x].)

Conjecture 5.10 A preiteration Σ-algebra is an iteration Σ-algebra iff it is a Conway Σ-algebra and satisfies the equation (10), for each n ≥ 3.

If this conjecture holds, then so does Conway’s.

6 Algebras with a semilattice structure

We will consider preiteration Σ-algebras equipped with a commutative idempotent additive structure. These are in fact preiteration Δ-algebras for the signature Δ = Σ_{+} that results by adding the binary symbol + to Δ. Such a preiteration algebra is called a semilattice preiteration Σalgebra if it satisfies the equations:

x + (y + z) = (x + y) + z  (11)
x + y = y + x  (12)
x + x = x  (13)
x + ⊥ = x.  (14)

Thus, semilattice preiteration Σ-algebras have the structure of a commutative idempotent monoid with neutral element the constant denoted by the term ⊥, i.e., μx.x. Each such algebra A comes with the semilattice order defined by a ≤ b iff a + b = b. Note that ⊥_{A} is least with respect to this order.

A semilattice Σ-algebra is called continuous if, equipped with the semilattice order, it is a continuous Σ-algebra. Note that if A is a continuous semilattice algebra then A is in fact a complete semilattice, i.e., it has all suprema. Moreover, since the + operation is automatically continuous, A is a continuous Δ-algebra for the enlarged signature Δ = Σ_{+}. Hence, by Theorem 5.2, any continuous semilattice Σ-algebra is a strong iteration Δ-algebra and satisfies the Park induction rule, i.e., it is a Park Δ-algebra. We call such algebras semilattice Park algebras. In a similar fashion, we define a semilattice Conway Σ-algebra (semilattice iteration Σ-algebra, respectively) to be a semilattice preiteration Σ-algebra which is a Conway Δ-algebra (iteration Δ-algebra, respectively). Morphisms of continuous semilattice Σ-algebras are continuous Δ-algebra morphisms. Morphisms of semilattice preiteration Σ-algebras, semilattice Conway algebras and semilattice iteration algebras and semilattice Park Σ-algebras are just preiteration Δ-algebra morphisms. Note that morphisms are automatically monotonic.

We end this section with a normal form theorem that applies to all semilattice Conway Σ-algebras, and thus to continuous semilattice Σalgebras, semilattice Park Σ-algebras and semilattice iteration Σ-algebras. We will return to semilattice iteration Σ-algebras, and in particular to continuous semilattice Σ-algebras in Section 8.

A simple term over Σ_{+} is a term that is the finite sum of different primitive terms over Σ excluding ⊥. More precisely, given a pair (X, Y) of disjoint sets of variables, a simple term over (X, Y) is a finite sum of pairwise different terms of two types: Terms σ(x_{1}, …, x_{k}), where σ is in Σ and each x_{i} is in X, and terms y, for y a variable in Y. By assumption, the empty sum is ⊥, so that the term ⊥ itself is simple. The next result is a version of Milner’s equational characterization of regular processes, cf. [30].

Theorem 6.1 [18] For each term t over Σ_{+} with free variables in Y = {y_{1}, …, y_{p}} there exist a set X = {x_{1}, …, x_{n}} and simple terms t_{1}, …, t_{n} over (X, Y) such that

t = (μ(x_{1}, …, x_{n}).(t_{1}, …, t_{n}))_{1}

holds in all additive Conway Σ-algebras satisfying

μx.x + y = y.  (15)

Remark 6.2 In Conway Σ_{+}-algebras, (15) is a strengthened form of idempotence. In fact, (13) follows from the fixed point equation and (15).

7 Regular languages and tree languages

Suppose that A is a Σ-algebra. Then we may turn P(A), the power set of A into a Δ-algebra, where Δ = Σ_{+}. For each σ ∈ Σ_{n} and B_{1}, …, B_{n} ∈ P (A), we define

σ(B_{1}, …, B_{n}) = {σ(b_{1}, …, b_{n}) : b_{i} ∈ B_{i}, i ∈ [n]}.

Moreover, we define B_{1} +B_{2} = B_{1} ∪B_{2}, for all B_{1}, B_{2} ∈ P(A). Equipped with these operations, P(A) is a continuous semilattice Σ-algebra, hence a (strong) semilattice iteration Σ-algebra and a semilattice Park Σ-algebra. Note that when A is the free Σ-algebra (Σ, B)FT of finite (complete) (Σ, B)-trees, then P(A) is the algebra of all (finite total) (Σ, B)-tree languages that we denote by (Σ, B)TL.

Theorem 7.1 [13] For each set A, (Σ, A)TL is freely generated by A in the class of all continuous semilattice Σ-algebras satisfying the following equations for all σ ∈ Σ_{n} and i ∈ [n], n > 0:

σ(x_{1} + y_{1}, …, x_{n} + y_{n}) = ∑_{z_{i}∈{x_{i},y_{i}}} σ(z_{1}, …, z_{n})  (16)
σ(x_{1}, …, ⊥, …, x_{n}) = ⊥.  (17)

On the left-hand side of (17), the symbol ⊥ is on the ith position. Suppose now that Σ is a unary signature, i.e., each symbol in Σ

has rank one. Then a finite total tree in (Σ, A)FT may be represented as a word in Σ^{∗}A. Hence (Σ, A)TL is just the algebra of languages in Σ^{∗}A equipped with the prefixing operations L ↦ σL, σ ∈ Σ, and the operation of set union as its sum operation. We let (Σ^{∗}A)L denote this continuous semilattice Σ-algebra. By our general results, (Σ^{∗}A)L is a (strong) semilattice iteration Σ-algebra and a semilattice Park Σalgebra. The regular sets in (Σ^{∗}A)L determine a subalgebra, denoted (Σ^{∗}A)RL, which is also a strong semilattice iteration Σ-algebra and a semilattice Park Σ-algebra. The following result is a reformulation of Krob’s theorem [26] that confirms a conjecture of Conway [10]. In [17], Krob’s result is derived from Theorem 5.2.

Theorem 7.2 [26] For each set A and unary signature Σ, the algebra (Σ^{∗}A)RL is freely generated by A in the class of all (strong) semilattice iteration Σ-algebras satisfying (15) and

t[y + z/x] = t[y/x] + t[z/x]  (18)
t[0/x] = 0,  (19)

for all terms t = t[x] over Σ_{+} containing at most the free variable x.

Since each semilattice Park Σ-algebra is an iteration Σ-algebra (Theorem 5.8), and since (Σ^{∗}A)RL is a semilattice Park Σ-algebra, by Krob’s theorem we have

Corollary 7.3 For each set A and each unary signature Σ, the algebra (Σ^{∗}A)RL is freely generated by A in the class of all semilattice Park Σalgebras satisfying (18) and (19).

This corollary may be viewed as a strengthened version of Kozen’s axiomatization [24] of the equational theory of the regular sets.

Corollary 7.4 The following conditions are equivalent for an equation t = t′ between μ-terms over Σ_{+}, where Σ is a unary signature.

1. The equation holds in all continuous semilattice Σ-algebras equipped with operations satisfying (16) and (17).

2. The equation holds in all algebras (Σ^{∗}A)L of languages, or (Σ^{∗}A)RL of regular languages.

3. The equation holds in all semilattice Park Σ-algebras satisfying (16) and (17).

4. The equation holds in all (strong) semilattice iteration Σ-algebras satisfying (18), (19) and (15).

We do not know how Theorem 7.2 carries over to arbitrary signatures. Nevertheless the following result holds for all signatures containing symbols of arbitrary rank. For regular tree languages we refer to [20].

Theorem 7.5 [16] For each signature Σ and set A, the algebra (Σ, A)RL of regular tree languages is freely generated by the set A in the class of all semilattice Park Σ-algebras satisfying (16) and (17).

Note that since distributivity is required here only for basic symbols, this result is stronger for unary signatures than Corollary 7.3.

Corollary 7.6 The following conditions are equivalent for an equation t = t′ between μ-terms over Σ_{+}.

1. The equation t = t′ holds in all continuous semilattice Σ-algebras equipped with operations satisfying (16) and (17).

2. The equation t = t′ holds in all complex algebras P(A) derived from Σ-algebras.

3. The equation t = t′ holds in all algebras (Σ, A)TL of languages, or (Σ, A)RL of regular tree languages.

4. The equation t = t′ holds in all semilattice Park Σ-algebras satisfying (16) and (17).

8 Synchronization trees

In this section, we consider the class of all continuous semilattice Σalgebras, where Σ is any signature. The basic question we seek answer to is to provide a basis of identities for these structures. We refer to [30] and in particular [18] for the definition of (Σ, A)-labeled synchronization trees and the definition of simulation, originally introduced in [34].

Theorem 8.1 [18] For each signature Σ and set A, the algebra (Σ, A)RST of regular synchronization trees over A is freely generated by A in the class of all semilattice iteration Σ_{+}-algebras satisfying (15) and

t ≤ t[x + y]  (20)
μx.t ≤ μx.t + t′  (21)

for all terms t over Σ_{+} and variables x, y.

Note that the meaning of (20) is that each function induced by any term t is monotonic, while (21) can be rephrased as an implication between equations:

∀x, y⃗(t ≤ t′) ⇒ ∀y⃗(t ≤ t′),

where t(x, y⃗) and t′(x, y⃗) are any terms over Σ_{+}.

Since (Σ, A)RST can be embedded in a continuous semilattice Σalgebra, as shown in [18], we have:

Theorem 8.2 [18] The following conditions are equivalent for an equation t = t′ between terms over Σ_{+}:

1. t = t′ holds in all continuous semilattice Σ-algebras.

2. t = t′ holds in all semilattice Park Σ-algebras.

3. t = t′ holds in all iteration semilattice Σ-algebras satisfying (15), (20) and (21).

4. t = t′ holds in all algebras of regular synchronization trees modulo simulation.

It is natural to ask what happens if we drop (20) and (21) in Theorem 8.1. The answer to this question was given in [8]: The free algebras can be described as bisimulation equivalence classes of regular synchronization trees.

9 Conclusion

Several models studied in computer science have some facility of recursion, usually modeled by fixed points. Continuous algebras are those cpo’s equipped with a Σ-algebra structure whose operations are continuous, giving rise to recursive definitions by least fixed points. Unfortunately, for μ-terms, the equational theory of the class of models studied is not always recursive, or recursively enumerable. For example, the equational theory of languages equipped with sum (set union) and concatenation as basic operations is not r.e., due to the fact that the equivalence of context-free grammars is not semidecidable. However, the theory of all continuous algebras is decidable, and in fact lies in P, and several equational theories are finitely axiomatizable over it. Moreover, the equations of fixed points in continuous algebras are quite general, and can thus be taken as a basis for the study of the respective equational theories. The relative axiomatization results presented here and elsewhere also provide a classification of the models by their logical properties. We have seen such examples in Sections 7 and 8. It would be of great importance to explore the boundary between axiomatizability and nonaxiomatizability, and decidability and undecidability.

10 Acknowledgment

This paper was prepared during the author’s visit at BRICS (Basic Research in Computer Science, Centre of the Danish Research Foundation) and the Department of Computer Science of the University of Aalborg. He would like to thank the members of the Department, and in particular Anna Ingólfsdóttir, Luca Aceto and Kim G. Larsen, for their hospitality.

References

[1] L. Aceto, Z. Ésik and A. Ingólfsdóttir. In preparation.

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

[3] H. Bekić. Definable operations in general algebra. Technical Report, IBM Laboratory, Vienna, 1969.

[4] L. Bernátsky and Z. Ésik, Semantics of flowchart programs and the free Conway theories. RAIRO Inform. Théor. Appl., 32(1998), 35–78.

[5] S. L. Bloom and Z. Ésik. Floyd-Hoare logic in iteration theories. J. Assoc. Comput. Mach., 38(1991), 887–934.

[6] S. L. Bloom and Z. Ésik. Program correctness and matricial iteration theories. In: Proc. Mathematical Foundations of Programming Semantics’91, LNCS 598, Springer-Verlag, 1992, 457–475.

[7] S. L. Bloom and Z. Ésik. Iteration Theories. Springer-Verlag, 1993.

[8] S. L. Bloom, Z. Ésik and D. Taubner. Iteration theories of synchronization trees. Inform. and Comput., 102(1993), 1–55.

[9] S. Bozapalidis. Equational elements in additive algebras. Theory Comput. Syst., 32(1999), 1–33.

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

[11] B. Courcelle, G. Kahn and J. Vuillemin. Algorithmes d’équivalence et de réduction á des expressions minimales dans une classe d’équations récursives simples. In Proc. ICALP 74, Saarbrücken, LNCS 14, Springer, 200–213.

[12] C. C. Elgot, S. L. Bloom and R. Tindell. On the algebraic structure of rooted trees. J. Comput. System Sci., 16(1978), 362–399.

[13] J. Engelfriet and E. M. Schmidt. IO and OI. I. J. Comput. System Sci., 15(1977), 328–353.

[14] Z. Ésik. Identities in iterative and rational algebraic theories. Comput. Linguist. Comput. Lang., 14(1980), 183–207.

[15] Z. Ésik. Completeness of Park induction. Theoret. Comput. Sci., 177(1997), 217–283.

[16] Z. Ésik Axiomatizing the equational theory of regular tree languages. In: Proc. STACS 98, Paris, LNCS 1373, Springer, 1998, 455–466.

[17] Z. Ésik. Group axioms for iteration. Inform. and Comput., 148(1999), 131–180.

[18] Z. Ésik. Axiomatizing the least fixed point operation and binary supremum. In: Proc. CSL 2000, LNCS 1862, Springer-Verlag, 302– 316.

[19] Z. Ésik and H. Leiß. In preparation.

[20] F. Gécseg and M. Steinby. Tree Automata. Akadémiai Kiadó. Budapest, 1984.

[21] A. Ginzburg. Algebraic theory of automata. Academic Press, New York–London, 1968.

[22] J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B. Wright. Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach., 24(1977), 68–95.

[23] 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, July 1999, 394-401.

[24] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In: Proc. 1991 IEEE Symposium on Logic in Computer Science (Amsterdam, 1991), and Inform. and Comput., 110(1994), 366–390.

[25] D. Kozen. On Hoare logic and Kleene algebra with tests. In: Proc. IEEE Conf. Logic in Computer Science (LICS’99), IEEE, July 1999, 167–172, and ACM Trans. Computational Logic, 1(2000), 60–76.

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

[27] I. Takanami and N. Honda. A characterization of Parikh’s theorem and semilinear sets by commutative semigroups with length. Electronics and Communications in Japan, 52(1969), 179–184.

[28] W. Kuich. The Kleene and the Parikh theorem in complete semirings. In: Proc. ICALP ’97, LNCS 267, Springer-Verlag, 212–225.

[29] W. Kuich. Gaussian elimination and a characterization of algebraic power series. In: Proc. Mathematical Foundations of Computer Science, 1998, LNCS 1450, Springer, Berlin, 1998, 512–521.

[30] R. Milner. A complete inference system for a class of regular behaviors. J. Comput. System Sci., 28(1984), 439–466.

[31] D. Niwinski. Equational μ-calculus. In: Computation Theory (Zaborw, 1984), LNCS 208, Springer, 1985, 169–176.

[32] R. J. Parikh. On context-free languages. J. Assoc. Comput. Mach., 4(1996), 570–581.

[33] D. Park. Fixpoint induction and proofs of program properties. In: Machine Intelligence, 5, American Elsevier, New York, 1970, 59–78.

[34] D. Park. Concurrency and automata on infinite sequences. In: Proc. GI Conf., LNCS 104, Springer, 1981, 167–183.

[35] D. L. Pilling. Commutative regular equations and Parikh’s theorem. J. London Math. Soc., 6(1973), 663–666.

[36] A. Salomaa. Two complete axiom systems for the algebra of regular events. J. Assoc. Comput. Mach., 13(1966), 158–169.

[37] J. Tiuryn. Fixed-points and algebras with infinitely long expressions. I. Regular algebras. Fund. Inform., 2(1978/79), 103–127.

Recent BRICS Report Series Publications

RS-01-22 Zoltán Ésik. The Equational Theory of Fixed Points with Applications to Generalized Language Theory. June 2001. 21 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-21 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Theories of Tropical Semirings. June 2001. 52 pp. Extended abstracts of parts of this paper have appeared in Honsell and Miculan, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’01 Proceedings, LNCS 2030, 2000, pages 42–56 and in Gaubert and Loiseau, editors, Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, MAX-PLUS ’01 Proceedings, IFAC (International Federation of Automatic Control) IFAC Publications, 2001.

RS-01-20 Catuscia Palamidessi and Frank D. Valencia. A Temporal Concurrent Constraint Programming Calculus. June 2001. 31 pp.

RS-01-19 Jiří Srba. On the Power of Labels in Transition Systems. June

2001.

RS-01-18 Katalin M. Hangos, Zsolt Tuza, and Anders Yeo. Some Complexity Problems on Single Input Double Output Controllers. 2001. 27 pp.

RS-01-17 Claus Brabrand, Anders Møller, Steffan Olesen, and Michael I. Schwartzbach. Language-Based Caching of Dynamically Generated HTML. May 2001. 18 pp.

RS-01-16 Olivier Danvy, Morten Rhiger, and Kristoffer H. Rose. Normalization by Evaluation with Typed Abstract Syntax. May 2001. 9 pp. To appear in Journal of Functional Programming.

RS-01-15 Luigi Santocanale. A Calculus of Circular Proofs and its Categorical Semantics. May 2001. 30 pp.

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001. 38 pp.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.