AN INFINITE PEBBLE GAME AND APPLICATIONS

A.J. Kfoury^{∗}

Department of Computer Science

Boston University Boston, MA 02215, U.S.A.

A.P. Stolboushkin^{†} Program in Computing UCLA Department of Mathematics Los Angeles, CA 90024, U.S.A.

September 30, 1996

Contents

1 Introduction 1 2 The Infinite Pebble Game 1 3 Applying the Infinite Pebble Game 3 4 Two Specific Infinite Dag’s 3 5 A CFG of an Infinite Index 7 6 Bounded vs. Unbounded Memory 8 7 Conclusion 12

∗Partly supported by NSF grant CCR–9417382.

†Partly supported by NSF grant CCR–9403809.

1 Introduction

We generalize the pebble game to infinite dag’s (directed acyclic graphs), and we use this generalization to give new and shorter proofs of well-known results in two areas of computer science (as diverse as “logic of programs” and “formal language theory”).

Our main application is a short and perspicuous proof of a theorem that first appeared in Tiuryn [18] and (independently) in Erimbetov [2, 3], asserting that unbounded memory increases the power of logics of programs. The driving idea in these papers is an analysis of bounded-memory program logics in a free algebra of one binary function, involving back-and-forth constructions based on a variant of Ehrenfeucht-Fraïssé games. A careful implementation of this idea, however, becomes quite technical and lengthy. Musikaev and Taitslin [11] point to some, apparently correctable, problems in [18] and present another construction proving a stronger result from which the main theorem of [18, 2] follows, although comprehensibility remains an issue, to say the least.

By contrast, our proofs are not only shorter, but also elementary. All we need is essentially finite induction and some freshmen-level logic. We feel that our technique can be widely applied in computer science, and indeed we apply it to give a simple proof of a result due to Salomaa [15], asserting the existence of a context-free grammar with infinite index.

The peculiar structure N defined in Section 6 below was invented by the first author in [7], and the proof of Lemma 3 given in Section 4 was written by the second author as a result of reading [7] in 1986. However, without recent encouragement from D. Kozen, Y. Moschovakis, and J. Tiuryn, this paper might not have been written. We express our thanks to them all, as well as to M.A. Taitslin for his valuable comments. Special thanks are due to S. Gao and to the anonymous referees for their help in improving the present paper.

2 The Infinite Pebble Game

The standard pebble game on a finite dag D is defined as follows. At any point in the game, some nodes of D will have pebbles on them. A configuration is a subset of the nodes, comprising just those nodes that have pebbles on them. A legal move consists in either:

• removing a pebble from a node a, or

• placing a pebble on a node a′ such that all the immediate predecessors of a′ have pebbles on them, or

• leaving the configuration unchanged (this one is needed for technical reasons). An input node b is one that has no immediate predecessors, i.e. its in-degree = 0, and therefore a pebble may be placed on b at any time.

A legal move goes from a configuration C to a new configuration C′, and is therefore represented by the pair (C, C′). A calculation is a sequence of configurations, each successive pair of which being a legal move. A calculation is said to reach a node a if it includes a in one of its configurations.

The pebble game on a finite dag is usually examined to study questions of time-space trade-offs. “Time” corresponds to the number of moves in a calculation and “space” to the maximum number of nodes in any configuration in this calculation. The dag’s usually have exactly one output node, i.e. a node with out-degree = 0. We can state the aim of the pebble game on a finite dag D as follows:

Determine a lower bound on the number of pebbles required by a calculation that begins with the empty configuration and reaches the output node of D.

We have just described the basic pebble game on finite dag’s, the so-called “black pebble game”. There are several generalizations of the game on finite dag’s, introduced for various applications in computer science.^{1}

We now introduce the infinite pebble game. The game is played on an infinite dag D. The concepts of “configuration” and “legal move” are the same as in the case of the finite pebble game (a configuration C is a subset of the nodes of D, while a legal move either removes a node a from C or adds a node a′ to C provided all the immediate predecessors of a′ are in C). The aim of the pebble game on an infinite dag D is:

Determine a lower bound on the number of pebbles required by a calculation (necessarily infinite) that begins with the empty configuration and reaches every node of D.

