BRICS RS-01-46 L. Kristiansen: The Implicit Computational Complexity of Imperative Programming Languages BRICS

Basic Research in Computer Science

The Implicit Computational Complexity of Imperative Programming Languages

Lars Kristiansen

BRICS Report Series RS-01-46 ISSN 0909-0878 November 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Lars Kristiansen.

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/46/

The Implicit Computational Complexity of Imperative Programming Languages

Lars Kristiansen^{∗}.

Preface

This report presents research conceived during a few months the fall 2001 when I was visiting BRICS at the University of Århus. I would like emphasise the preliminary character of the report. So please forgive me all the inaccuracies, the unpolished presentation, the lack of references and acknowledgements, the sketchy proofs and the outright errors that might be there. The aim is to quickly communicate some ideas and results before I continue the work in a more comfortable and pleasant pace, either on my own or in cooperation with others. I would like to thank The Faculty of Engineering at Oslo University College, BRICS, and in particular Ulrich Kohlenbach, for supporting my research. I would like to thank Ivar Rummelhoff for comments on the manuscript. Finally I would like to thank Karl-Heinz Niggl for numerous inspiring discussions.

Lars Kristiansen Århus, November, 2001

∗Oslo University College, Faculty of Engineering.

e-mail:larskri@iu.hio.no, home page:http://www.iu.hio.no/~larskri/ I dedicate this research to Jasmina Reza.

Abstract

During the last decade Cook, Bellantoni, Leivant and others have developed the theory of implicit computational complexity, i.e. the theory of predicative recursion, tiered definition schemes, etcetera. We extend and modify this theory to work in a context of imperative programming languages, and characterise complexity classes like P, linspace, pspace and the classes in the Grzegorczyk hiearchy. Our theoretical framework seems promising with respect to applications in engineering.

1 Preliminaries

We assume some basic knowledge about subrecursion theory, in particular about the Grzegorczyk hierarchy. Readers unfamiliar with these subjects are referred to Grzegorczyk [9], Rose [29], Odifreddi [26] or Clote [6]. We summarise some basic definitions and facts from Rose. For unary functions f, f^{k} denotes kth iterate of f, that is, f^{0}(x) = x and f^{k+1}(x) = f(f^{k}(x)). The sequence E_{1}, E_{2}, E_{3}, … of number-theoretic functions is defined by E_{1}(x) = x^{2} + 2 and E_{n+2}(x) = E_{n+1}^{x}(2). We have the following monotonicity properties: x + 1 ≤ E_{n+1}(x), E_{n+1}(x) ≤ E_{n+1}(x + 1), E_{n+1}(x) ≤ E_{n+2}(x) and E_{n+1}^{t}(x) ≤ E_{n+2}(x + t) for all n, x, t. A function f is defined by bounded (limited) recursion from functions g, h, b if f(x⃗, 0)=g(x⃗), f(x⃗, y + 1)=h(x⃗, y, f(x⃗)), and f(x⃗, y) ≤ b(x⃗, y) for all x⃗, y. The nth Grzegorczyk class E^{n}, n ≥ 2, is the least class of functions containing the initial functions zero, successor, projections, maximum and E_{n−1}, and is closed under composition and bounded recursion. The 0th Grzegorczyk class E^{0} is the least class of functions containing the initial functions zero, successor, projections and is closed under composition and bounded recursion. The 1st Grzegorczyk class E^{1} is the least class of functions containing the initial functions zero, successor, projections, addition and is closed under composition and bounded recursion. By Ritchie [28] the class E^{2} characterises the class linspacef of functions computable by a Turing machine in linear space; E^{3} equals the Kalmárelementary functions (cf.[29]). Every f ∈ E^{n} satisfies f(x⃗) ≤ E_{n−1}^{k}(max(x⃗)) for a fixed number k. Thus, every function in E^{2} is bounded by a polynomial, and E_{n} ∉E^{n}, showing that each E^{n} is a proper subset of E^{n+1}. Every f ∈ E^{0} satisfy f(x_{1}, …, f_{k}) ≤ x_{i} + k for some fixed numbers k and i (where 1 ≤ i ≤ k), every f ∈ E^{1} satisfy f(x⃗) ≤ k max(x⃗) + l for some fixed numbers k and l. Thus, we also have E^{0} ⊂ E^{1} ⊂ E^{2}. The union of all the Grzegorczyk classes is identical to the set of primitive recursive functions. If F is a class of functions, F_{⋆} denotes the corespondent relational class, i.e.

F_{⋆} = {f | f ∈ F and ran(f) = {0, 1}} .

The class E^{i+1} contains a universal function for the class E^{i} whenever i ≥ 2. Thus, we have E_{⋆}^{i} ⊂ E_{⋆}^{i+1} for i ≥ 2. It is not known whether any of the inclusions E_{⋆}^{0} ⊆ E_{⋆}^{1} ⊆ E_{⋆}^{2} are strict. See e.g. Rose [29] or Kutylowski [14].

Functions f_{1}, …, f_{k} are defined by simultaneous recursion from g_{1}, …, g_{k} and h_{1}, …, h_{k} if f_{i}(x⃗, 0)=g_{i}(x⃗) and f_{i}(x⃗, y+1)=h_{i}(x⃗, y, f_{1}(x⃗, y), …, f_{k}(x⃗, y)) for i = 1, …, k. If in addition each f_{i} is bounded by a function b_{i}, that is, f_{i}(x⃗, y) ≤ b_{i}(x⃗, y) for all x⃗, y, then f is said to be defined by bounded simultaneous recursion from g_{1}, …, g_{k}, h_{1}, …, h_{k}, b_{1}, …, b_{k}. Note that for i = 1 the definition scheme for bounded simultaneous recursion degenerates to the scheme for bounded recursion. Hence every class closed under bounded simultaneous recursion is also closed under bounded recursion, but not necessarily vice versa. While each class E^{n+2} is closed under bounded simultaneous recursion, one application of unbounded simultaneous recursion from functions in E^{n+2} yields functions in E^{n+3}. We also assume some familiarity with complexity-theoretic classes like P (the class of problems decided by a Turing machine working in polynomial time in the length of input), linspace (the class of problems decided by a Turing machine working in linear space in the length of input), pspace (the class of problems decided by a Turing machine working in polynomial space in the length of input), conspace (the class of problems decided by a Turing machine which working in constant space). We use pf, linspacef and pspacef denotes the correspondent classes of functions. On some occasions we view these classes as classes a of number theoretic functions, i.e. functions from tuples of natural numbers into the natural numbers, on other occasions we view these classes as classes of functions from tuples of words over an alphabet into the words of an alphabet. The readers not familiar with these classes should consult e.g. Odifreddi [26]. We will use informal Hoare-like sentences to specify or reason about imperative programs, that is, we will use the notation {A} P {B}, the meaning being that if the condition given by the sentence A is fulfilled before P is executed, then the condition given by the sentence B is fulfilled after the execution of P. For example, {X⃗ = w⃗} P {X⃗ = w′} reads as if the data w⃗ are stored in the registers (or variables) X⃗, respectively, before the execution of P, then data w′ are stored in X⃗ after the execution of P. Another typical example is {X⃗ = w⃗} P {|X_{1}| ≤ f_{1}(|w⃗|), …, |X_{n}| ≤ f_{n}(|w⃗|)} meaning that if the data w⃗ are stored in the registers X⃗, respectively, before the execution of P, then the data stored in X_{i} after the execution of P has a length bounded by f_{i}(|w⃗|). Here f_{i} is function with range ℕ, and |w⃗| abbreviates as usual the list |w_{1}|, …, |w_{n}|. As usual |x| denote the length of the data x.

We use V(P) to denote the set of variables occurring in a program P. A program P computes a functions f when {X⃗ = x⃗}P{Y = f(x⃗)} for some X⃗, Y ∈ V(P). If {X⃗ = x⃗}P{Y = f(x⃗)} we will also occasionally refer to f as the function P computes into Y. This is a slightly sloppy use of words since P might very well compute many functions into Y, e.g. if Z ∈ V(P) and Z ∉ {X⃗} then we also have {X⃗ = x⃗, Z = z}P{Y = g(x⃗, z) = f(x⃗)} for some function g. When we construct programs, we occasionally need what we call fresh variables. That a variable is fresh simply means that the variable is not used elsewhere. Let P and Q be imperative programs where the registers holds values of ℕ. Assume (P) ⊆ (Q), say V(P) = X and V(Q) = X⃗, Y⃗. We say that Q is a bound on P, denoted P ≪ Q, if

{X⃗ = x⃗} P {X⃗ = z⃗} and {X⃗ = x⃗, Y⃗ = y⃗} Q {X⃗ = u⃗} implies x⃗ ≤ u⃗.

2 Introduction

Implicit computational complexity theory can be viewed as theory on how to design programming languages that capture complexity classes. There are of course much more to implicit computational complexity than this, e.g. proof theoretical aspects, philosophical aspects, etcetera. We are talking about a broad and rich research area, but still, if we should explain the area to a layman or an engineer, it would not be too misleading to say that this is an area where we search for programming languages that captures complexity classes. The engineer would probably respond that this seems like a worthy endeavour, and then he^{1} would expect us to come up with a nice practical programming language which he can use in his daily work. If we view the formalisms developed in Bellantoni-Cook [1], Leivant [17], and several other entries in the bibliography, as programming languages, we do not have exactly what an engineer conceives as practical programming languages. He would probably have problems to carry out simple tasks, like multiplying two numbers, in any of these formalisms. What would be the most precious gift implicit computational complexity theory possibly could give to an engineer? Well, perhaps we could give him a neat practical programming language reminiscent of Pascal or C, a language which permits him to write programs more or less in way he is used to, but still a language which endows him with means to easily retrieve useful information about the computational complexity of the programs. The language should be rich and able to express as many algorithms as possible, also algorithms of high computational complexity because sometimes the engineer indeed wants to implement such algorithms. (He makes sure that such programs only are executed on inputs they can cope with.) Will there ever be possible to provide such a language which engineers actually will use, either to develop programs that compiles into executable code on some electronic gadgets, or as a pen and paper language for analysing algorithms before they eventually are implemented by other means? As we will see, there are theoretical results and mathematical insights that put obstacles in the way of such a programming language, in spite of these results and insights we are able to present a theoretical framework which seems promising for developing languages satisfying the needs and requirements of engineering. The main ideas are simple: We introduce programming languages capable of computing a huge class of functions e.g. every primitive recursive functions. We introduce measures on programs.

1We assume that women do not exist.

Definition 2.1. Given any programming language L, a measure on L is a computable function π: L-programs → ℕ. We say that the program P has π-measure n if π(P) = n. End of definition.

The idea is that a measure should tell us something about the computational complexity of a program, for example, if P has π-measure 0, then every function computed by P is in the complexity class C where C might be pf, linspacef, the Kalmár elementary functions, or any other complexity class. One might ask how successful such a project can be. Is it for for example possible to find a nontrivial programming language and a measure π such that every program with polynomial running time (and only programs with polynomial running time) will receive π-measure 0? Unfortunately, the answer to this question is not an unqualified yes, it depends on what we mean by a nontrivial programming language. By ordinary computability-theoretic methods we shall prove some negative results. Thereafter we shall see that the situation is not as bad as these results may indicate at the first glance. We start off by defining some generic languages.

Definition 2.2 (Loop programs). We have an infinite supply of program variables (registers). We will normally use X, Y, Z, A, B, C, U, V with or without subscripts and superscripts to denote variables. For any variables X and Y we have the following imperatives (primitive instructions): nil(X), suc(X),

pred(X), X:= Y.

A loop language is a set of programs generated by the following syntactical rules:

• every imperative is a program

• if P is a program with no occurrence of the variable X in an imperative, then the loop loopX[P] is a program

• if P_{1}, P_{2} are programs, then the sequence P_{1};P_{2} is a program

