A Nonasymptotic Lower Time Bound for a Strictly Bounded Second Order Arithmetic
by
Anatoly Beltiukov
Udmurt State University

The most of complexity theory results concerning computational complexity lower bounds are essentially asymptotical and refers to models of computations that are far from real computers (see for example [1]). Though practical tasks of evaluating complexity should deal with realistic computer models, realistic data and time bounds. Asymptotical bounds may not be appropriate for them. They may give nonrealistic coefficients or nonrealistic bounds for input data. For example, the lower time bound 1000nlog₂n is asymptotically worse than n(log₂n)², but it is not so in practical sense.

This work gives an example of realistic nonasymptotic lower bound. The task under consideration is evaluating some bounded formulas of second order arithmetic and the considered computer model is a modification of RASP [2].

The considered abstract computer model is a modification of RASP [2]. We call it minimal random access machine with stored program (MRASP). It consists of a potentially infinite sequence of registers (cells): R[0], R[1], R[2], R[3], ... Each register at any moment contains a natural number (nonnegative integer). The register R[0] always contains the modified difference between R[2] and R[3], i. e. if the content of R[2] is greater than the content of R[3], then R[0]=R[2]-R[3], else R[0] contains 0. At the beginning of the work the registers from R[1] until some R[p] are loaded by a natural number sequence that is said to be a "program" of the computer. And the registers from R[p+2] until R[p+q+1] contain input data of the program. The register R[p+1] contains the maximal address (cell number) that is used at the beginning of the work: p+q+1. All other registers contain zeroes.

The computer executes the following actions (in a potentially endless loop):

1) R[R[R[1]]]:=R[R[R[1]-1]];

2) if the previous action did not write to the register R[1] (i. e. R[R[1]] did not contain 1), then R[1]:=R[1]-2;

3) R[0]:=R[2]-R[3].

All the differences here are modified, i. e. negative results are replaced by zeroes. Here R[1] is the ïnstruction address register" and any instruction is an instruction of data moving and consists of two addresses: R[R[1]] and R[R[1]-1]. The first of them is the address of the recipient cell. The second one is the address of the source cell. Instructions are executed in the order of address decreasing. It is not hard to simulate go to m and

if R[x]=0 then go to m

commands.

Halt command is simulated by the command that changes nothing. For example,

R[I]=1;R[i-1]=iaddr,

where R[iaddr] contains the number i.

If the program computes a natural number valued function, then the result at executing "halt" command is in the register R[0]. If the program checks some condition then it places 1 or 0 into the register R[0] at the end of the work. If R[0] contains 1, then the conditions holds, otherwise the register R[0] contains 0.

Let us consider the bounded theory of natural numbers with modified subtraction, "minimal bounded second order arithmetic" (MBA). The theory contains constants for denoting natural numbers (constants are written in the form ci, where symbol c is the indication of a constant, and i is the constant value that is considered as indivisible symbol also), object and functional variables (they are written as xji, where x is letter, j is its arity, if j=0, then it is an object variable, i is the number of variable with the given number of arguments, the sign of (modified) subtraction "-" (a binary functional constant), the signs of relations " < " and "=" (binary predicates), the negation sign "\lnot", the implication sign "= > ", conjunction sign "&", the signs of the bounded quantifiers: "A" and "E".

Let us consider formulas with one free unary functional variable and bounded values of this variable. Choose natural numbers as codes for all the symbols of the theory. A formula is coded as the sequence of the consisting symbol codes. The formula can contain only one free variable: unary functional variable. It is the parameter of the formula. A (bounded) value of the parameter is coded as follows. Let f be a value of the parameter. It is not 0 only for natural arguments from 0 to n. Then the code of this value is the sequence f(0), f(1), ..., f(n). All other values are equal to 0. The entire input data sequence for the recognition is the concatenation of the formula code and the parameter value code.

It is not hard to build a MBA formula that describes work of MRASP. The formula will contain unique unary parameter F, the sense of which is a code of an initial memory content. At the beginning of the work the storage of the described machine is supposed to contain a sequence

f(1), ..., f(f(0)), f(0), f(1), ..., f(f(0))

(the next registers contain zeroes), which is coded by the formula parameter value f: f(0), f(1), .., f(f(0)). The sense of the formula G_N(F) is the following: MRASP with the given initial content of the storage has 0 in the register R₀ at the step number N.

It is not hard to build such the formula so that its length is not greater than 400. Denote this length by C.

THEOREM. For any natural N, if the truth value of the formula G_N with parameter F is recognized by a program P (with the length p), then a such value f of the parameter F can be built (with the length not more than p+C+2), that the program P will work at this input during not less than N+1 steps.

This work is supported by INTAS grant N 2000-447.

[1] A. R. Meyer: Weak monadic second order theory of successor is not elementary recursive. Preliminary Report, 1973.

[2] A. V. Aho, J. E. Hopcroft, J. D. Ullman: The Design and Analysis of Computer Algorithms 1976.

Date received: March 15, 2003