We say that a dag D is n-accessible, or accessible to the n-pebble game, if there is a calculation that begins with the empty configuration, reaches the output node of D (if D is finite) or reaches all the nodes of D (if D is infinite), and uses at most n pebbles. The ω-pebble game is the one which can use countably many pebbles. We say that a dag D is ω-accessible if it is accessible to the ω-pebble game.

It is easy to see that a dag D is ω-accessible iff every node in D has finitely many predecessors (not necessarily all immediate). No calculation starting from the empty configuration can reach all the nodes of a dag which is not ω-accessible. We therefore limit our attention to dag’s D such that:

1. D is ω-accessible, and

2. D contains only finitely many input nodes

Requirement 1, ω-accessibility, is stronger than well-foundedness; in a well-founded dag there are no infinite descending chains, but this does not preclude the presence of nodes with infinitely many predecessors. Requirement 2, the restriction to finitely many input nodes, is added in order to make some of the definitions below compatible.

We need a finer view of the accessibility properties of a dag D. Following standard terminology in algebra, we say D is locally finite if every node in D has finitely many successors (not necessarily all immediate), and that D is uniformly locally finite if there is a constant k ⩾ 1 such that every node in D has at most k successors (not necessarily all immediate). We say D is uniformly locally finite w.r.t. bounded space if for every n ⩾ 1, there is a k_{n} ⩾ 1 such that every calculation of the n-pebble game on D reaches at most k_{n} nodes.

1Some of the generalizations of the game on finite dag’s are the “black-and-white pebble game”, the “pebble game with auxiliary pushdown stores”, the “edging game”, and the “parallel pebble game” (see [13], [14], [9], and [17], respectively). Other relevant research on finite pebble games can be found in [1], [6], and in their references.

If D is uniformly locally finite, then D is uniformly locally finite w.r.t. bounded space; in Section 4 we show the opposite implication is not always true.

It is also clear that if D is uniformly locally finite, then D is locally finite, and the opposite implication does not always hold. On the other hand, the class of locally finite dag’s and the class of dag’s that are uniformly locally finite w.r.t. bounded space are incomparable, i.e. neither contains the other. This last result, although not used in the applications of Sections 5 and 6, is easily derived from the analysis of Section 4.

3 Applying the Infinite Pebble Game

A finite dag D is always accessible to the |D|-pebble game, where |D| is the number of nodes in D. What makes the finite pebble game interesting is the possibility that fewer than |D| pebbles will also suffice. Using fewer than |D| pebbles will generally increase the time (the number of moves) required to reach the output node of D, and the hard question is usually to determine how time increases as the number of pebbles is decreased.

Similarly, what makes the infinite pebble game interesting is the fact that an infinite ω-accessible dag D may not be n-accessible for every finite n ⩾ 1 . In each of the applications below we want to prove that a certain resource cannot be finitely bounded. The resource in question in the Salomaa theorem is the number of “occurrences of variables in derivations in a context-free grammar”; in the Tiuryn-Erimbetov theorem, the resource is the number of “memory locations used by a program”. In each case this resource is simulated by the number of pebbles used in a game on an appropriately defined infinite dag.

In our infinite pebble game there are no time considerations. From the moment we prove that infinitely many pebbles are required to reach all the nodes of a dag, there is clearly no question of trading time (moves) for space (pebbles).

4 Two Specific Infinite Dag’s

Let ⟨f, a⟩ be a first-order signature, where f is a binary function symbol and a is a zero-ary (constant) symbol. We define A to be the set of all terms over ⟨f, a⟩, i.e., A is the least set such that:

A ⊇ {a} ∪ {f(t, u) | t, u ∈ A}

To turn A into a dag, we place an arrow from t ∈ A to u ∈ A iff u = f(t, t′) or u = f(t′, t) for some t′ ∈ A. It is clear that A is ω-accessible (every node has finitely many predecessors).

We consider another dag B. The set of nodes of B is ω, the set of all the natural numbers. For every integer n ⩾ 0 we place an arrow from n to n + 1, as well as an arrow from n to 2n + 1 and an arrow from n to 2n + 2. The dag B is conveniently viewed as two superimposed dag’s, B_{1} and B_{2}. B_{1} is the ordinary linear order of the natural numbers. B_{2} is the complete binary tree, where 0 is the root node and the nodes of the k-th level are 2^{k} − 1, …, 2^{k+1} − 2. It is clear that B is also an infinite ω-accessible dag. An initial fragment of B is shown below: B_{1} is described by the dashed arrows, and B_{2} by the plain arrows.