L_{0} is the loop language which only has the imperative suc(X) (for any variable X). L_{1} is the loop language which has the imperatives suc(X) and X:= Y (for any variables X and Y). L is the loop language which has the imperatives nil(X), suc(X), pred(X) and X:= Y (for any variables X and Y). Loop programs have a standard semantics, e.g. like Pascal or C programs. The imperative nil(X) sets the register X to zero. The imperative suc(X) increments the number stored in X by one, while pred(X) decrements any nonzero number stored in X by one, X:= Y is ordinary assignment. Imperatives and loops in a sequence are executed one by one from the left to the right. The meaning of a loop statement loop X[P] is that P is executed x times whenever the number x is stored in X, besides, X keeps the value x during the execution of the loop body P. End of definition. Example 2.3. If a variable X governs a loop, then X cannot occur in an imperative in the body of the loop. Still X is allowed to govern a loop in the body. The following L-program square the number stored in the register X.

   {X = x} nil(Y); loop X [ loop X [ suc(Y) ] ]; X:= Y {X = x^{2}}

End of example. Definition 2.4. Let P be a program in a loop language and let C be a complexity class. P is C-feasible if every function computed by P is in C. P is honestly C-feasible if every subprogram of P is C-feasible. P is dishonestly C-feasible, or C-dishonest for short, if P is C-feasible, but not honestly C-feasible. Whenever convenient we will leave out the reference to a particular complexity class and talk about feasible programs, honestly feasible programs, etcetera. End of definition.

Note that if a function is computable by a feasible program, then it is also computable by an honestly feasible program. C-dishonest programs fall into two groups. One group consists of those programs which only compute functions in C, but the execution of the program require more resources than the complexity class C admits. The other group consists of programs which always are executed within the resource bounds C admits, but some subprograms exceed these bounds if executed separately. Typical of the latter group are programs of the form R;if<test>[Q] where R is an honestly C-feasible program, <test> is a test that always fails, and Q is an arbitrary program which is not C-feasible. Another example is a program of the form P;Q where Q runs in time O(2^{x}), but where P is an honestly pffeasible program which assures that Q always is executed on ”logarithmically large input”. The program P;Q is dishonestly pf-feasible. Obviously, we cannot expect to separate (by purely syntactical means) the feasible programs from the non-feasible ones if we take into account dishonest programs. Thus, it seems reasonable to restrict our discussion to the honestly feasible programs, and after all, it is the computational complexity inherent in the code we really want to analyse and recognise. But even then, our project is bound to fail. Definition 2.5. Let C be a complexity class, let C be a programming language, and let π be a measure on C. The pair (π, C) is called

• C-sound if every C-program with π-measure 0 is C-feasible,

• C-complete if every honestly feasible C-program has π-measure 0, and

• C-adequate if every function in C can be computed by a C-program with π-measure 0.

End of definition.

Note that if we have a pair (π, C) which is both C-sound and C-adequate, we have a characterisation theorem for the class C, i.e. f ∈ C iff f can be computed by a C-program with π-measure 0. Now, let us restrict our discussion to the linear space computable functions for a while, i.e. the Grzegorczyk class E^{2}. (Recall that E^{2} = linspacef.)

Theorem 2.6. Let C be any programming language extending L_{0}, and (π, C) be a E^{2}-sound and E^{2}-adequate pair. Then (π, C) is E^{2}-incomplete, that is, there exists an honestly E^{2}-feasible program P ∈ C such that π(P) > 0.

Proof. Assume a effective enumeration {ρ_{i}}_{i∈ω} of the Turing machines with alphabet {0, 1}. Let n be a fixed natural number. It is well-known that there is a function f_{n} in E^{2} satisfying f_{n}(x) = 1 if ρ_{n} (on the empty input) halts within x steps, and f_{n}(x) = 0 else. It is also well-known that it is undecidable whether ρ_{i} halts. Since (π, C) is adequate and sound, there is an honestly feasible program Q ∈ C with π-measure 0 such that

{Y = y} Q {if ρ_{n} does not halt within y steps then Z = 0 else Z = 1}

Moreover, such a program Q can be effectively constructed from n, that is, there exists an algorithm for constructing Q from n. Since C extends L_{0}, the program

             P :≡ loopX[Q;loopZ[loopV[suc(W)]];
                             loopW[suc(V)]]

is also in C, where X, V, W are fresh variables. Now, if ρ_{n} never halts then loop V[suc(W)] will never be executed, whatever the inputs to P. Thus, if ρ_{n} never halts, then P is honestly feasible. In contrast, if ρ_{n} halts after s steps, say, then part loop V[suc(W)] and part loop W[suc(V)] will be executed each time the body of the outermost loop is executed whenever Y = y ≥ s. Each such execution implies that the number stored in the register V is at least doubled, and then the function computed into V is not in E^{2}. (For any f ∈ E^{2} we have f(x⃗) ≤ q(x⃗) for some polynomial q, but the function computed into V cannot be bounded by a polynomial.) Thus, if ρ_{n} eventually halts, then P is not feasible. In other words, P is honestly feasible if and only if ρ_{n} never halts. As P is effectively constructible from n, we conclude that (π, C) cannot be complete. For if (π, C) were complete, then ρ_{n} would never halt if and only if π(P) = 0. This would yield an algorithm which decides whether ρ_{n} halts: Construct P from n and then check whether ν(P)>0. Such an algorithm does not exist.

Theorem 2.6 regards loops languages and the linear space computable functions, but similar theorems can be proved for any other interesting programming languages and complexity classes. So, maybe it will be wise to put an end to our project then? In a way we have lost before we even started. Still, we will continue our research project since we belive we can achieve completeness in practice. For a significant amount of natural programs, and in particular for programs that actually will be written for commercial and industrial purposes, we belive we can find sound and complete measures for interesting complexity classes, that is measures when applied on such natural programs always yield the the best possible answers. Moreover, for sound and adequate pairs (π, C) there might be possible to prove that the measure π is complete for an interesting sublanguage C′ of C. This type partial completeness results (or lack of such results) will give a mathematical indication of how well (or bad) we are doing.

3 The μ-measure and some fundamental definitions.

Note 3.1. In the previous section we defined the loop languages L_{0}, L_{1} and L. Any program in any of these languages can be written uniquely in the form P_{1};…;P_{k} such that each P_{i} is either a loop or an imperative, and where k = 1 whenever P is an imperative or a loop. End of note.

Definition 3.2. The relations ≺P and \underrightarrow{P} are binary relations over V(P). The relation X ≺P Y holds iff P has a subprogram loop X [Q] where suc(Y) is a

subprogram of Q. The relation \underrightarrow{P} is the transitive closure of ≺P. We call \underrightarrow{P} the control relation (of P), and if X ≺P Y we say that X controls Y. α is a clique of degree 1 in the program P iff α is a minimal subset of V(P) satisfying

(i) there is a 1-principal variable in α, where a variable X is 1-principal iff

     X\underrightarrow{P}X

(ii) if X is a 1-principal variable in α and X\underrightarrow{P}Y, then Y ∈ α.

Let α be a clique (of any degree) in the program P. The cover set α̂ ⊂ V(P) of the clique α is defined by α̂ = {X | X ≺P Y for every Y ∈ α}. α is a clique of degree n + 1 in the program P iff α is a minimal subset of V(P) satisfying

(i) there is a n + 1-principal variable in α, where a variable X is n + 1principal when there exists a clique β of degree n in P such that X ∈ β̂ and Y\underrightarrow{P}X for some Y ∈ β (ii) if X is a n + 1-principal variable in α and X\underrightarrow{P}Y, then Y ∈ α.

We define the μ-measure μ(P) of an L_{0}-program P by

• μ(suc(X)) = 0 for every variable X.

• Let P ≡ Q_{1};Q_{2}. Then μ(P) = max(μ(Q_{1}), μ(Q_{2})).

• Let P ≡ loopX[Q]. Then

