Lower bounds for RAMs and quantifier elimination
Miklós Ajtai · 2013
For each natural number d we consider a finite structure Md whose universe is the set of all 0,1-sequence of length n=2d, each representing a natural number in the set {0,1,...,2n-1} in binary form. The operations included in the structure are the four constants 0,1,2n-1,n, multiplication and addition modulo 2n, the unary function min{2x, 2n-1}, the binary functions ⌊ x/y⌋ (with ⌊ x/0 ⌋ =0), max(x,y), min(x,y), and the boolean vector operations, vee,- defined on 0,1 sequences of length n, by performing the operations on all components simultaneously. These are essentially the arithmetic operations that can be performed on a RAM, with wordlength n, by a single instruction. We show that there exists an ε>0 and a term (that is, an algebraic expression) F(x,y) built up from the mentioned operations, with the only free variables x,y, such that if Gd(y), d=0,1,2,..., is a sequence of terms, and for all d=0,1,2,..., Md models ∀ x, [Gd(x)-> ∃ y, F(x,y)=0], then for infinitely many integers d, the depth of the term Gd, that is, the maximal number of nestings of the operations in it, is at least ε (log d)1/2 = ε (log log n)1/2.