15  16  17  18  19  20  21  22  23  24  25  26  27  28  29  30 0 1  2 3  4  5  6  14 13 12 11 10 9 7  8

Lemmas 1 and 2 are simple and intuitive facts about the pebble game on an arbitrary dag (not only A or B), finite or infinite. We give formal proofs for the sake of completeness. If a and b are nodes in a dag D, we write a ⟶ b if there is an arrow from a to b. The transitive closure of ⟶ is denoted ⟶^{+}, and its reflexive transitive closure ⟶^{∗}.

Lemma 1 Let C be a configuration of the n-pebble game on a dag D, with n ⩾ 1. Let a ∈ D and b ∈ C such a ⟶^{+} b. If τ is a calculation of the n-pebble game on D starting with C such that:

• in every configuration C′ of τ, at least one element c ∈ C′ is such that b ⟶^{∗} c, and

• τ reaches a, then there exists a calculation τ̂ of the (n − 1)-pebble game on D that starts with the configuration C \ {b} and reaches a.

Proof: Intuitively, because b is not a predecessor of a, it follows that b (and all its successors) can be omitted from the calculation τ reaching a. More formally, let τ be the sequence of configurations C_{0}, C_{1}, C_{2}, …, where C_{0} = C. Let k ∈ ω be the least number such that a ∈ C_{k}. Define a new sequence of configurations Ĉ_{0}, Ĉ_{1}, …, Ĉ_{k}, where Ĉ_{j} = C_{j} \ {c | b ⟶^{∗} c} for every j = 1, …, k. Clearly, |Ĉ_{j}| ⩽ (n − 1) for every j = 1, …, k and, moreover, if (C_{j}, C_{j+1}) is a legal move then so is (Ĉ_{j}, Ĉ_{j+1}). The sequence Ĉ_{0}, Ĉ_{1}, …, Ĉ_{k} is therefore a calculation of the (n − 1)-pebble game which, moreover, reaches a because a ∈ Ĉ_{k}. The desired calculation τ′ is Ĉ_{0}, Ĉ_{1}, …, Ĉ_{k}. Q.E.D.

A subdag E of a dag D is obtained by removing: (1) some of the arrows, and (2) some of the nodes together with all arrows adjacent to these nodes. We can identify a dag by its set of arrows. The inward closure [E] of subdag E of D is the least set of arrows such that:

[E] ⊇ E ∪ { a ⟶ b ∈ D | there is a node c such that c ⟶ b ∈ [E] }

Nodes a and c in this definition are not necessarily distinct. E is inward closed if E = [E].

Lemma 2 If a dag D is accessible to the n-pebble game for some n ⩾ 1, then every inward closed subdag E of D is also accessible to the n-pebble game.

Proof: Suppose D is infinite (the finite case is similar). Let X = D \ E. Let C_{0}, C_{1}, … be a calculation that reaches all the nodes of D. Then (C_{0} \X), (C_{1} \X), … is a calculation that reaches all the nodes of E. Q.E.D.

Lemma 3 is specific to the dag B defined earlier. On the dag B, the relation i ⟶^{∗} j coincides with i ⩽ j (there is a directed path, not necessarily a single arrow, from i to j). Let C be a configuration in B, i.e., C is here a finite set of natural numbers, and k ⩾ 0 is an integer. We define the k-neighborhood of C, denoted N(C, k), as:

N(C, k) = {j | (∃i ∈ C ∪ {0}) [ j ⩾ i and j − i ⩽ k ] }

N(C, k) is clearly a finite set. We define the function α on the natural numbers inductively:

α(0) = 0  and  α(n + 1) = 4 · (n + 1) · (α(n) + 1) + 1 .

Lemma 3 Let C be a configuration of the n-pebble game on B, with n ⩾ 1. Every calculation of the n-pebble game on B that begins with configuration C can only reach nodes in N(C, α(n)).