μ(P) = \{ \begin{matrix}μ(Q) + 1 & if Q has a clique of degree μ(Q) + 1, \\ μ(Q) & otherwise \end{matrix}

End of definition.

We shall elucidate Definition 3.2 by some examples and explanations. Let μ(P) = n > 0. The functions computed by P which are not in the Grzegorczyk class E^{n+1} will be precisely those functions computed into the variables in the n-cliques of P, i.e. if {X⃗ = x⃗}P{Y = f(x⃗)} and Y ∈ α for some n-clique α of P, then f ∉ E^{n+1} (but f ∈ E^{n+2}). Let P_{0} be the program

               loop A [suc(B)]; loop B [suc(A)]

The μ-measure of P_{0} is 0, so every function computed by P_{0} is in E^{2}. There is one 1-clique α in P_{0}, namely α = {A, B}. The cover set α̂ of α is empty. We put P_{0} inside loop controlled by a variable X and get the program

       P_{1} ≡ loop X [ loop A [suc(B)]; loop B [suc(A)] ]

Then we have μ(P_{1}) = 1 since the body of the outermost loop has μ measure 0 and contains a 1-clique. Still there is only one clique in the program, namely the 1-clique α = {A, B}, but the cover set of α is not empty anymore. Now we have α̂ = {X}. The functions computed by P_{1} into A, B are not in E^{2} whereas the function computed into X is in E^{2}. We have

{A = a, B = b, X = x} P_{0} {A = f(a, b, x), B = g(a, b, x), X = x}

and the reader can check that neither f nor g is bounded by a polynomial, thus neither f nor g is in E^{2}. We extend the body of the outermost loop in P_{1} and get the program P_{2} ≡

loop X [ loop A [suc(C)];
         loop A [suc(B)];
         loop B [suc(A)];
         loop U [suc(V)] ]

Still we have only one 1-clique α, but now the variable C is also in the clique, i.e. α = {A, B, C}. We still have α̂ = {X}. Note that the value the program computes into C cannot be bounded by a polynomial in the input since the value the program computes into A is not bounded by such a polynomial. Thus the functions computed into C are not in E^{2}. The function computed into U and V are in E^{2}, e.g. we have

{X = x, U = u, V = v} P_{2} {V = v + (x × u)} .

Let us study the program

              Q_{0} ≡ loop Y [ P_{2};loop V [suc(U)] ] .

The μ measure of Q_{0} is also 1, but here we find two cliques of degree 1, the clique α = {A, B, C} and the clique β = {U, V}. Further, we have the cover sets α̂ = {X, Y} and β̂ = {Y}. Now, if we extend the body of the outermost loop of Q_{0} such that we get the program

       Q_{1} ≡ loop Y [P_{2};loop V [suc(U)]; loop A [suc(X)]]

then we have a program with μ-measure 2. Why? Well, in the body of the outermost loop of Q_{1}, i.e. in the program

              P_{2};loop V [suc(U)]; loop A [suc(X)]

we find the 1-clique α = {A, B, C} and the cover set α̂ = {X}. (This clique is inside P_{2}.) Besides, we see that A controls X since the subprogram

                       loop A [ suc(X) ]

is a part of the body. So, a variable (A) in a 1-clique (α) controls a variable (X) in the cover set (α̂) of the 1-clique, and hence there is a clique γ of degree 2 in the body. Thus, the program Q_{1} has μ measure 2. The sole principal variable of γ is X and every variable X controls, and no other variable, should be in γ, i.e. γ = {A, B, C, X, V}. The cover set of γ in Q_{1} contains only one variable. We have γ̂ = {Y}. The functions the program Q_{1} computes into the variables in γ will be hyper exponential, i.e. they will not be bounded by any Kalmár elementary function.

Definition 3.3. Let V(P) = X⃗. We use #P(x⃗) to denote the number of steps in the execution of the imperative program P on the input X⃗ = x⃗, i.e. the number of primitive imperatives which is executed. Let π be a measure and let C be a loop language. We say that the pair (π, C) is sound (with respect to the Grzegorczyk hierarchy) when

π(P) ≤ n ⇒ #P ∈ E^{n+2}

for every n ∈ ℕ and every P ∈ C. We say that the pair (π, C) is complete (with respect to the Grzegorczyk hierarchy) when

#P ∈ E^{n+2} ⇒ π(P) ≤ n

for every n ∈ ℕ and every P ∈ C. We say that the pair (π, C) is adequate (with respect to the Grzegorczyk hierarchy) when every function in E^{n+2} can be computed by a C-program with π-measure ≤ n (for every n ∈ ℕ). End of definition.

4 Soundness and completeness of (μ, L_{0})

Definition 4.1. We say that a loop loop X [Q] with μ-measure n+1 is simple if Q has μ-measure n. A program P_{1}; …;P_{k} with μ-measure n+1 is flattened out if each component P_{i} either is a simple loop or has μ-measure strictly less than n + 1, i.e. μ(P_{i}) ≤ n. End of definition.

For any program P in L_{0} we have {X = x}P{X ≥ x}. This entails a lot of monotonicity properties for programs in L_{0}, for instance, if Q_{0} ≪ Q_{1}, then we also have R_{0};Q_{0};R_{1} ≪ R_{0};Q_{1};R_{1} . Such monotonicity properties of L_{0} will be used frequently in the sequel, and in particular in the proof of the next lemma.

Lemma 4.2 (Flattening lemma). Let P be an L_{0}-program such that μ(P) > 0. Then there exists a flattened out L_{0}-program P′ such that

- P′ is flattened out

- P ≪ P′

- μ(P′) ≤ μ(P).

Proof. We define the rank of a loop P denoted rk(P) by

rk(P) =\{ \begin{matrix}0 & if μ(P) = 0 \\ k & otherwise \end{matrix}

where k is the number of times the word loop occurs in P. We will prove (Claim) If the loop P ≡ loop X [Q] is not simple, then there are loops P_{1} and P_{2} such that

(i) rk(P) > rk(P_{1}) and rk(P) > rk(P_{2})

(ii) μ(P) ≥ μ(P_{1}) and μ(P) ≥ μ(P_{2})

(iii) P ≪ P_{1};P_{2}

Let us see how the very lemma follows from (Claim). Let R_{0} ≡ Q_{1}; …; Q_{m} be a program with μ-measure n + 1 which is not flattened out. Then there must be a loop Q_{i} among the components Q_{1}; … Q_{m} such that Q_{i} is not a simple loop and μ(Q_{i}) = n + 1. Clause (iii) of the claim yields loops P_{1} and P_{2} such that and P ≪ P_{1};P_{2}. Let

R_{1} ≡ Q_{1}; …;Q_{i−1};P_{1};P_{2};Q_{i+1}; …;Q_{m} .

Then we have R_{0} ≪ R_{1}. If the program R_{1} is not flattened out, we can use the same procedure once more to get a program R_{2} such that R_{0} ≪ R_{1} ≪ R_{2}. And thus we might proceed, constructing programs R_{1}, R_{2}, R_{3}, … such that R_{0} ≪ R_{i}. The process terminates when we encounter a flattened out program R_{•}. Clause (i) of the claim ensures that we eventually will encounter such a flattened out program. The program R_{i+1} is the program R_{i} where one loop in a sequence of loops (and primitive instructions) is replaced by two loops of strictly lower rank, and thus it follows straightaway from the definition of rank in the beginning of this proof, that the process must terminate. Finally, clause (ii) of the claim ensures that the result of process, i.e. the flattened out program R_{•} has μ-measure less or equal to R_{0}. This proves that the lemma follows from (Claim). We turn to the proof of (Claim). The proofs splits into two cases. The case (1) where Q is a loop loop Y [R] and the case (2) where Q is a sequence Q_{1}; …;Q_{m}.

Case (1). We have P ≡ loop X [loop Y [R]]. Let Z be a fresh variable,

let P_{1} ≡ loop X [loop Y [suc(Z)]. and let P_{2} ≡ loop Z [R]. It is easy to

see that (Claim) holds. Case (2). This is the hard case. We have P ≡ loop X [Q], where Q ≡ Q_{1}; …; Q_{m} for some m ≥ 2. Since P is not a simple loop, we have μ(P) = μ(Q) = n + 1. Thus, there must be a component Q_{i} in Q_{1}; …; Q_{m} such that μ(Q_{i}) = n + 1. Furthermore, Q_{i} has the form Q_{i} ≡ loop Y [R], where R contains an n + 1-clique α and Y ∈ α̂. Now, it must be the case that no

V in the clique α controls Y in the program Q, i.e. we have V \underrightarrow{Q̸} Y for every V ∈ α. If this were not the case, there would be a clique of degree n + 2 in Q, and then the μ-measure P would be n + 2. Let Z be a fresh variable, and let R' be R, where every loop controlled by a variable in the clique α is deleted. Note that since α has degree n + 1, the number of occurrences of the word loop in R' will be strictly less than the number in R. (There is no reason to formalise what it means to delete a loop. Any sensible way of deleting a loop will work. The body of the loop may or may not be deleted.) Let

  P_{1} ≡ loop X [ Q_{0}; . . .;Q_{i−1};loopY[suc(Z); R'];Q_{i+1}; . . .;Q_{k} ] .

When we execute P and P_{1} on the same input, the loop loopY[suc(Z); R'] in P_{1} will be executed exactly as many times as the loop loop Y[R] in P because the variable Y is not controlled by any variable in α. Hence, let

           P_{2} ≡ loop Z [ Q_{0}; . . .;Q_{i−1};R;Q_{i+1}; . . .;Q_{k} ]

and we have P ≪ P_{1}; P_{2}. It is easy to see that we also have rk(P_{i}) < rk(P) and μ(P_{i}) ≤ μ(P) for i = 1, 2. This completes the proof of (Claim).

Theorem 4.3. Every function computed by an L_{0}-program with μ-measure n is in the Grzegorczyk class E^{n+2}.

Proof. We prove the theorem by induction on n. Assume f is computed by a program P with μ-measure 0. Then the program P has the form P_{1}; …;P_{k} (for some k ≥ 1) where no P_{i} contains a clique of degree 1. This entails

that the control relation \underrightarrow{P_{i}} is a partial ordering (for i = 1, …, k). Use induction on this ordering to prove that any function computed by P_{i} is in E^{2}. It follows that any function computed by P is in E^{2}, since E^{2} is closed under composition. (The induction over the partial ordering \underrightarrow{P_{i}} is tedious and contains some unpleasant details, but no big surprises show up and everything is quite straightforward. The reader interested in the details should consult Kristiansen-Niggl [13] where such an induction is used to prove a similar result.) We turn to the induction step. Assume f is computed by a program P with μ-measure n + 1. By Lemma 4.2 there exists a flattened out program P′ such that P ≪ P′ and μ(P′) ≤ n + 1. The program P′ has the form P_{1}; …;P_{k} (for some k ≥ 1) where P_{i} is a simple loop or has μ-measure strictly less than n+1 (for i = 1, …, k). It suffices to prove that each P_{i} only computes functions in E^{n+3}. If P_{i} has μ-measure strictly less than n + 1, it follows straightaway from the inductions hypothesis that P_{i} does not compute functions outside E^{n+3}. If P_{i} is a simple loop, then P_{i} has the form loop X [Q] where μ(Q) = n. By the induction hypothesis every function computed by Q is in E^{n+2}. Any function computed by P_{i} can be defined by one application of simultaneous recursion over functions computed by Q. Hence any function computed by P_{i} is in E^{n+3} since one application of simultaneous recursion over functions in E^{n+2} yields a function in E^{n+3}.

Definition 4.4. We define the sequence of functions K_{0}, K_{1}, K_{2}, … from by K_{0}(x) = 2(x + 1) and K_{n+1}(x) = K_{n}^{x}(0). We say that a Hoare statement {A}P{B} holds almost everywhere if there exists a fixed number k such that {A}P{B} holds whenever all the inputs to the program P is greater or equal to k. We put the tag (a.e) next to a Hoare statement to mark that the statement just is supposed to hold almost everywhere. (A Hoare statement without such a tag is of course supposed to hold for all possible inputs.) End of definition. Example 4.5. Let P be the program loop Z [loop X [suc(Y)]]. We have {X = x}P{Y ≥ x} (a.e) because the statement holds when all inputs is greater or equal to 1. The statement may not be true for inputs where Z = 0.So the statement does not hold for all possible inputs, but it does hold almost everywhere. End of example.

Lemma 4.6. We have K_{n+1} ∉ E^{n+2} for n ∈ ℕ (but we do have K_{n} ∈ E^{n+2}).

Proof. This proof is a standard exercise. We skip the details.

Lemma 4.7. Let P be a loop, and let α be a clique of degree n in P. For every Y ∈ α̂ and X ∈ α we have

{Y = y} P {X ≥ K_{n}(y ^{.} 1)} (a.e)

Proof. We prove this lemma by induction on n. Assume n = 1. (There is no such thing as a 0-clique.) Let α be an arbitrary 1-clique in P and let A be a

principal variable of α and let B ∈ α be such that A \underrightarrow{P} B and B \underrightarrow{P} A. (Such A and B exist when α is a 1-clique.) Let

            Q ≡ loop A [suc(B)]; loop B [suc(A)] .

Then

{A = a, B = b} Q {A = a + b + a ≥^{(a.e)} 2(a + 1) = K_{0}(a)} .

Further, let Q_{1} ≡ loop Y [Q]. Then we have

{Y = y, A = a} Q_{1} {A ≥ K_{0}^{y}(a) ≥ K_{0}^{y}(0) = K_{1}(y)} (a.e)

and if Y is any variable in the cover set α̂ and {Y = y}P{A = a} then a ≥ K_{1}(y). Hence we have {Y = y}P{A ≥ K_{1}(y)}(a.e) for any Y ∈ α̂. Now, A

is a principal variable of α, so if X ∈ α then A \underrightarrow{P} X. It follows that we have {Y = y}P{X ≥ K_{1}(y ^{.} 1)} (a.e) for any X ∈ α and Y ∈ α̂. This concludes the proof for n = 1, and we can turn to the induction step. Let α be any clique of degree n + 1 in the loop P. Then there exists a subprogram P_{0} ≡ loop U [Q] such that μ(Q) = n, μ(P_{0}) = n + 1 and an n + 1-clique α_{0} is in Q. The clique α_{0} is a subclique of α, i.e. α_{0} ⊂ α. Now, Q has the form Q_{1}; …; Q_{m} for some m ≥ 2. Pick a component Q_{i} among Q_{1}; …; Q_{m} such that μ(Q_{i}) = n, and there is an n-clique β in Q_{i} such that

A \underrightarrow{Q} B for some A ∈ β and B ∈ β̂. Such a Q_{i} exists since μ(P_{0}) = n + 1. Furthermore, B is a principal variable for the clique α_{0}. By the induction hypothesis we have

{B = b}Q_{i}{A ≥ K_{n}(b ^{.} 1)} . (a.e)

Let Y be any variable in the cover set α̂ and let P_{1} ≡ loop Y [B:= A; Q_{i}]. (B:= A is ordinary assignment. It does not affect our argument that assignment is not a part of the language L_{0}.) First, we note that

\{Y = y, A = a\}P_{1}\{A ≤ \overline{K}_{n}^{y}(a)\} (a.e)

where \overline{K}_{n}(x) = K_{n}(x ^{.} 1). Further, we note that K_{n}(K_{n}(x) ^{.} 1) ≥ K_{n}(K_{n}(x ^{.} 1)). Hence

\overline{K}_{n}^{y}(a) ≥ K_{n}^{y}(a ^{.} y) ≥ K_{n}^{y}(0) = K_{n+1}(y) .

Altogether this entails that {Y = y}P_{1}{A ≥ K_{n+1}(y)} (a.e). It is easy to see that P_{1} ≪ P, and thus we have proved that {Y = y}P{A ≥ K_{n+1}(y)} (a.e)

holds for any Y ∈ α̂ and the variable A ∈ α. Now, A \underrightarrow{P} B and B is a principal variable of the clique α_{0}. The variable B will control (in P) any variable in the clique α, and thus A controls (in P) any variable in the clique α. Moreover, P is a loop. It follows that {Y = y}P{X ≥ K_{n+1}(y ^{.} 1)} (a.e) for any X ∈ α, Y ∈ α̂.

Theorem 4.8 (Soundness and Completeness of (μ, L_{0})). We have

μ(P) ≤ n ⇔ #P ∈ E^{n+2}

for every n ∈ ℕ and every P ∈ L_{0}.

Proof. Suppose μ(P) ≤ n. Let A be a fresh variable, and let Q be P where each occurrence of an imperative on the form suc(X) is replaced by the program suc(X);suc(A). Let f be the function which Q computes into A, i.e. we have

{X⃗ = x⃗, A = a} Q {A = f(x⃗, a)} .

It is easy to see that Q has μ-measure less or equal n, and thus we have f ∈ E^{n+2} by Theorem 4.3. Now, f(x⃗, a) = a + #P(x⃗). It follows that #P ∈ E^{n+2} Suppose μ(P) > n. Then a subprogram Q of P is a loop containing a clique of degree n + 1. By Lemma 4.7 there will be variables Y and X such that

{Y = y} Q {X ≥ K_{n+1}(y ^{.} 1)} (a.e) .

The function K_{n+1} is not in E^{n+2}. (Lemma 4.6.) It follows that #P cannot be in E^{n+2}, i.e. we have #P ∉ E^{n+2}

The μ-measure introduced above is considerably more sophisticated than a similar measure (also called μ-measure) in Kristiansen-Niggl [13]. The measure in [13] is sound, but not complete, for a language corresponding to L_{0}.

5 The ν-measure and how to deal with assignment

Recall that L_{1} is the language L_{0} extended by the assignment imperative .. := ... An interesting feature of the theory we are developing is that the measures on programs still will be well defined when we extend the language in a natural way. The μ-measure is still well defined for L_{1}, but the next example shows that the pair (μ, L_{1}) is not sound with respect to the Grzegorczyk hierarchy.

Example 5.1. The program

               loop X [ loop Y [suc(Z)]; Y:= Z ]

computes a function into Y which are not bounded by a polynomial, and thus not bounded by any function in E^{2}. (So the number of steps in an execution of the program is not bounded by a function in E^{2} either.) Still the μ-measure of the program is 0. End of example.

So we need a measure ν that makes the pair (ν, L_{1}) sound. We will achieve

ν by redefining the control relation \underrightarrow{P}. In any other respect the ν-measure will be defined exactly as the μ-measure, e.g. the notions of clique, cover set etc. will not be redefined. The naive way to redefine the control relation would be to say that the relation X ≺P Y holds if P has a subprogram loop X [Q] where suc(Y) is a subprogram of Q or if Y:= X is a subprogram of P; and then define the relation \underrightarrow{P} as the transitive closure of ≺P. If we do so, the pair (ν, L_{1}) will certainly be sound, still this solution turns out to be thoroughly unsatisfactory. Example 5.2 shows a natural and innocent little program of very low computational complexity, which receives ν-measure 1 if we assume this naive definition of the control relation. The example speaks for itself, moreover, the naive definition would not enable us to prove several of the theorems in the sequel.

Example 5.2. Let P be the program

loop X [ C:= A; A:= B; B:= C ]

Then we have {X = x, A = a, B = b}P{A = f(x, a, b,)} where f(x, a, b) equals a if x is even and b if x is odd. End of example.

So, how should one define define the control relation ? The next definition shows a way which turns out to be satisfactory.

Definition 5.3. The relations ≺P and \underrightarrow{P} are binary relations over V(P). The relation X ≺P Y holds iff P has a subprogram loop X [Q] where suc(Y) is a subprogram of Q. Let X:=PY denote that X:= Y is a subprogram of P. The

relation \underrightarrow{P} is the smallest relation such that

• if X ≺P Y, then X\underrightarrow{P}Y

• \underrightarrow{P} is transitive

   • if X:=PY and Z\underrightarrow{P}Y, then Z\underrightarrow{P}X

We keep the definitions from 3.2 of principal variable, n-clique and cover set (in P). These notions depends solely on the relations ≺P and \underrightarrow{P}. Finally, we define the ν-measure as we defined the μ-measure, i.e. we define the νmeasure of a program P, denoted ν(P), by

• ν(imp) = 0 for every imperative imp.

• Let P ≡ Q_{1};Q_{2}. Then ν(P) = max(ν(Q_{1}), ν(Q_{2})).

• Let P ≡ loopX[Q]. Then

ν(P) = \{ \begin{matrix}ν(Q) + 1 & if Q has a clique of degree ν(Q) + 1 \\ ν(Q) & else \end{matrix}

End of definition.

A bit informally stated, the ν-measure is the μ-measure with the extension: if X:= Y occur in P, then X inherits all the \underrightarrow{P}-predecessors of Y. The program in Example 5.1 has ν-measure 1, whereas the program in Example 5.2 has ν-measure 0. Everything seems fine, and as we soon will prove, the pair (ν, L_{1}) is indeed sound. Programs in L_{1} do not possess the same nice monotonicity properties as the the programs in L_{0}. E.g. we do not have {X = x}P{X ≥ x} for arbitrary P ∈ L_{1} and X ∈ V(P). The program in Example 5.2 yields a counterexample.

This clutters the proof of soundness for the pair (ν, L_{1}). We will introduce a new loop language L_{M} with convenient monotonicity properties, redefine the measure ν for this language, and then prove that the pair (ν, L_{M}) is sound with respect to the Grzegorczyk hierarchy. It will follow easily that the pair (ν, L_{1}) is also sound. Definition 5.4. Let L_{M} be the loop language with the imperatives suc(X) and X:= max(X,Y) for any variables X and Y. The semantics of the imperative X:= max(X,Y) is indicated by the syntax, i.e. we have {X = x, Y = y}X:= max(X,Y){X = max(x, y), Y = y}. Note that X:= max(Y,Z) is not an imperative of L_{M}. We define the measure ν for L_{M} exactly as we defined ν for L_{1}, except that X:=PY now denotes that X:= max(X,Y) is a subprogram of P. (There is no need to repeat the definition.) End of definition.

Lemma 5.5 (Flattening lemma). Let P be an L_{M}-program such that μ(P) > 0. Then there exists a flattened out L_{M}-program P′ such that

- P′ is flattened out

- P ≪ P′

- ν(P′) ≤ ν(P).

Proof. This lemma is similar to Lemma 4.2. The proofs of the two lemmas are also very similar. First we define “rank” as we did in the proof of 4.2, i.e. the rank of a loop P denoted rk(P) by

rk(P) =\{ \begin{matrix}0 & if ν(P) = 0 \\ k & otherwise \end{matrix}

where k be the number of times the word loop occurs in P. Then we need to prove a claim similar to the claim in proof of 4.2. (Claim) If the loop P ≡ loop X [Q] is not simple, then there exist loops P_{1} and P_{2} such that

(i) rk(P) > rk(P_{1}) and rk(P) > rk(P_{2})

(ii) ν(P) ≥ ν(P_{1}) and ν(P) ≥ ν(P_{2})

(iii) P ≪ P_{1};P_{2} The desired result follows from (Claim) by the same argument we used above. The proof (Claim) is also very similar to the corresponding proof above. The proofs splits into two cases. Case (i) is more or less identical to the corresponding case above. Case (ii) is also similar to the corresponding case above, but an additional argument is required to establish rk(P_{1}) < rk(P). The augment is quite easy: When a program contains a clique (of any degree) there will be a least one loop in the program. (This is obvious, a program which is just a sequence of imperatives cannot have a clique.) The program P_{1} is the program

     loop X [ Q_{0}; . . .;Q_{i−1};loopY[suc(Z); R'];Q_{i+1}; . . .;Q_{k} ]

where the subprogram R' is obtained by removing loops form a certain program R. All loops controlled by the variables in a certain clique in R are removed, so there will be at least one loop to remove. It follows that rk(P_{1}) < rk(P). This concludes the proof of Lemma 5.5.

Theorem 5.6 (Soundness of (ν, L_{1})). We have

μ(P) ≤ n ⇒ #P ∈ E^{n+2}

for every n ∈ ℕ and every P ∈ L_{1}.

Proof. Let P be a L_{1} program with ν-measure n. Obviously there exists a L_{M} program P′ with ν-measure n such that P ≪ P′. By Lemma 5.5 we can assume that P′ is flattened out. Henceforth we can proceed as in the proof of Theorem 4.3, and prove by induction on n that every function computed by an L_{1}-program with ν-measure n is in the Grzegorczyk class E^{n+2}. Thereafter we can proceed as the left-right direction in the proof of Theorem 4.8.

Unfortunately, the pair (ν, L_{1}) is not complete. The program

                P ≡ loop X [ loop A [suc(B)] ]

has ν-measure 0, and thus #P ∈ E^{2} by Theorem 5.6. We expand P to the program Q ≡

loop X
[ loop A [suc(B)]
  C:= A; A:= B; A:= C; (* swap the values of A and B *)
  C:= A; A:= B; A:= C; (* swap the values of A and B *) ]

and get a program with ν-measure 1, but obviously we also have #Q ∈ E^{2}. Thus, the pair (ν, L_{1}) is not complete. On the other hand, the language L_{1} is not adequate, and hence we cannot use the argument in the proof of Theorem 2.6 to prove that no complete measure for L_{1} exist. We have an open problem.

Open problem 5.7. Does there exist a measure π such that the pair (π, L_{1}) is sound and complete with respect to the Grzegorczyk hierarchy?

6 Soundness and adequacy of (ν, L)

Recall that L is the loop language where suc(..), pred(..), nil(..) and ..:= .. are the imperatives. Note that the ν-measure is well defined for L-programs.

Theorem 6.1 (Soundness of (ν, L)). We have

ν(P) ≤ n ⇒ #P ∈ E^{n+2}.

for every n ∈ ℕ and every P ∈ L.

Proof. Assume P ∈ L and ν(P) ≤ n. Let Z be a fresh variable and let P_{0} be P where each occurrence of a an imperative imp is replaced by imp; suc(Z). Let P_{1} ≡ nil(Z);P_{0}. It is easy to see that ν(P_{1}) = ν(P) and that P_{1} computes the function #P. It is also easy to see that there exists a L_{M}-program P_{2} such that P_{1} ≪ P_{2} and ν(P_{2}) = ν(P_{1}). (Delete each string on the form nil(X); and each string on the form pred(X); from P_{1}. Let Q denote the resulting program. Let P_{2} be Q where each imperative on the form X:= Y is replace by X:= max(X,Y).) By lemma 5.5 we can assume that P_{2} is flattened out. Henceforth we can proceed as in the proof of Theorem 4.3, and use induction on n to prove that every function computed by P_{2} is in E^{n+2}. It follows that #P ∈ E^{n+2}.

Theorem 6.2 (Adequacy of (ν, L)). Every function in E^{n+2} can be computed by a L-program with ν-measure n.

Proof. We skip this proof. A proof of a similar result can be found in Kristiansen-Niggl [13].

It follows straightaway from Theorem 6.1 and Theorem 6.2 that we can characterise the Grzegorczyk hierarchy at and above the linear space level in terms of L-programs. We have E^{n+2} = L^{n} for all n ∈ ℕ where L^{n} is the set of function computed by an L-program with ν-measure n. It also follows from the two theorems (and Theorem 2.6) that the pair (ν, L) cannot be complete with respect to the Grzegorczyk hierarchy. There are a number of rather obvious, but still interesting, ways to extend the language L such that the pair (ν, L) remains sound (and of course adequate). We can add if-then and if-then-else structures:

     ........ if <test> then [......] else [.....] .......

The expressions permitted in <test> can be very sophisticated. The only requirement is that <test> must be a relation in E^{2} and that the evaluation of <test> does not mess the content of any registers. None of these requirements are very restrictive. We can add a statements which will terminate loops, e.g. the construction

     ..... loop X [ .......; exit <test>; .........] .....

where the loop governed by X terminates immediately when <test> is evaluated to true. Further, can we extend our arsenal of imperatives with a number of operations usually available in Pascal-like languages, e.g.

• \{X = x\} sqrt(X) \{X = ⌊\sqrt{x}⌋\} (square root)

• \{X = x, Y = y\} div(X,Y) \{X = if y > 0 then ⌊\frac{x}{y}⌋ else 0, Y = y\} (division)

• \{X = x, Y = y\} mod(X,Y) \{X = x − (⌊\frac{x}{y}⌋ × y), Y = y\} (remainder)

• {X = x, Y = y} sub(X,Y) {X = x ^{.} y, Y = y } (modified subtraction)

Note that all the proposed imperatives fulfil the requirements: (1) the imperative will never increase the value of a register, and (2) the imperative does not compute functions outside E^{2}. Indeed we are free to extend the language L by any imperative not violating these two requirements, and still retain soundness of the pair (ν, L). We can also permit constants anywhere it makes sense, e.g. as the second parameter in the subtraction imperative or at the right hand side of an assignment. The imperative X:= c, where c is a fixed natural number, should not be viewed as an assignment, but as a basic imperative setting the value of X to c (like nil(X) sets the value to 0). Thus, introduction of imperatives of the form X:= c, where c is a constant, will not affect the definition of the ν-measure. Perhaps it is not entirely obvious that the pair (ν, L) still will be sound when such assignments are permitted, but it will. No doubt, many other extensions which will bring L closer to a high level Pascal-like language and still not violate soundness of the pair (ν, L) are possible. The following properties of L are used in the proof of Theorem 6.1: (1) For very program P ∈ L there exists a program P′ ∈ L_{M} such that P ≪ P′. (2) No imperative in L computes functions outside E^{2}. Roughly speaking, these two properties of L (together with a number of other obvious properties) are all we need to prove soundness of the pair (ν, L). When we include the few trivial extensions we have proposed above in L, then L becomes a nice little language which engineers and students of applied computer science will recognise. Of course the language is not well equipped in many respects, but the language is actually useful as a tool for analysing the complexity of number-theoretic problems. Let us take the decision problem PRIME as an example, i.e. is it the case whether x is prime. A natural algorithm that solves the problem is easy to implement in L. The first algorithm which falls into our mind is perhaps to check for each number u from 2 to ⌊\sqrt{(}x)⌋ whether u divides x. As soon as we find a number in the given interval which divides x, we know that x is not prime. If we can search through the whole interval without finding such a number, we know that x is prime. It is straight forward to implement this algorithm in the extended version of L. Let P ≡

Y:= X; sqrt(Y); sub(Y,1); U:= 2;
loop Y [ Z:= X; mod(Z,U); exit Z=0; Z:= 1; suc(U) ]

It is easy to check that implementation is correct, i.e. that we have

{X = x > 1} P {Z = if x is prime then 1 else 0} .

Then we can check the ν-measure of P. This is a mechanical process, and in the present case it is easy to see that ν(P) = 0. Hence, we have established that PRIME is a problem in linspace by a straightforward implementation of the first algorithm which fell into our minds (accompanied by some trivial and mechanisable argumentation). The standard way to establish that a problem is in linspace is to find a suitable algorithm, implement the algorithm on a Turing machine, and then verify that the Turing machine work in linear time in the length of the input. Now, this is not easy unless you are a trained complexity theorist. So, a language like L together with a measure like μ is a useful tool when it comes to analysing the complexity of natural problems. Other formalisms developed in implicit computational complexity theory do not provide such tools. (Well, at least not so useful tools.) We will probably be better off analysing the computational complexity of a problem by ordinary mathematical reasoning than to trying to find a program which solves the problem in a formalism of e.g. Bellantoni-Cook.

7 Stack programs computing on the symbols of an alphabet

To capture the important complexity classes p and pf we need the stack programming language introduced in Kristiansen-Niggl [13]. We presuppose an arbitrary but fixed alphabet Σ and define a programming language computing on stacks over Σ. Intuitively, variables serve as stacks, each holding an arbitrary word over Σ. Like loop languages, stack languages are based on loops where the (maximal) number of times the body of a loop will be executed is determined before the execution of a loop starts.

Definition 7.1 (Stack programs). We have an alphabet Σ. We have an infinite supply of program variables (stacks). We will normally use X, Y, Z, A, B, C, U, V with or without subscript and superscripts to denote variables. For any variables X, Y and any a ∈ Σ we have the following imperatives (primitive

instructions): push(a,X), pop(X), nil(X), X:= Y.

A stack language is a set of programs generated by some of the following syntactical rules:

(I) Every imperative is a stack program.

(II) If P_{1}, P_{2} are stack programs, then so is the sequence statement P_{1};P_{2}.

(III) If P is a stack program, then so is every conditional statement

                          iftop(X)≡a[P]

.

(IV) If P is a stack program with no occurrence of the variable X in an imperative, then so is the loop statement foreachX[P].

The semantics of stack programs are as follows:

• the subprograms in a sequence P_{1}; …;P_{k} are executed one by one from the left to the right (Note that every stack program can be written uniquely in the form P_{1};…;P_{k} such that each component P_{i} is either a loop, an imperative, or a conditional.)

• the semantics of imperatives and conditionals are as follows:

– push(a,X) pushes letter a on top of stack X,

– pop(X) removes the top symbol on stack X, if any, otherwise (X is empty) the statement is ignored,

– nil(X) empties stack X,

– iftop(X)≡a[P] executes the body P if the top symbol on stack X is identical to letter a, otherwise the conditional statement is ignored,

• loop statements foreach X[P] has a “call by value” semantics: let U be a fresh variable and let P′ be P where each occurrence of X is replaced by U, then the semantics of foreachX[P] is given by the program

                  U:= X;

                         P′;pop(U); . . .;P′;pop(U)

|X| times

S_{0} is the stack language generated by rule (I), (II) and (IV) from the sole imperative push(a,X) (for any stack X and any a ∈ Σ). (So, there will be no conditionals in S_{0}-programs.) S_{1} is the stack language generated by rule (I), (II), (III) and (IV) from the imperatives push(a,X) and X:= Y (for any variables X, Y and any a ∈ Σ). S is the full stack language containing all the imperatives listed above (push(a,X), pop(X), nil(X), X:= Y), and closed under rule (I), (II), (III) and (IV). End of definition.

So, when a loop foreach X[P] is executed, the subprogram P works on a local copy of the stack X, and when the loop terminates the stack X has the same value as immediately before the execution of the loop started. This callby-value semantics ensures that S_{0}-programs are length-monotonic, that is, if P is a S_{0}-program with variables X⃗, then {X⃗=w⃗} P {X⃗=u⃗} implies |w⃗|≤|u⃗| (component-wise), and if |w⃗|≤|w′|, {X⃗=w⃗} P {X⃗=u⃗} and {X⃗=w′} P {X⃗=u′}, then |u⃗| ≤ |u′|. These monotonicity properties are essential in the proofs of the theorems in the sequel. We will now proceed and define the μ-measure and the ν-measure for stack programs. The definitions are identical to the corresponding definitions for loop programs, except that the push-imperative has taken the place of the suc-imperative, and that the loop foreach ... has taken the place of the

loop loop ....

Definition 7.2. The relations ≺P and \underrightarrow{P} are binary relations over V(P). The relation X ≺P Y holds iff

P has a subprogram foreach X [Q] where Q has a subprogram on the

     form push(b,Y).

The relation \underrightarrow{P} is the transitive closure of ≺P. Cliques, cover sets, etcetera are defined exactly as for loop programs (definition 3.2). We define the the μ-measure μ(P) of an S_{0}-program P by

• μ(push(a,X)) = 0 for every variable X and every a ∈ Σ.

• Let P ≡ Q_{1};Q_{2}. Then μ(P) = max(μ(Q_{1}), μ(Q_{2})).

   • Let P ≡ foreachX[Q]. Then

μ(P) = \{ \begin{matrix}μ(Q) + 1 & if Q has a clique of degree μ(Q) + 1 \\ μ(Q) & else \end{matrix}

End of definition.

We can now state and prove theorems, which in a perfectly good sense are soundness theorems, or completeness theorems, for stack languages and their measures.

Theorem 7.3 (Soundness and Completeness of (μ, S_{0})). We have

μ(P) ≤ n ⇔ #P(x⃗) ≤ f(|x⃗|) for some f ∈ E^{n+2}.

for every n ∈ ℕ and every P ∈ S_{0}.

Proof. Analogous to the proof of 4.8.

Corollary 7.4. Let P ∈ S_{0}. Every function computed by P is in pf if and only if P has μ-measure 0.

Proof. Assume P has μ-measure 0. By Theorem 7.3 there is a function f ∈ E^{2} such that #P(x⃗) ≤ f(|x⃗|), and then we also have #P(x⃗) ≤ q(|x⃗|) for some polynomial q since every function in E^{2} is bounded by a polynomial. So, the number of steps in the execution of the stack program P is bounded by a polynomial in the length of the input. It is a standard exercise to prove that P can be simulated by a Turing machine also working in polynomial time. It follows that every function computed by P is in pf. Assume that every function computed by P is in pf. Then we have #P(|x⃗|) ≤ q(|x⃗|) for some polynomial q. (Assume that such a q does not exists. Then then at least one loop in P will be controlled by a stack which length is not bounded by any polynomial in the length of the input. But then, since S_{0}- programs are length-monotonic, the program P computes a function which is not in pf.) Every polynomial is bounded by a function in E^{2}. Hence, P has μ-measure 0 by Theorem 7.3.

Definition 7.5. We shall define the measure ν for the programming languages S_{1} and S. The definition is analogous to the definition of the ν-measure for loop programs. Let ≺P be defined as in Definition 7.2. Let X:=PY denote that X:= Y is a

subprogram of P. The relation \underrightarrow{P} is the smallest relation such that

- if X ≺P Y, then X\underrightarrow{P}Y

- \underrightarrow{P} is transitive

   - if X:=PY and Z\underrightarrow{P}Y, then Z\underrightarrow{P}X

Then we define clique, cover set, etcetera exactly as above, and finally we define the ν-measure ν(P) of the program P by

• ν(imp) = 0 for every imperative imp.

• Let P ≡ Q_{1};Q_{2}. Then ν(P) = max(ν(Q_{1}), ν(Q_{2})).

• Let P ≡ iftop(X)≡a[Q]. Then ν(P) = ν(Q).

   • Let P ≡ foreachX[Q]. Then

ν(P) = \{ \begin{matrix}ν(Q) + 1 & if Q has a clique of degree ν(Q) + 1 \\ ν(Q) & else \end{matrix}

End of definition.

Theorem 7.6 (Soundness of (ν, S)). We have

ν(P) ≤ n ⇒ #P(x⃗) ≤ f(|x⃗|) for some f ∈ E^{n+2}.

for every n ∈ ℕ and every P ∈ S_{1}.

Proof. Analogous to the proof of Theorem 6.1. Introduce a language S_{M} with nice monotonicity properties such that for every program P ∈ S there exists a program Q ∈ S_{M} such that ν(P) = ν(Q) and P ≪ Q. Prove a flattening lemma for S_{M}, i.e. a lemma corresponding to Lemma 5.5. Thereafter proceed as in the proof of Theorem 6.1.

To be able to state adequacy results for stack programs we introduce a new hierarchy.

Definition 7.7. For every n ∈ ℕ we define H^{n} to be the class of functions from tuples of strings over Σ into strings over Σ which can be computed by a Turing machine which works in time f for some f ∈ E^{n}, i.e. the number of steps in the execution of the Turing machine on input w is bounded by f(|w|) for some f ∈ E^{2}. (Now, |w| denotes as usual the length of the string w, so H^{2} = pf.) End of definition.

Theorem 7.8 (Adequacy of (ν, S)). Every function in H^{n+2} can be computed by a S-program with ν-measure n (for every n ∈ ℕ).

Proof. We skip this proof. A proof of a similar result can be found in Kristiansen-Niggl [13].

Corollary 7.9. (i) A function is in pf if and only if it can be computed by an S-program with ν-measure 0. (ii) A problem is in p if and only if it can be decided by a program with ν-measure 0.

Proof. Recall that H^{2} = pf. Hence, the corollary follows straightaway from Theorem 7.6 and Theorem 7.8.

8 Subelementary complexity classes

In this section we will focus on some subclasses of the Kalmár elementary functions. In order to have a suitable framework for our analysis we will introduce a modified version of the Grzegorczyk hierarchy. In this hierarchy we have the Kalmár elementary relations on level 4; we have pspace on level 3; we have linspace on level 2, 1 and 0.

Definition 8.1. We define the sequence {G_{i}}_{i∈ℕ} of number-theoretic functions by G_{0}(x) = x + 1, G_{1}(x) = 2x + 1, G_{2} = x^{2} + 2, G_{3}(x) = 2^{(|x|^{2})}, G_{4}(x) = 2^{x}, and G_{i+1}(x) = G_{i}^{x}(2) for i ≥ 4. (The function |x| is usually defined as the number bits of required to represent the number x, i.e. |x| = ⌈log_{2} x⌉.) The ith modified Grzegorczyk class G^{i}, is the least class of functions containing the initial functions zero, successor, projections, maximum and G_{i}, and is closed under composition and bounded simultaneous recursion. We dub {G^{i}}_{i∈ℕ} the modified Grzegorczyk hierarchy. End of definition.

Theorem 8.2. (i) For every n ∈ ℕ and f ∈ G^{n} there exists a fixed number k such that f(x⃗) ≤ G_{n}^{k}(max(x⃗)). Thus, we have G^{n} ⊂ G^{n+1} for any n ∈ ℕ. (ii) E^{0} ⊂ G^{0}. (iii) E^{2} = G^{2}, and thus G^{2} equals linspacef. (iv) G^{n+1} = E^{n} for n ≥ 3. In particular, G^{4} equals the class of Kalmár-elementary functions.

(v) G_{⋆}^{0} = G_{⋆}^{1} = G_{⋆}^{2}. Thus, each of these classes equals linspace. (vi) G^{3} = pspacef.

Proof. (i) Use induction on the definition of f. (ii) It is obvious that E^{0} ⊆ G^{0}. Further, max is one of the initial functions in G^{0}, but E^{0} does not contain max. To see this, assume max ∈ E^{0}. Then there exist constants k and i ∈ {1, 2} such that max(x_{1}, x_{2}) ≤ x_{i} + k. This is a nonsense. (iii) and (iv).

It is obvious that E^{2} ⊆ G^{2} and that E^{i} ⊆ G^{i+1} for i ≥ 3. The right-to-left inclusions follows from the fact that E^{i} is closed under bounded simultaneous recursion for all i ≥ 2. (v) Muchnick [24] studies the vectorised Grzegorczyk hierarchy E^{v,0}, E^{v,1}, E^{v,2}, . . .. He proves that E_{⋆}^{v,i} = E_{⋆}^{2} for i = 0, 1, 2. Thus (v) holds since it is obvious that E_{⋆}^{v,i} ⊆ G_{⋆}^{i}. (vi) We skip this proof.

Note 8.3. (i) We would have achieved the same hierarchy if we had defined G_{4}(x) = G_{3}^{x}(2). Thus, we could have defined the backbone functions in a uniform way from level 4 and upwards. Transparency is the sole motive for defining G_{4}(x) to equal 2^{x}. (ii) The modified Grzegorczyk hierarchy is not an unnatural hierarchy compared to the original hierarchy. The class G^{3} is in a way artificially inserted into the hierarchy, but one should note, so is E^{2} in the original hierarchy. One application of of unbounded primitive recursion over functions in E^{1} might yield a function on the Kalmár-elementary level, i.e. a function which is not in E^{2}. Thus, one could argue that E^{2} is artificially inserted into the the hierarchy. We cannot uniformly define the original hierarchy all the way from the very the bottom without loosing the linspacelevel. In the modified hierarchy we have in addition to the linspace-level (G^{2}) inserted a pspace-level (G^{3}). One unbounded application of simultaneous (or primitive) recursion over functions in G_{i} for i = 1, 2, 3 might yield a function on the Kalmár-elementary level, i.e. on the 4th level of the hierarchy. (iii) The classes in the modified hierarchy retain all the closure properties of classes in the original hierarchy, and the class G^{3} is no exception. (More on generalised Grzegorczyk classes can be found in Kristiansen [12].) (iv) The classes G^{0} and G^{1} are by definition closed under bounded simultaneous recursion, whereas it is an open problem whether E^{0} and E^{1} are closed under such recursion. Thus it also becomes an open problem if G^{1} = E^{1}. End of note.

Definition 8.4. Let L be defined as in the previous sections, i.e. as the loop language with the imperatives suc(X), X:= Y, pred(X) and nil(X). Let L^{∅}

be the set of L programs P such that the relation \underrightarrow{P} is empty, and let Lir be the set of L programs P such that the relation \underrightarrow{P} is irreflexive. Let L^{n} be the set of programs with ν-measure n. If L^{•} is a set of loop programs, then L^{•} denotes the set of functions which can be computed by the programs in L^{•}. End of definition.

Theorem 8.5. Lir_{⋆} = L_{⋆}^{0} = G_{⋆}^{2} = linspace.

Proof. It is quite obvious that Lir = L^{0}. It follows from 6.2 that L^{0} = E^{2} = linspacef. Theorem 8.2 says that G^{2} = E^{2}.

Lemma 8.6. Let P be an L-program where V(P) = X⃗. Let m be a fixed number such that no register during an execution of P on input X⃗ = x⃗ exceeds m. Then there exists Q ∈ L^{∅} such that

{X⃗ = x⃗}P{X⃗ = x′} ⇔ {X⃗ = x⃗, M = m}Q{X⃗ = x′} .

Proof. Let U and V be a fresh variables. Let P′ be P where every subprogram on the form pred(Z) is replaced by the subprogram

             nil(U);loopZ[ V:= U;suc(U) ];Z:= V .

Then we have {X⃗ = x⃗}P{X⃗ = y⃗} iff {X⃗ = x⃗}P′{X⃗ = y⃗} and there are no occurrences of pred(..) in P′. Now, let M be a fresh variable, let the function τ from L-programs (with no occurrences of pred(..)) into L-programs be defined by

- τ(P;Q) = τ(P); τ(Q)

   - τ(loopW[P]) = loop W [τ(P)]
   - τ(W:= Y) = τ(W:= Y)
   - τ(nil(W)) = W:= M
   - τ(suc(W)) = pred(W)

and let P′′ = τ(P′). The program P′′ has no occurrences of the statement suc(..), and for all sufficiently large m we have {X⃗ = x⃗}P{X⃗ = y⃗} iff {X⃗ = x⃗, M = m}P′′{X_{1} = m − y_{1}, …, X_{l} = m − y_{l}} where X⃗ = X_{1}, …, X_{l}. Let U be a fresh variable and let

               R_{i} ≡ U:= M;loop X_{i}[pred(U)];X_{i}:= U

Finally, let

Q ≡ P′′;R_{1}; …;R_{l} .

Then, we have {X⃗ = x⃗}P{X⃗ = x′} iff {X⃗ = x⃗, M = m}Q{X⃗ = x′}.

Lemma 8.7. The function max(x, y) can be computed by a program in L^{∅}.

Proof. Let P be the program

U:= X; loop Y [pred(U)];
nil(V); suc(V); loop U [pred(V)];
Z:= X; loop V [Z:= Y]

Then P is in L^{∅} and {X = x, Y = y}P{Z = max(x, y)}.

Theorem 8.8. G^{0} = L^{∅}.

Proof. First we prove G^{0} ⊆ L^{∅}. Assume f ∈ G^{0}. It is easy to see that there exists an L-program P such that {Z⃗ = z⃗}P{Y = f(z⃗)}. It is also easy to see that there is fixed number k such that no register exceeds the value max(z⃗)+k during an execution of P on input Z⃗ = z⃗. Lemma 8.7 entails that there exists a program imax in L^{∅} such that {X⃗ = x⃗} imax {X⃗ = x⃗, M = max(x⃗) + k}, and then Lemma 8.6 entails that f can be computed by a program in L^{∅}. This completes the proof of G^{0} ⊆ L^{∅}. The proof of L^{∅} ⊆ G^{0} is straightforward. Let L^{∅−} be the set of L^{∅} programs with no occurrence of imperatives on the form suc(X). Use induction over the syntax of programs to prove that for each P ∈ L^{∅−} where V(P) = {X_{1}, …, X_{n}} = X⃗ there exists functions f_{1}, …, f_{n} ∈ G^{0} such that

{X⃗ = x⃗} P {X_{1} = f_{1}(x⃗) ≤ max(x⃗), …, X_{1} = f_{n}(x⃗) ≤ max(x⃗)} .

The desired result follows easily.

Corollary 8.9. L_{⋆}^{∅} = Lir_{⋆} = linspace.

Proof. The equalities follow from the theorems 8.5, 8.8 and 8.2.

Note 8.10. The previous corollary implies that we cannot characterise any smaller complexity class than linspace solely by imposing restrictions on the relation “X controls Y” in any language containing L.

Definition 8.11. Recall that S denotes the set of stack programs (defined in a previous section). Let S^{∅} be the set of S-programs P such that the relation

\underrightarrow{P} is empty, and let Sir be the set of S-programs P such that the relation \underrightarrow{P} is irreflexive. Let S^{n} be the set of program with ν-measure n. If S^{•} is a set stack of programs, then S^{•} denotes the set of functions which can be computed by programs in S^{•}. End of definition.

Theorem 8.12. S_{⋆}^{0} = Sir_{⋆} = p.

Proof. Corollary 7.9 states that S_{⋆}^{0} = p. It is easy to prove that S_{⋆}^{0} =

Sir_{⋆}.

We have seen that L_{⋆}^{∅} = Lir_{⋆}. In contrast, the next theorem tells that S_{⋆}^{∅} is strictly included in Sir_{⋆}.

Theorem 8.13. conspace ⊂ S_{⋆}^{∅} ⊂ Sir_{⋆} = p.

Proof. Every one-way finite automaton can be simulated by a program in S^{∅}. Thus, conspace ⊆ S_{⋆}^{∅}. (conspace equals the class of languages recognised by such automatons, see Odifreddi [26].) Let

A = {w | |w| = x^{2} for some x ∈ ℕ} .

Membership in A can be decided by a program in S^{∅}, but not by a finite automaton. Hence conspace ⊂ S_{⋆}^{∅}. It is trivial that S_{⋆}^{∅} ⊆ Sir_{⋆}. Let w^{R} denote the word w reversed. Let B = {w | w = w^{R} }. Membership in B can obviously be decided by a Turing machine working in polynomial time, but no program in S^{∅} can decide membership in B. Thus S_{⋆}^{∅} ⊂ Sir_{⋆} = p.

The languages L and S can be merged into one imperative programming language I. The resulting language I computes both on numbers and on symbols in the alphabet {0, 1}. (All our result can be generalised to arbitrary alphabets with cardinality ≥ 2.) Still, the language will have only one type of variables. Whether a variable X hold a natural number or a stack over the fixed alphabet {0, 1} depends on the point of view. Used in an L-construction, e.g. suc(X), we view X as a number variable; used in an Sconstruction, e.g. push(0,X), we view X as a stack variable. In order to make this strategy work we need a suitable bijection between the natural numbers an the strings over the alphabet {0, 1}.

Definition 8.14. We use 𝕎 to denote the set of words, i.e. the set of strings over bits (the alphabet {0, 1}). We use ε to denote the empty word. As usual, |w| denotes the length of the word w, and w_{i} denotes the ith bit of the word w starting from 0 in the rightmost position. Thus, if |w| = 4, then w = w_{3}, w_{2}, w_{1}, w_{0}. We use juxtaposition to concatenate words. So, e.g. w0 denotes the word w extendend by 0 in the rightmost position. The function σ : 𝕎 → ℕ is defined by

σ(w) = 2^{n} + w_{n−1}2^{n−1} + ⋯ + w_{1}2^{1} + w_{0}2^{0} − 1

where n = |w|. End of definition.

The function σ is a bijection and the numbers 0, 1, 2, 3, … are respectively mapped to the words ε, 0, 1, 00, 01, 10, 11, 000, 001, 010, 011, . . ..

Lemma 8.15. (1) σ is a bijection. (2) σ(w) ≤ 2^{|w|+1}. (3) σ(w0) = 2(σ(w) + 1) − 1 and σ(w1) = 2(σ(w) + 1).

Proof. We leave (1) and (2) to the reader. Let n = |w|. Then

σ(w0) = 2^{n+1} + w_{n−1}2^{n} + ⋯ + w_{0}2^{1} + (0 × 2^{0}) − 1 def. of σ(w0)
= 2(2^{n} + w_{n−1}2^{n−1} + ⋯ + w_{0}2^{0}) − 1
= 2(2^{n} + w_{n−1}2^{n−1} + ⋯ + w_{0}2^{0} − 1 + 1) − 1
= 2(σ(w) + 1) − 1  def. of σ(w)

This proves σ(w0) = 2(σ(w) + 1) − 1. A similar argument proves σ(w1) = 2(σ(w) + 1)

Note 8.16. We push and pop bits on the right hand side of a word, e.g. {X = w}push(0,X){X = w0} and {X = w1}pop(X){X = w}.

Definition 8.17 (General imperative programs). The syntax of the programming language I are inductively defined as follows:

   • Every imperative among nil(X), suc(X), pred(X), pop(X), push(b,X)

X:= Y is an program (for any variables X, Y and b ∈ {0, 1}) .

• If P is a program with no occurrence of the variable X in an imperative, then so is the loop loopX[P] (for any variables X).

• If P is a program, then so is every conditional if top(X) ≡ b [P] (for every variable X and b ∈ {0, 1}).

• If P is a program with no occurrence of the variable X in an imperative, then so is the loop foreachX[P] (for any variables X).

• If P_{1}, P_{2} are programs, then so is the sequence P_{1};P_{2}.

The semantics of I are a straightforward merging of the semantics of the languages L and S. Note that since σ(ε) = 0, the imperative nil(X) will turn X into the empty stack when X is viewed as an stack, and set X to 0 if X is viewed as a natural number. End of definition.

Example 8.18. The following program computes the function G_{4}. (Recall that G_{4}(x) = 2^{x}.)

   {X = x} nil(Y); loop X [push(0,Y)]; suc(Y){Y = 2^{x}} .  (∗)

The next program computes the length function |w|.

      {X = w} nil(Y); foreach X [suc(Y)]{Y = |w|} .  (∗∗)

End of example.

Definition 8.19. We define relation \underrightarrow{P} for programs in I. (The definition is analogous to the definition of the corresponding relations for programs in L and S.)

The relations ≺P and \underrightarrow{P} are binary relations over V(P). The relation X ≺P Y holds iff at least one of (i) and (ii) holds:

(i) P has a subprogram loop X [Q] where suc(Y) or push(b,Y) are subprograms of Q.

(ii) P has a subprogram foreach X [Q] where suc(Y) or push(b,Y) are subprograms of Q.

Let X:=PY denote that X:= Y is a subprogram of P. The relation \underrightarrow{P} is the smallest relation such that

- if X ≺P Y, then X\underrightarrow{P}Y

- \underrightarrow{P} is transitive

   - if X:=PY and Z\underrightarrow{P}Y, then Z\underrightarrow{P}X

Let I^{∅} denote the set of I-programs P where the relation \underrightarrow{P} is empty, and let Iir denote the set of I-programs P where the relation \underrightarrow{P} is irreflexive. Let Iir- denote the set of I-programs P such that P ∈ Iir and no subprogram of P on the form loop X[Q] has a subprogram on the form push(b,Y). If I^{•} is a set of imperative programs, then I^{•} denotes the class of functions which can be computed by the programs in I^{•}. End of definition. Example 8.20. The program (**) in Example 8.18 is in Iir-. The program (*) in the same example is in Iir, but not in Iir-. The following program which computes the function G_{3} is in Iir-. (Recall that G_{3}(x) = 2^{|x|^{2}}, and if 0^{n} denotes a string of n zeros, then σ(0^{n}) = 2^{n} − 1.)

{X = x}

    nil(Y); Z:= X; foreach X [foreach Z [push(0,Y)]]; suc(Y)

{Y = 2^{|x|^{2}}}

End of example.

Theorem 8.21. The class Iir equals the class of Kalmàr elementary functions G^{4}.

Proof. Use induction on the syntactical build-up of a program P ∈ Iir to prove that for every function f computed by P we have f(x⃗) ≤ G_{4}^{k}(max(x⃗)) for some fixed number k. It follows easily that Iir ⊆ G^{4} since G^{4} is closed under composition and bounded simultaneous recursion. Assume f ∈ G^{4}. Use induction on a definition of f to prove that f(x⃗) can be computed by a program P ∈ L such that during the computation no register exceeds the value G_{4}^{k}(max(x⃗)) for some fixed number k. By Lemma 8.6 there is a program Q ∈ L^{∅} (and thus Q ∈ Iir) such that

{X⃗ = x⃗}P{X⃗ = x′} ⇔ {X⃗ = x⃗, M ≥ G_{4}^{k}(max(x⃗))}Q{X⃗ = x′} .

Example 8.18 shows that the function G_{4} can be computed by a program in Iir. Hence, a program in Iir can also compute the function G_{4}^{k}(max(x⃗)). It follows that f can be computed by a program in Iir. Thus we have proved G^{4} ⊆ Iir.

Theorem 8.22. The class Iir- equals the class of polynomial space computable functions G^{3}, i.e. pspacef.

Proof. This proof is identical to the proof of Theorem 8.21 where “4” is replaced by “3”, “ir” is replaced by “ir-” and “Example 8.18” is replaced by “Example 8.20”.

In order to state some normal form results, we shall introduce the notion of a core language and core programs. Roughly speaking, the core language is the part of the programming language we need to compute fast growing functions.

Definition 8.23. The set of core programs is a subset of the set of I-programs. A core program is defined by

• every imperative among suc(X), push(0,X), push(1,X) is a core program (for any variable X).

• If P is a core program with no occurrence of the variable X in an imperative, then so are loop X[P] and foreach X[P] (for any variables X).

• If P_{1}, P_{2} are core programs, then so is P_{1};P_{2}.

Assume V(P) = X⃗. We us !P(x⃗) to denote the least natural number m such that no register exceeds m during an execution of the program P on input X⃗ = x⃗. Assume V(P) ⊆ V(Q). Let us say, V(P) = X⃗ and V(Q) = X⃗, Y⃗. We use P ∼ Q to denote that Q computes the same functions as P with respect to the variables X⃗, i.e. the relation P ∼ Q holds if and only if

{X⃗ = x⃗}P{X⃗ = z⃗} ⇔ {X⃗ = x⃗, Y⃗ = y⃗}Q{X⃗ = z⃗} .

End of definition.

Lemma 8.24. Let Lan be any of the programming languages Iir-, Iir, Lir, L^{n} (for n ∈ ℕ), Sir, and S^{n} (for n ∈ ℕ). Let V(P) = X⃗. If P ∈ Lan, then there exists a core program Q ∈ Lan such that {X⃗ = x⃗}Q{X⃗ = x⃗, Z ≥ !P(x⃗)} (where Z is any fresh variable).

Proof. We leave this proof to the reader.

Lemma 8.25. For each P ∈ I (and thus we might have P ∈ S) there exists Q ∈ L such that P ∼ Q and !Q(x⃗, 0, …, 0) ≤ !P(x⃗) + k for some fixed number k.

Proof. Let Y be a fresh variable. Lemma 8.15 says that σ(s0) = 2(σ(s)+1)−1. Thus, if Q_{0} is the program

    suc(X); nil(Y); loop X [suc(Y); suc(Y)]; X:= Y; pred(X)

we have push(0,X) ∼ Q_{0}. Furthermore, we

!_{Q_{0}}(x, 0) ≤ !push(0,X)(x) + 1 .

Obviously, we also have Q_{1} ∈ L such that push(1,X) ∼ Q_{1} and such that we have the required bound on !_{Q_{1}}. Let P_{0} be P where each occurrence of push(0,X) is replaced by Q_{0} and each occurrence of push(1,X) is replaced by Q_{1}. Then we have P ∼ P_{0} and !_{P_{0}}(x⃗,0) ≤ !P(x) + k for some fixed k. Now we have a program P_{0} without “push”. We can proceed in the same way to remove the occurrences of “pop” and the constructions on the form iftop(X)≡a[R] and foreachX[R]. It is a rather straightforward process.

Theorem 8.26 (Normal Form). Let Lan be any of the programming languages Iir-, Iir, Lir, L^{n} (for n ∈ ℕ), Sir, and S^{n} (for n ∈ ℕ). For any P ∈ Lan there exists a core program C ∈ Lan and a program Q ∈ L^{∅} such that P ∼ C;Q.

Proof. Assume P ∈ Lan. By Lemma 8.25 there is an L-program Q_{0} such that P ∼ Q_{0} and !_{Q_{0}}(x⃗,0) ≤ !P(x⃗) + k for some fixed k. Then, by Lemma 8.6 there exists Q ∈ L^{∅} such that

{X⃗ = x⃗}P{X⃗ = x′} ⇔ {X⃗ = x⃗, M = m}Q{X⃗ = x′}

whenever m ≥ !P(x⃗)+k. By Lemma 8.24 there exists a core program C ∈ Lan such that {X⃗ = x⃗}C{X⃗ = x⃗, M ≥ !P(x⃗) + k}. Hence

{X⃗ = x⃗}P{X⃗ = x′} ⇔ {X⃗ = x⃗}C;Q{X⃗ = x′}

i.e. we have P ∼ C;Q, where Q ∈ L^{∅} and C is a core program in Lan.

Corollary 8.27 (Normal Form). For every program P ∈ Iir- there are programs Q_{0} ∈ Sir and Q_{1} ∈ L^{∅} such that P ∼ Q_{0};Q_{1}.

Proof. By Theorem 8.26 there exists a core program C ∈ Iir- and a program Q_{1} ∈ L^{∅} such that P ∼ C;Q_{1}. The proof of the theorem shows that C has the property {X⃗ = x⃗}C{X⃗ = x⃗, M ≥ !P(x⃗) + k} and that the theorem will hold for any program C′ with this property. Since C ∈ Iir-, there will be a program in Sir satisfying the property, i.e. there is a program Q_{0} ∈ Sir such that {X⃗ = x⃗}Q_{0}{X⃗ = x⃗, M ≥ !P(x⃗) + k}. Hence, we have also have P ∼ Q_{0};Q_{1} where Q_{0} ∈ Sir and Q_{1} ∈ L^{∅}.

Corollary 8.28. If p ≠ pspace, then linspace \ p ≠ ∅.

Proof. We assume linspace \ p = ∅, and thus L^{∅} = linspace ⊆ p = Sir, and prove that p = pspace. Pick an arbitrary problem α in pspace. Now, pspace = Iir-_{⋆} and thus there is a program P ∈ Iir- which solves the problem. According to Corollary 8.27 there are programs Q ∈ Sir and R ∈ L^{∅} such that P ∼ Q;R. Now, since we have linspace ⊆ p by our assumption, every zero-one function computed by R can be computed by a program in Sir. Hence, there is a program P′ ∈ Sir which solves the problem α, and thus α ∈ p. This proves pspace ⊆ p. The inclusion p ⊆ pspace is trivial. Hence p = pspace.

Corollary 8.28 is of course a very well known fact. Indeed, many problems in linspace are known to be pspace complete. Still, it is nice to see that such a corollary follows from our theory on programming languages.

9 Uniform translations between formalisms

Several formalisms have been introduced in order to give implicit characterisations of complexity classes, e.g. predicative recursion (Bellantoni-Cook [1]), tiered definition schemes (Leivant [17]), measures on lambda terms (Niggl [25]) and measures on primitive recursive definitions (Bellantoni-Niggl [5]). In contrast to these formalism, the imperative languages introduced in this report are flexible programming languages closely related to a von Neumann computer architecture. It is likely that programs and definitions of functions in several other formalism easily and uniformly can be translated into our imperative languages. Theorem 9.2 exemplifies the type of translation results we are discussing. We consider the theorem to be a mere exercise preparing us for more sophisticated results along the same line.

There can be several benefits of discovering such translations. It might yield a valuable analysis of actual computations of functions defined in a formalism, e.g. an analysis of the flow of data, or a refined analysis of the space requirements. Another benefit might be an easy and transparent proof that functions defined in a certain formalism is in a certain complexity class, e.g. it is a corollary of Theorem 9.2 below that the set of functions defined by predicative recursion over natural numbers is included in linspacef. The theorem states that every function defined by such recursion can be computed by a program in Lir, and Lir equals linspacef. Definition 9.1. Let B be the Bellantoni-Cook class of function definitions over ℕ generated by the definition schemes

- Safe composition: f(x⃗; a⃗) = h(r⃗(x⃗; ); t⃗(x⃗; a⃗))

- Predicative recursion on numbers:

f(0, x⃗; a⃗) = g(x⃗; a⃗) f(y + 1, x⃗; a⃗) = h(y, x⃗; a⃗, f(y, x⃗; a⃗))

from the initial functions 0 (constant), π_{j}^{m,n}(x_{1}, …, x_{n}; x_{n+1}, …, x_{n+m}) (projections), s(; a) (successor), p(; a) (predecessor) and c(; a, b, c) (conditional, c(; a, b, c) = b if a = 0 and c(; a, b, c) = c if a ≠ 0 ). We say that an element in a partial ordering is minimal if it has no predecessors, and maximal if it has no successors. End of definition.

Theorem 9.2. For every f ∈ B we can uniformly construct an L-program P such that

{X⃗ = x⃗, A⃗ = a⃗} P {O = f(x⃗; a⃗)}

and the relation \underrightarrow{P} is irreflexive (and thus an ordering relation). Moreover,

the variables X⃗ are minimal elements in the ordering \underrightarrow{P}, and the variables A⃗ and O are maximal elements.

Proof. We use induction on a definition of f to prove the theorem strengthened by the assertion

(*) the program P does not contain the subprogram suc(Z) for any Z ∈ X⃗.

The following programs shows that the theorem and (*) hold when f is an initial function.

   - nil(O){O = 0}
   - {A = a} suc(A); O:=A {O = s(; a)}
   - {A = a} pred(A); O:=A {O = p(; a)}

- {X⃗ = x⃗} O:=X_{j} {O = π_{j}^{m,n}(x_{1}, …, x_{n}; x_{n+1}, …, x_{n+m})}
- {A = a, B = b, C = c} O:= B; for A [ O:= C ] {O = c(; a, b, c)}

Suppose f is defined by safe composition. It should be sufficient to carry out the proof for the case

f(x, y; a, b) = h(r_{1}(x, y; ), r_{2}(x, y; ); t_{1}(x, y; a, b), t_{2}(x, y; a, b))

. The induction hypothesis gives programs R_{1}, R_{2}, T_{1}, T_{2} such that

{X^{R^{i}} = x, Y^{R^{i}} = y} R_{i} {O^{R^{i}} = r_{i}(x, y; )}

and

{X^{T^{i}} = x, Y^{T^{i}} = y, A^{T^{i}} = a, B^{T^{i}} = b} T_{i} {O^{T^{i}} = t_{i}(x, y; a, b)}

for i = 1, 2. Furthermore, the induction hypothesis yields a program H such that

{XH = x, YH = y, AH = a, BH = b} H {OH = h(x, y; a, b)} .

We have renamed variables such that each variable occur in at most one of the programs. (The notation XQ indicates that the variable XQ does not occur in any other program than Q.) Let X, Y, A, B, O be fresh variables. The theorem and (*) hold when P is the program

        X^{R^{1}}:= X;Y^{R^{1}}:= Y;R_{1};X^{R^{2}}:= X;Y^{R^{2}}:= Y;R_{2};
        X^{T^{1}}:= X;Y^{T^{1}}:= Y;A^{T^{1}}:= A;B^{T^{1}}:= B;T_{1};
        X^{T^{2}}:= X;Y^{T^{2}}:= Y;A^{T^{2}}:= A;B^{T^{2}}:= B;T_{2};
        XH:= O^{R^{1}};YH:= O^{R^{2}};AH:= O^{T^{1}};BH:= O^{T^{2}};H;O:= OH

Suppose f(0, x⃗; a⃗) = g(x⃗; a⃗) and f(y +1, x⃗; a⃗) = h(y, x⃗; a⃗, f(y, x⃗; a⃗)). In order to avoid cluttered notation, we say that x⃗ is the single variable x and that a⃗ is the single variable a. The induction hypothesis yields programs G and H such that

{XG = x, AG = a, } G {OG = g(x; a)}

and

{YH = y, XH = x, AH = a, BH = b} H {OH = h(y, x; a, b)}

where we have renamed variables such that no variable occur both in G and H. Let X, Y, A, W, O be fresh variables and let P be the program

          XG:= X;AG:= A;G;BH:= OG;nil(W)
          for Y [ YH:= W;XH:= X;AH:= A;H;
                 BH:= OH;suc(W) ];
          O:= OH

Then the theorem and (*) hold for P. In particular, the relation \underrightarrow{P} will be

irreflexive since both BH and OH are maximal elements in the ordering \underrightarrow{H}.

References

[1] S. J. Bellantoni and S. Cook. A New Recursion-Theoretic Characterization of the Polytime Functions. Computational Complexity, 2:97–110, 1992.

[2] S. J. Bellantoni. Predicative Recursion and Computational Complexity. PhD thesis, Toronto, September 1993.

[3] S. J. Bellantoni. Predicative recursion and the polytime hierarchy. In P. Clote and J. Remmel, editors, Feasible Mathematics II, Perspectives in Computer Science, pp. 15–29, Birkhäuser, 1994.

[4] S. J. Bellantoni, K.-H. Niggl and H. Schwichtenberg. Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104:17–30, 2000.

[5] S.J. Bellantoni and K.-H. Niggl. Ranking primitive recursions: The low Grzegorczyk classes revisited. SIAM J. of Comput., 29(2):401–415, 2000.

[6] P. Clote. Computation Models and Function Algebra. In: Handbook of Computability Theory. Ed Griffor, ed., Elsevier 1996.

[7] P. Clote. A Safe Recursion Scheme for Exponential time Technical Report 9607, Computer Science Department, LMU Munich, October 1996.

[8] B. Goetze and W. Nehrlich. The structure of loop programs and subrecursive hierarchies. Zeitschr. f. math. Logik und Grundlagen d. Math., 26:255–278, 1980.

[9] A. Grzegorczyk. Some classes of recursive functions. Rozprawy Matematyczne, No. IV, Warszawa, 1953.

[10] M. Hofmann. Typed lambda calculi for polynomial-time computation. Habilitation Thesis, TU Darmstadt, 1998.

[11] M. Hofmann. (Editor) Proceedings of the 3rd International Workshop on Implicit Computational Complexity ICC ’01. BRICS Notes Series, Department of Computer Science University of Aarhus. http://www.brics.dk,

ftp://ftp.brics.dk

[12] L. Kristiansen. Papers on subrecursion theory. Dr Scient Thesis, ISSN 0806-3036, ISBN 82-7368-130-0, Research Report 217, Department of Informatics, University of Oslo 1996.

[13] L. Kristiansen and K.-H. Niggl. On the computational complexity of imperative programming languages. Theoretical Computer Science, to appear

[14] M. Kutylowski. Small Grzegorczyk classes. J. London Math. Soc., 36:193– 210, 1987.

[15] D. Leivant. Stratified functional programs and computational complexity. In: Conference Record of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pp. 325-333, New York, 1993.

[16] D. Leivant and Jean-Yves Marion. Lambda Calculus Characterizations of Poly-Time. Fundamenta Informaticae, 19:167–184, 1993.

[17] D. Leivant. Ramified recurrence and computational complexity I: Word recurrence and poly-time. In: P. Clote and J. Remmel, editors, Feasible Mathematics II, Perspectives in Computer Science, pp. 320–343, Birkhäuser, 1994.

[18] D. Leivant. Predicative recurrence in finite type. In: A. Nerode and Y. V. Matiyasevisch, editors, Logical Foundations of Computer Science, Springer Lecture Notes in Computer Science, 813:227–239, 1994.

[19] D. Leivant and J.-Y. Marion. Ramified Recurrence and Computational Complexity II: Substitution and Poly-space. Computer science logic (Kazimierz, 1994), 486–500, Lecture Notes in Comput. Sci., 933, Springer, Berlin, 1995

[20] D. Leivant and J.-Y. Marion. Ramified Recurrence and Computational Complexity IV: Predicative Functionals and Poly-space. Information and Computation, to appear.

[21] D. Leivant. Intrinsic reasoning about functional programs. Annals of Pure and Applied Logic, to appear.

[22] M. Machthey. Augmented loop languages and classes of computable functions. J. Comp. and System Sciences, 6:603–624, 1972.

[23] A.R. Meyer and D.M. Ritchie. The complexity of loop programs. In: Proc. ACM Nat. Conf. 1967, pp. 465–469.

[24] S.S. Muchnick. The vectorized Grzegorczyk hierarchy. Z. Math. Logik Grundlag. Math. 22:441–480, 1976.

[25] K.-H. Niggl. The μ-measure as a tool for classifying computational complexity. Archive for Mathematical Logic, 39:515–539, 2000.

[26] P. Odifreddi. Classical recursion theory. Vol. II. . Studies in Logic and the Foundations of Mathematics, 143. North-Holland Publishing Co., Amsterdam, 1999.

[27] I. Oitavem. New Recursive Characterizations of the Elementary Functions and the Functions Computable in Polynomial Space. Revista Mathematica de la Universidad Complutense de Madrid, 10(1), 1997.

[28] R. W. Ritchie. Classes of predictably computable functions. Trans. A.M.S., 106:139–173, 1963.

[29] H. E. Rose. Subrecursion. Functions and hierarchies. Clarendon Press, Oxford 1984.

[30] H. Simmons. The Realm of Primitive Recursion. Archive for Mathematical Logic, 27:177–188, 1988.

Recent BRICS Report Series Publications

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.

RS-01-40 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. October 2001. 9 pp.

RS-01-39 Olivier Danvy and Mayer Goldberg. There and Back Again. October 2001. 14 pp.

RS-01-38 Zoltán Ésik. Free De Morgan Bisemigroups and Bisemilattices. October 2001. 13 pp.

RS-01-37 Ronald Cramer and Victor Shoup. Universal Hash Proofs and a Paradigm for Adaptive Chosen Ciphertext Secure Public-Key Encryption. October 2001. 34 pp.

RS-01-36 Gerth Stølting Brodal, Rolf Fagerberg, and Riko Jacob. Cache Oblivious Search Trees via Binary Trees of Small Height. October 2001.

RS-01-35 Mayer Goldberg. A General Schema for Constructing One-Point Bases in the Lambda Calculus. September 2001. 6 pp.

RS-01-34 Flemming Friche Rodler and Rasmus Pagh. Fast Random Access to Wavelet Compressed Volumetric Data Using Hashing. August 2001. 31 pp.