DSPACE[n^k] = VAR[k+1]

In this paper we prove that the set of properties checkable by a Turing machine in DSPACE[n k ] is exactly equal to the set of properties describable by a uniform sequence of first-order sentences using at most k + 1 distinct variables. We prove that this is also equal to the set of properties describable using an iterative definition for a finite set of relations of arity k. This is a refinement of the theorem PSPACE = VAR[O[1]] [I82]. We suggest some directions for exploiting this result to derive trade-offs between the number of variables and the quantifier-depth in desciptive complexity. This has applications to parallel complexity. 1 Introduction In Descriptive Complexity one analyzes the complexity of a language in terms of the complexity of describing the language. It is known that the quantifier-depth and number of variables needed to express the membership property of a language is closely related to the parallel time and amount of hardware needed to check whether an input ..