Proof: By induction on n. The lemma is obviously true for n = 1. Proceeding inductively, assume it is true for any number of pebbles < n. Assume for a moment that the lemma fails for n. Then there exists a finite calculation τ in the n-game starting with C that reaches some k ∉ N(C, α(n)). Fix this k. Take the largest j ∈ C ⋃{0} such that j < k. Clearly, • k − j > α(n) , and

• the set {j + 1, j + 2, …, k} contains no element in C .

Fix this j as well.

Let C_{0} = C, and C_{i} be the i-th configuration in the calculation τ. Then let τ_{0} = τ, and τ_{i} be τ without the first i configurations.

Further let m = ⌈(k − j + 1)/2⌉ + j + 1, and let F = {m, m + 1, …, k}. In other words, F consists of the second half of the sequence {j + 1, j + 2, …, k}. It can be seen that F satisfies the following properties:

• no element of C belongs to F , and

• ⌊k/2⌋ < m .

Let ℓ be the least index such that for every i ⩾ ℓ, the set C_{i} contains an element in F. Clearly,

• the set C_{ℓ−1} contains no element of F, and

• for every j ∈ F there is an i ⩾ ℓ such that C_{i} contains j

Fix this ℓ. According to the rules of the pebble game, in order to place pebbles on the elements {m, m + 1, …, k}, it is necessary to have pebbles on ⌈m/2⌉ − 1, ⌈(m + 1)/2⌉ − 1, …, ⌈k/2⌉ − 1. Let F′ = {⌈m/2⌉ − 1, ⌈(m + 1)/2⌉ − 1, …, ⌈k/2⌉ − 1}. It follows from the properties of ℓ that for every j ∈ F′ there exists an i ⩾ ℓ such that j ∈ C_{i}. Since every j ∈ F′ is less than m, we may now apply Lemma 1. Thus there exists a calculation τ̂ in the (n − 1)-game starting with the configuration Ĉ_{ℓ} = C_{ℓ} \ {m} which, in contradiction with the induction hypothesis, reaches nodes outside of N(Ĉ_{ℓ}, α(n − 1)). Indeed, all the elements in the set F′ are reachable, while the cardinality of the set F′ is

|F′| = ⌊\frac{|F |}{2}⌋ ⩾ \frac{k − j}{4} > \frac{α(n)}{4} = \frac{4n(α(n − 1) + 1) + 1}{4} > n(α(n − 1) + 1) .

At the same time, |N(Ĉ_{ℓ}, α(n − 1))| ⩽ n(α(n − 1) + 1). Q.E.D.

Theorem 4 is an immediate consequence of Lemma 3 . It first appeared in [7], stated differently (Proposition 3, page 53), with a substantially longer proof (several journal pages).

Theorem 4 B is uniformly locally finite w.r.t. bounded space, but not uniformly locally finite.

Corollary 5 For every n ⩾ 1, the dag B is not accessible to the n-pebble game.

The following result follows from Lemma 2, Corollary 5 and the fact that the dag B is an inward closed subdag of the dag A.

Theorem 6 For every n ⩾ 1, the dag A is not accessible to the n-pebble game. (Note, however, that A is not uniformly locally finite w.r.t. bounded space.)

5 A CFG of an Infinite Index

Let G = (V, X, S, P) be a context-free grammar, where V is the set of variables, X the set of terminal letters, S ∈ V the start symbol, and P the production rules. For a word w ∈ (V ∪ X)^{∗}, we write V(w) for the word obtained from w by erasing all letters of X. The index of a derivation:

D : S = w_{0} ⇒ w_{1} ⇒ ⋯ ⇒ w_{n} = w

in G is defined by:

ind(D) = max{ |V(w_{i})| | i = 0, 1, …, n }

where |V(w_{i})| denotes the length of the word V(w_{i}). The index of a word w ∈ L(G) in G is:

ind(w, G) = min{ ind(D) | D : S ⟹^{∗} w }

The index of G, denoted ind(G), is the smallest integer n such that, for all w ∈ L(G), ind(w, G) ⩽ n. If no such n exists, G is said to be of infinite index. The index of a context-free language L is:

ind(L) = min{ ind(G) | L = L(G) }

Salomaa (see [15, 16]) proved that the following context-free grammar is of infinite index:

S ⟶ SS | (S) | ε

We prove that the same result for a slightly different grammar G̃:

S ⟶ (SS) | ()

We associate with the language L̃ generated by this grammar, the dag A of Section 4. If we consider the words of L̃ as nodes, and we place an arrow from v ∈ L̃ to w ∈ L̃ iff w = (vv′) or w = (v′v) for some v′ ∈ L̃, then the resulting dag is clearly isomorphic to A (with () being mapped to a). This isomorphism between L̃ and A, together with Theorem 6, allows us to prove the following results in a straightforward manner.

Theorem 7 The grammar G̃ is of infinite index.

Proof: Consider a derivation D. We scan this derivation in reverse order (starting with the last production), and play a pebble game as follows:

If at the current step the derivation applies the rule S ⟶ (), we place a new pebble on a and say that this pebble corresponds to the occurrence of S.

If at the current step the derivation applies the rule S ⟶ (SS), the two occurrences of S on the right-hand side correspond to some two pebbles in A that sit on some t, u ∈ A, respectively. We then place a pebble on f(t, u), and remove the two pebbles from t and u. The new pebble on f(t, u) is said to correspond to the occurrence of S on the left-hand side of the rule.

It is clear that, as the result of this game determined by the derivation D, we place a pebble on the isomorphic image of the word that D yields. It is also clear, that the number of pebbles used in the game is the index of the derivation D, plus 1. A minor difference from the definition of the pebble game is that we do allow more than one pebble to be put on the same node. However, this can be straightened out very easily. The theorem follows. Q.E.D.

¿From his grammar result, Salomaa [15, 16] went further and showed using a simple argument that the language of well-formed sequences of parentheses is of infinite index as well. Using the same argument, it can be shown that our language L̃ is of infinite index.

6 Bounded vs. Unbounded Memory

A fundamental result about program schemes is that unbounded memory adds to the computational power of programs.^{2} An early version of this result, comparing flowchart schemes and recursive schemes, was first proved by Paterson and Hewitt [12]. The result was later refined and reproduced relative to other classes of program schemes.

We will be deliberately vague in defining “program schemes”. There are several closely related definitions in the literature (e.g. see [5, 10]), which all start from the same basic programming formalism, and gradually add to it various features such as: non-determinism, recursive calls (with or without parameters, with or without higher-order parameters), counters, pushdown stores (binary and algebraic), arrays, and others. This same basic programming formalism is varyingly called: “flowchart programs”, “regular programs”, “while-programs”, and “iterative programs”, which are all assumed deterministic, and restricted to finitely many ground variables and atomic tests on ground variables.

Let P be an arbitrary member from anyone of these classes of program schemes. We leave it to the interested reader to check, by going back to the relevant literature, that P can always be translated into a possibly infinite non-deterministic if-fi statement, denoted eds(P), written as a recursively enumerable sequence of “guarded commands” (to use a well-established notion in programming). We call a recursively enumerable sequence of guarded commands an effective definitional scheme, abbreviated eds, where all the guarded commands are written over the same finite (first-order) signature and finite set of (first-order) variables. The uninterpreted function and relation symbols appearing in P form a finite signature, which is also the signature of eds(P). Following common notation, e.g. see [4], we take a guarded command as an expression of the form φ → t, where φ is a quantifier-free first-order formula and t is a first-order term, both containing no free variable other than the input variables of P. We can therefore write

eds(P) = ( φ_{i} → t_{i} | i ∈ I )

2Perhaps more accurately, we should say that it adds power to the “control structure” of programs, since we are dealing with program schemes (uninterpreted programs).

where I is an r.e. subset of ω. Let S = eds(P). Assuming that P takes one input value, stored in input variable x, and returns one output value,^{3} the interpretation of P (or S) in a first-order structure M with universe M, denoted P^{M} (or S^{M}), is the relation on M defined by the possibly infinite disjunction:

⋁_{i∈I}( φ_{i}(x) ∧ y = t_{i}(x) )

in the structure M, i.e.

P^{M} = S^{M} = {(a, b) ∈ M × M | there is an i ∈ I such that M ⊧ φ_{i}[a] ∧ b = t_{i}[a] } .

For this definition to make sense, the signature of P and S is assumed to be contained in the signature of M. Likewise, the interpretation of a term t in a structure M is denoted t^{M}.

With every first-order term t we associate a finite dag, called dag(t), with as many nodes as there are distinct subterms in t. The input nodes of dag(t) are labelled with the variables and constant symbols appearing in t, and its single output node is labelled with the full expression for t. Put differently, dag(t) is obtained from the parse tree of t by merging equal subterms. The pebble complexity of t is given by:

pebble(t) = min { n | dag(t) is accessible to the n-pebble game } .

The pebble complexity of a guarded command φ → t is:

pebble(φ → t) = max { pebble(t) } ∪ { pebble(u) | u is a term appearing in φ } .

The pebble complexity of an eds S = ( φ_{i} → t_{i} | i ∈ I ) is:

pebble(S) = lub { pebble(φ_{i} → t_{i}) | i ∈ I } .

We say that an eds S uses bounded space if pebble(S) < ω. Otherwise, if pebble(S) = ω, we say that S uses unbounded space. Let EDS denote the class of all effective definitional schemes. Let BOUNDED-EDS ⊂ EDS be the subclass of eds’s each restricted to use bounded space:

BOUNDED-EDS = { S ∈ EDS | pebble(S) < ω } .

An eds S = ( φ_{i} → t_{i} | i ∈ I ) unwinds in a structure M if there is a finite approximation S̃ of S, i.e. S̃ = ( φ_{i} → t_{i} | i ∈ J ) where J is a finite subset of I, such that S̃^{M} = S^{M}. A structure M has the unwind property for a class S of eds’s (or a class P of program schemes) if every S ∈ S (or every S ∈ eds(P)) unwinds in M.

We define a particular first-order structure N with universe ω, based on the dag B of Section 4. We set:

N = ⟨ω, =, g, 0⟩

3Our analysis is easily generalized to any program scheme with any finite number of input and output variables, not necessarily identical. Input and output variables are always ground variables; depending on the class of program schemes, higher-order variables may also be used but only during execution.

where g : ω × ω → ω is the function:

g(m, n) = \{ \begin{matrix}n + 1, & if m = ⌊n/2⌋, \\ 0, & otherwise. \end{matrix}

The correspondence between N and B is the following. For all natural numbers m, n, and p, if p ≠ 0 then g(m, n) = p iff there is an arrow from m to p and an arrow from n to p.

Using the correspondence between N and B, Lemma 3, and the simulation of “memory locations” by “pebbles”, the following is a straightforward result.

Lemma 8 N has the unwind property for BOUNDED-EDS.

Proof: Let S ∈ BOUNDED-EDS and S = ( φ_{i}(x) → t_{i}(x) | i ∈ I ). Assume I is infinite, otherwise the lemma is trivial. Let T be the following set of first-order terms:

T = { t_{i}(x) | i ∈ I } ∪ { u(x) | u(x) appears in φ_{i}(x), i ∈ I } .

Because S uses bounded space, there is n ⩾ 1 such that pebble(t) ⩽ n for every t ∈ T. Given an arbitrary a ∈ ω, define the set T^{N} (a) = { t^{N} (a) | t ∈ T } ⊆ ω. We view dag(t) as prescribing the moves of a (finite) n-pebble game, where the initial configuration contains a single node (the value assigned to x); these are the moves (not necessarily unique) required to reach the output node of dag(t) with at most n pebbles. By Lemma 3 and the correspondence between N and B, the size of T^{N} (a) is finite and independent of a, namely

|T^{N} (a)| ⩽ N({a}, α(n)) ⩽ 2α(n) + 2 .

(Review the definition of N(C, k) in Section 4 to understand the factor 2 in “2α(n)”.) Put differently, because B is uniformly locally finite w.r.t. bounded space, at most 2α(n) nodes are reached in the n-pebble game played according to dag(t), for all t ∈ T and all initial configuration C = {a}. As there are finitely many non-isomorphic partial substructures of N of size ⩽ 2α(n), the desired conclusion follows. (We say “partial” substructures because we do not require that their universe be closed under the function g.) Q.E.D.

Theorem 9 There is an eds Ŝ ∈ EDS not equivalent to any S ∈ BOUNDED-EDS over N.

Proof: By Lemma 8, it suffices to define an eds Ŝ that does not unwind in N. Let t_{0}, t_{1}, t_{2}, … be an infinite sequence of closed first-order terms such that t_{0}^{N} = 0, t_{1}^{N} = 1, t_{2}^{N} = 2, etc. The desired Ŝ is ( x = t_{i} → t_{i+1} | i ∈ ω ). Ŝ^{N} defines the successor function on ω. Q.E.D.

Theorem 9 generalizes the Paterson-Hewitt result, which says that the class FC of flowchart schemes is strictly weaker than the class REC of recursive schemes. If P ∈ FC then eds(P) ∈ BOUNDED-EDS and, therefore, P unwinds in N. On the other hand, it is a straightforward programming exercise to write a R ∈ REC such that R^{N} computes the successor function on ω and, therefore, R does not unwind in N.^{4}

The analogue of the Paterson-Hewitt result for logics of programs appeared in [18] and [2, 3], which asserts that the “first-order logic of FC” is less expressive than the “first-order logic of REC”.

If P is a class of program schemes, the “first-order logic of P” is denoted by L(P). Briefly, L(P) is conventional first-order logic to which we add a construct ⟨P ⟩θ with the meaning that “there is an execution of program scheme P ∈ P after which the assertion θ holds”. Hence, the symbols of L(P) are the usual symbols of first-order logic (including function symbols, relation symbols, equality, quantifiers, etc.) in addition to the modal operator ⟨ ⟩ and the symbols of the programming formalism P. (Another modal operator [ ] is usually considered also, but we can take [ ] as an abbreviation for ¬⟨ ⟩¬, just as ∀ is an abbreviation for ¬∃¬.) Further details on “logics of programs” can be found in [5] and [8].

Let P and P′ be classes of program schemes. We say that the logic L(P) is reducible to the logic L(P′), in symbols L(P) ⩽ L(P′), iff for every formula θ in L(P) there is a formula θ′ in L(P′) such that θ and θ′ are equivalent in all interpretations. We write L(P) < L(P′) if L(P) ⩽ L(P′) and L(P′) ⩽̸ L(P).

The preceding definitions extend in the obvious way to classes of eds’s. The logics L(EDS) and L(BOUNDED-EDS) are therefore well-defined, and it is meaningful to compare them.

Theorem 10 L(BOUNDED-EDS) < L(EDS), i.e. L(BOUNDED-EDS) is strictly less expressive than L(EDS).

Proof: Since EDS (as well as BOUNDED-EDS) is closed under substitution, it is a trivial exercise to write an eds that uses the eds Ŝ of Theorem 9, namely ( x = t_{i} → t_{i+1} | i ∈ ω ), and defines the addition relation x + y = z in N. Similarly, multiplication in N is definable by an eds. As a matter of fact, all these eds’s are very simple. Clearly then, the relations definable by the logic L(EDS) in N are exactly the arithmetical relations (we have shown the “at least” part, which is sufficient for our argument, but the other direction is simple too using the fact that, by definition, every eds is a r.e. sequence of guarded commands).

On the other hand, because every S ∈ BOUNDED-EDS unwinds in N, every formula of the logic L(BOUNDED-EDS) is equivalent to a first-order formula in N. Moreover, 0 and 1 are firstorder definable (trivially) in the structure ⟨ω, =, +, succ, 0⟩ of Presburger arithmetic, and so is our function g : ω × ω → ω, because

g(x, y) = z ⟺ ( (x + x = y ∨ x + x = y + 1) ∧ y + 1 = z )

Hence, the relations that are first-order definable in our structure N are also definable in Presburger arithmetic, and these do not include all arithmetical relations. Q.E.D.

4Such a recursive scheme R is given in Section 3 of [7], where it is called SUCC.

7 Conclusion

Theorem 10 is our version of the Tiuryn-Erimbetov theorem. It implies several well-known results in first-order dynamic logic, such as Rec-DL > CF-DL, Array-DL > DL, Random-DL > DL, and the deterministic version of each of these inequalities. These results follow from the fact that the schemes used in DL or CF-DL have only finitely many memory locations each, and can therefore be simulated by pebble games with finitely many pebbles. While leading to the same results, our analysis is significantly shorter and more straightforward.

Our definition of a guarded command allows quantifier-free formulas only. Allowing arbitrary first-order formulas to appear in guarded commands leads to the definition of “elementary EDS”, or EEDS. The bounded-space version of this class, BOUNDED-EEDS, imposes a bound on the quantifier-depth of formulas, in addition to bounding the pebble complexity of terms. These classes are somewhat exotic, as it is questionable whether they continue to reflect intuition of effective computations.

Nonetheless, all our results, including Theorem 10, can be proved for elementary schemes and logics. For instance, to prove Lemma 8, observe that in a first-order formula of pebble complexity n, each quantifier can be bounded by the distance 2α(n) from the preceding variables. Therefore, any bounded-space elementary eds, with a bound k on quantifier-depth, is equivalent to a boundedspace eds (already quantifier-free) with 2kα(n) new free variables under a substitution that replaces the new free variables with expressions of the form x + i or x − i, for some old free variable x and a constant i ⩽ 2kα(n). This new eds unwinds in N, and this implies that our original elementary eds does.

References

[1] Ben-Or, M., and Cleve, R., “Computing algebraic formulas using a constant number of registers”, Proc. of 20-th ACM Symp. on Theory of Computing, pp 254–257, May 1988.

[2] Erimbetov, M.M., “On the expressive power of programming logics”, in Research in Theoretical Programming (M.A. Taitslin, Ed.), pp 49–68, Alma-Ata, 1981 (in Russian).

[3] Erimbetov, M.M., “A fragment of a logic with infinite formulas”, in Research in Theoretical Programming (M.A. Taitslin, Ed.), pp 30–48, Alma-Ata, 1981 (in Russian).

[4] Dijkstra, E.W., A Discipline of Programming, Prentice Hall, 1976.

[5] Harel, D., First-Order Dynamic Logic, LNCS, 68, Springer-Verlag, 1979.

[6] Kalyasundaram, B., and Schnitger, G., “On the power of white pebbles”, Proc. of 20th ACM Symp. on Theory of Computing, pp 258–266, May 1988.

[7] Kfoury, A.J., “Definability by programs in first-order structures”, Theoretical Computer Science, 25, pp 1–66, 1983.

[8] Kfoury, A.J., Stolboushkin, A.P., and Urzyczyn, P., “Some open problems in the theory of program schemes and dynamic logics”, Russian Mathematical Surveys, 44:1, pp 43–68, 1989. (English transl. of Russian original)

[9] Kozen, D., “Pebblings, edgings, and equational logic”, Proc. 16th ACM Symp. on Theory of Computing, pp 428–435, 1984.

[10] Kozen, D., and Tiuryn, J., “Logics of Programs”, in Handbook of Theoretical Computer Science, Vol. B, Formal Methods and Semantics, ed. J. van Leeuven, Elsevier Science Publ. and The MIT Press, pp 789–840, 1990.

[11] I.Kh. Musikaev and M.A. Taitslin, “Limitations of the program memory and the expressive power of dynamic logics”, Information and computation, 103:2, pp 195–203, 1993.

[12] Paterson, M.S., and Hewitt, C., “Comparative schematology”, MIT A.I. Lab Technical Memo No. 201 (also in Proc. of Project MAC Conference on Concurrent Systems and Parallel Computation), 1970.

[13] Pippenger, N., “Pebbling with an auxiliary pushdown”, J. Computer and System Sciences, 23, pp 151–165, 1981.

[14] Pippenger, N., “Advances in Pebbling”, Proc. of 9th ICALP, LNCS no. 140, Springer-Verlag, 1982.

[15] Salomaa, A., “On the index of a context-free grammar and language”, Information and Control, 14, pp 474–477, 1969.

[16] Salomaa, A., Formal Languages, Academic Press, 1973.

[17] Savage, J., and Vitter, J., “Parallelism in space-time tradeoffs”, Proc. of International Workshop on VLSI: Algorithms and Architecture, Amalfi, Italy, 1984.

[18] Tiuryn, J., “Unbounded program memory adds to the expressive power of first-order programming logic”, Information and Control, 60, nos. 1-3, pp 12–35, 1984. (An earlier version appeared in Proc. of 22nd Symp. on Foundations of Comp. Science, 1981.)

[19] Tiuryn, J., “Implicit definability of finite binary trees by sets of equations”, in Logic and Machines: Decision Problems and Complexity, eds. Börger, Hasenjaeger, and Rödding, pp 320–332, LNCS no. 171, Spinger-Verlag, 1981.