Descriptive Complexity of Deterministic Polylogarithmic Time and Space

TL;DR

This paper introduces a logical framework that characterizes problems solvable in deterministic polylogarithmic time and space, providing new insights into the descriptive complexity of these classes.

Contribution

It presents a novel two-sorted logic capturing PolylogTime and PolylogSpace, along with a variant of random-access Turing machines for finite ordered structures.

Findings

Logic captures PolylogTime and PolylogSpace classes.

Introduces a random-access Turing machine model.

Highlights open problems in order-invariant queries.

Abstract

We propose logical characterizations of problems solvable in deterministic polylogarithmic time (PolylogTime) and polylogarithmic space (PolylogSpace). We introduce a novel two-sorted logic that separates the elements of the input domain from the bit positions needed to address these elements. We prove that the inflationary and partial fixed point vartiants of this logic capture PolylogTime and PolylogSpace, respectively. In the course of proving that our logic indeed captures PolylogTime on finite ordered structures, we introduce a variant of random-access Turing machines that can access the relations and functions of a structure directly. We investigate whether an explicit predicate for the ordering of the domain is needed in our PolylogTime logic. Finally, we present the open problem of finding an exact characterization of order-invariant queries in PolylogTime.

Equations

$$\sigma =\{R_1^{r_1},\dots ,R_p^{r_p},c_1,\dots c_q,f_1^{k_1},\dots ,f_s^{k_s}\},$$

$$\mathrm{PolylogTime}=\bigcup _{k\in \mathbb{N}}\mathrm{DTIME}[{\log }^{k}n]$$

$${\delta }_Q:Q\times {\Sigma }^m\times \{0,1{\}}^p\to Q.$$

$${\delta }_l:Q\times {\Sigma }^m\times \{0,1{\}}^p\to \Sigma \times \{\leftarrow ,\to ,-\}.$$

$${\delta }_l:Q\times {\Sigma }^m\times \{0,1{\}}^p\to \{\leftarrow ,\to ,-\}.$$

$$n^{r_1}+\cdots +n^{r_p}+q\lceil \log n\rceil +\lceil \log n\rceil n^{k_1}+\cdots +\lceil \log n\rceil n^{k_s}.$$

$$t::=x\mid c\mid f(t,\dots ,t),$$

$$\begin{gathered} \phi ::=t_1\le t_2\mid {\mathtt{x}}_1\le {\mathtt{x}}_2\mid R(t_1,\dots ,t_k)\mid X({\mathtt{x}}_1,\dots ,{\mathtt{x}}_k)\mid (\phi \wedge \phi )\mid \neg \phi \mid [{\mathrm{IFP}}_{\bar{\mathtt{x}},X}\phi ]\bar{\mathtt{y}}\mid \\ t=index\{\mathtt{x}:\phi (\mathtt{x})\}\mid \exists x(x=index\{\mathtt{x}:\alpha (\mathtt{x})\}\wedge \phi )\mid \exists \mathtt{x}\phi , \end{gathered}$$

$$F_{\phi ,\bar{\mathtt{x}},X}^{\mathbf{A},val}(S):=\{\bar{a}\in (\text{Num}(\mathbf{A}){)}^k\mid \mathbf{A},val(S/X,\bar{a}/\bar{\mathtt{x}})\models \phi (X,\bar{\mathtt{x}}).$$

$${\phi }_Z$$

$${\phi }_Y$$

$$\exists x(x<N\wedge K(x)=T).$$

$$\psi (\mathtt{l})$$

$${\phi }_Z$$

$${\phi }_L$$

$${\phi }_R$$

$$F_{\psi ,\bar{\mathtt{x}},X}^{\mathbf{A},val}(S):=\{\bar{a}\in (\text{Num}(\mathbf{A}){)}^k\mid \mathbf{A},val(S/X,\bar{a}/\bar{\mathtt{x}})\models \psi (X,\bar{\mathtt{x}})\}.$$

$$\mathbf{A},val(S/X,\bar{a}/\bar{\mathtt{x}})\models \psi (X,\bar{\mathtt{x}})$$

$$\exists\mathtt{x}_{0}\ldots\mathtt{x}_{k-1}\big{(}[\textrm{S-IFP}_{\bar{t},S_{q_{a}},\mathrm{A},\mathrm{B}_{1},\mathrm{B}_{2},\mathrm{B}_{3},\mathrm{C}}\;\varphi_{q_{a}},\Phi_{\mathrm{A}},\Phi_{\mathrm{B}_{1}},\Phi_{\mathrm{B}_{2}},\Phi_{\mathrm{B}_{3}},\Phi_{\mathrm{C}}](\mathtt{x}_{0},\ldots,\mathtt{x}_{k-1})\big{)},$$

$$\mathrm{A}=\bar{t},S_{q_0},\dots ,\bar{t},S_{q_{a-1}}{\mathrm{B}}_1=\bar{p}\bar{t},T_1^0,\dots ,\bar{p}\bar{t},T_m^0{\mathrm{B}}_2=\bar{p}\bar{t},T_1^1,\dots ,\bar{p}\bar{t},T_m^1$$

$${\mathrm{B}}_3=\bar{p}\bar{t},T_1^{\bigsqcup },\dots ,\bar{p}\bar{t},T_m^{\bigsqcup }\mathrm{C}=\bar{p}\bar{t},H_1,\dots ,\bar{p}\bar{t},H_m$$

$${\Phi }_{\mathrm{A}}={\phi }_{q_0},\dots ,{\phi }_{q_{a-1}}{\Phi }_{{\mathrm{B}}_1}={\psi }_{01},\dots ,{\psi }_{0m}{\Phi }_{{\mathrm{B}}_2}={\psi }_{11},\dots ,{\psi }_{1m}$$

$${\Phi }_{{\mathrm{B}}_3}={\psi }_{\bigsqcup 1},\dots ,{\psi }_{\bigsqcup m}{\Phi }_{\mathrm{C}}={\gamma }_1,\dots ,{\gamma }_m.$$

$$\neg (\bar{t}\sim 0)\wedge {\alpha }_i^0(\bar{p},\bar{t}-1),$$

$$\displaystyle\exists\bar{p}_{1}\dots\bar{p}_{i-1}\bar{p}_{i+1}\dots\bar{p}_{m}\Big{(}S_{q}(\bar{t}-1)\wedge$$

$$\displaystyle\big{(}\bigwedge_{1\leq j\leq m}H_{j}(\bar{p}_{j},\bar{t}-1)\wedge T^{a_{j}}_{j}(\bar{p}_{j},\bar{t}-1)\big{)}\wedge$$

$$\displaystyle\bigwedge_{1\leq l\leq p}\exists x_{1}\ldots x_{r_{l}}\big{(}\mathrm{check}(R_{l}(x_{1},\ldots,x_{r_{l}}),b_{l})\land$$

$$\displaystyle\quad\bigwedge_{1\leq k\leq r_{l}}x_{k}=\mathit{index}\{\mathtt{x}\mid(T^{1}_{\tau^{R}_{l,k}}(\mathtt{x},\bar{t}-1))\}\big{)}\Big{)},$$

$$\displaystyle\exists x_{1}\ldots x_{k_{j}}\Big{(}\big{(}\bigwedge_{1\leq l\leq k_{j}}x_{l}=\mathit{index}\{\mathtt{x}\mid T^{1}_{\tau^{f}_{j,l}}({\tt x},\bar{t})\}\big{)}\land\neg\mathrm{BIT}(f_{j}(x_{1},\ldots,x_{k_{j}}),p)\Big{)},$$

$$(\bar{t}\sim 0\wedge\bar{p}\sim 0)\vee\big{(}\neg(\bar{t}\sim 0)\wedge\alpha_{i}(\bar{p},\bar{t}-1)\big{)},$$

$$s^{\prime }:=\underset{\text{i times}}{\underbrace{0\dots 0}}1\underset{\text{n−i−1 times}}{\underbrace{0\dots 0}}.$$

$$\mathbf{A},val\models \phi \text{ if and only if }l<m.$$

$${\mathfrak{C}}_i=\{\mathbf{B}\in \mathfrak{C}\mid \forall j\in {\mathrm{Ins}}^i(\mathrm{bin}({\mathbf{A}}_i))\text{ the jth bit of bin(B) is 0}\}.$$

Full text

††journal: Journal of Computer and System Sciences

1 Introduction

The research area known as Descriptive Complexity [1, 2, 3] relates computational complexity to logic. For a complexity class of interest, one tries to come up with a natural logic such that a property of inputs can be expressed in the logic if and only if the problem of checking the property belongs to the complexity class. An exemplary result in this vein is that a family $\cal F$ of finite structures (over some fixed finite vocabulary) is definable in existential second-order logic (ESO), if and only if the membership problem for $\cal F$ belongs to NP [4]. We also say that ESO captures NP. The complexity class P is captured, on ordered finite structures, by a fixed point logic: the extensions of first-order logic with least fixed points [5, 6].

After these two seminal results, many more capturing results have been developed, and the benefits of this enterprise has been well articulated by several authors in the references given earlier, and others [7]. We just mention here the advantage of being able to specify properties of structures (e.g., data structures and databases) in a logical, declarative manner; at the same time, we are guaranteed that our computational power is well delineated.

The focus of the present paper is on computations taking deterministic polylogarithmic time, i.e., time proportional to $(\log n)^{k}$ for some arbitrary but fixed $k$. Such computations are practically relevant and common on ordered structures. Well known examples are binary search in an array or search in a balanced search tree. Another natural example is the computation of $f(x_{1},\dots,x_{r})$, where $x_{1}$, …, $x_{r}$ are numbers taken from the input structure and $f$ is a function computable in polynomial time when numbers are represented in binary.

Computations with sublinear time complexity can be formalized in terms of Turing machines with random access to the input [3]. When a family $\cal F$ of ordered finite structures over some fixed finite vocabulary is defined by some deterministic polylogarithmic-time random-access Turing machine, we say that $\cal F$ belongs to the complexity class $\mathrm{PolylogTime}$. In this paper, we show how this complexity class can be captured by a new logic which we call index logic.

Index logic is two-sorted; variables of the first sort range over the domain of the input structure. Variables of the second sort range over an initial segment of the natural numbers; this segment is bounded by the logarithm of the size of the input structure. Thus, the elements of the second sort represent the bit positions needed to address elements of the first sort. Index logic includes full fixed point logic on the second sort. Quantification over the first sort, however, is heavily restricted. Specifically, a variable of the first sort can only be bound using an address specified by a subformula that defines the positions of the bits of the address that are set. This “indexing mechanism” lends index logic its name.

In the course of proving our capturing result, we consider a new variant of random-access Turing machines. In the standard variant, the entire input structure is presented as one binary string. In our new variant, the different relations and functions of the structure can be accessed directly. We will show that both variants are equivalent, in the sense that they lead to the same notion of $\mathrm{PolylogTime}$. We note that, in descriptive complexity, it is a common practice to work only with relational structures, as functions can be identified with their graphs. In a sublinear-time setting, however, this does not work. Indeed, let $f$ be a function and denote its graph by $\tilde{f}$. If we want to know the value of $f(x)$, we cannot spend the linear time needed to find a $y$ such that $\tilde{f}(x,y)$ holds. Thus, in this work, we allow structures containing functions as well as relations.

We also devote attention to gaining a detailed understanding of the expressivity of index logic. Specifically, we observe that order comparisons between quantified variables of the first sort can be expressed in terms of their addresses. For constants of the first sort that are directly given by the structure, however, we show that this is not possible. In other words, index logic without an explicit order predicate on the first sort would no longer capture $\mathrm{PolylogTime}$ for structures with constants.

Finally, we introduce a variant of index logic with partial fixed point operators and show that it captures $\mathrm{PolylogSpace}$. This result is analogous to the classical result regarding the descriptive complexity of PSPACE, which is captured over ordered structures by first-order logic with the addition of partial fixed point operators [8]. For consistency, we define $\mathrm{PolylogSpace}$ using the model of direct-access Turing machines, i.e., the variant of the random-access Turing machine that we introduce in this paper. As with $\mathrm{PolylogTime}$, both models of computation lead to the same notion of $\mathrm{PolylogSpace}$. Moreover, we show that, in the case of $\mathrm{PolylogSpace}$, random-access to the input-tape can be replaced with sequential-access without having any impact on the complexity class. Similar to PSPACE, the nondeterministic and deterministic $\mathrm{PolylogSpace}$ classes coincide. It is interesting to note that beyond the problems in nondeterministic logarithmic space, there are well known natural problems that belong to $\mathrm{PolylogSpace}$ (see examples below, under related work).

A preliminary version of this paper was presented at the 26th International Workshop in Logic, Language, Information, and Computation [9]. This is an extended improved version which in addition to the full proofs of the results on deterministic polylogarithmic time reported in [9], also considers polylogarithmic space and its descriptive characterization in terms of a variant of index logic.

Related work

Many natural fixed point computations, such as transitive closure, converge after a polylogarithmic number of steps. This motivated the study in [10] of a fragment of fixed point logic with counting (FPC) that only allows polylogarithmically many iterations of the fixed point operators (polylog-FPC). They noted that on ordered structures polylog-FPC captures NC, i.e., the class of problems solvable in parallel polylogarithmic time. This holds even in the absence of counting, which on ordered structures can be simulated using fixed point operators. Moreover, an old result in [11] directly implies that polylog-FPC is strictly weaker than FPC with regards to expressive power.

It is well known that the (nondeterministic) logarithmic time hierarchy corresponds exactly to the set of first-order definable Boolean queries (see [3], Theorem 5.30). The relationship between uniform families of circuits within NC1 and nondeterministic random-access logarithmic time machines was studied in [12]. However, the study of descriptive complexity of classes of problems decidable by deterministic formal models of computation in polylogarithmic time, i.e., the central topic of this paper, has been overlooked by previous works.

On the other hand, nondeterministic polylogarithmic time complexity classes, defined in terms of alternating random-access Turing machines and related families of circuits, have received some attention [13, 14]. Recently, a theorem analogous to Fagin’s famous theorem [4], was proven for nondeterministic polylogarithmic time [14]. For this task, a restricted second-order logic for finite structures, where second-order quantification ranges over relations of size at most polylogarithmic in the size of the structure, and where first-order universal quantification is bounded to those relations, was exploited. This latter work, is closely related to the work on constant depth quasi-polynomial size AND/OR circuits and the corresponding restricted second-order logic in [13]. Both logics capture the full alternating polylogarithmic time hierarchy, but the additional restriction in the first-order universal quantification in the second-order logic defined in [14], enables a one-to-one correspondence between the levels of the polylogarithmic time hierarchy and the prenex fragments of the logic, in the style of a result of Stockmeyer [15] regarding the polynomial-time hierarchy. Unlike the classical results of Fagin and Stockmeyer [4, 15], the results on the descriptive complexity of nondeterministic polylogarithmic time classes only hold over ordered structures.

Up to the authors knowledge, very little is known regarding the relationship of $\mathrm{PolylogSpace}$ with the main classical complexity classes (see [16] and [17]). As usual, let $\mathrm{L}$ and $\mathrm{NL}$ denote deterministic and nondeterministic logarithmic space, respectively. Further, let $\mathrm{L}^{j}$ denote $\mathrm{DSPACE}[(\left\lceil\log n\right\rceil)^{j}]$. The following relations are known:

1. (i)

$\mathrm{PolylogSpace}\neq\mathrm{P}$, and it is unknown whether $\mathrm{PolylogSpace}\subseteq\mathrm{P}$. 2. (ii)

$\mathrm{PolylogSpace}\neq\mathrm{NP}$, and it is unknown whether $\mathrm{PolylogSpace}\subseteq\mathrm{NP}$. 3. (iii)

Obviously: $\mathrm{L}\subseteq\mathrm{NL}\subseteq\mathrm{L}^{2}\subseteq\mathrm{PolylogSpace}\subseteq\mathrm{DTIME}[2^{(\left\lceil\log n\right\rceil)^{O(1)}}]$, the latter class being known as quasi-polynomial time ($\mathrm{QuasiP}$). 4. (iv)

For all $i\geq j\geq 1$, $\mathrm{L}^{j}$ uniform $\mathrm{NC^{i}}$ $\subseteq\mathrm{L}^{i}$ (see [18]); hence we have that $\mathrm{PolylogSpace}$ $\mathrm{uniform}$ $\mathrm{NC}$ $\subseteq\mathrm{PolylogSpace}$. 5. (v)

For all $i\geq 1$, let $\mathrm{SC}^{i}:=\mathrm{DTIME{-}DSPACE}(n^{O(1)},(\log n)^{i})$ and let $\mathrm{SC}:=\bigcup_{i\in\mathbb{N}}\mathrm{SC^{i}}$ (see [19]). It follows that $\mathrm{PolylogSpace}=\mathrm{SC}\cap\mathrm{P}$.

Some interesting natural problems in $\mathrm{PolylogSpace}$ which are not known to be in $\mathrm{NL}$ follow. By item (iv) above, we get that division, exponentiation, iterated multiplication of integers [20], and integer matrix operations, such as exponentiation, computation of the determinant, rank and the characteristic polynomial (see [21] and [22] for detailed algorithms in $\mathrm{L}^{2}$), are all in $\mathrm{PolylogSpace}$. Other well-known problems in the class are $k$-colorability of graphs of bounded tree-width [23], primality, 3NF test, BCNF test for relational schemas of bounded tree-width [24, 25], and the circuit value problem of only EXOR gates [16]. Finally, in [26] an interesting family of problems is presented. It is shown that, for every $k\geq 1$, there is an algebra $(S;+,.)$ over matrices such that the depth $O(\log n)^{k}$ straight linear formula problem over $M(S;+,.)$ is $\mathrm{NC}^{k+1}$ complete under $\mathrm{L}$ reducibility. Now, by (iv) above, these problems are in $\mathrm{DSPACE}[(\log n)^{k+1}]$.

2 Preliminaries

We allow structures containing functions as well as relations and constants. Unless otherwise stated, we work with finite ordered structures of finite vocabularies. A finite structure $\bf A$ of vocabulary

[TABLE]

where each $R^{r_{i}}_{i}$ is an $r_{i}$-ary relation symbol, each $c_{i}$ is a constant symbol, and each $f^{k_{i}}_{i}$ is a $k_{i}$-ary function symbol, consists of a finite domain $A$ and interpretations for all relation, constant, and function symbols in $\sigma$. An interpretation of a symbol $R^{r_{i}}_{i}$ is a relation $R^{\bf A}_{i}\subseteq A^{r_{i}}$, of a symbol $c_{i}$ is a value $c_{i}^{\bf A}\in A$, and of a symbol $f^{k_{i}}_{i}$ is a function $f^{\bf A}_{i}:A^{k_{i}}\rightarrow A$. A finite ordered $\sigma$-structure $\mathbf{A}$ is a finite structure of vocabulary $\sigma\cup\{\leq\}$, where $\leq\notin\sigma$ is a binary relation symbol and $\leq^{\mathbf{A}}$ is a linear order on $A$. Every finite ordered structure has a corresponding isomorphic structure, whose domain is an initial segment of the natural numbers. Thus, we assume, as usual, that $A=\{0,1,\ldots,n-1\}$, where $n$ is the cardinality $|A|$ of $A$.

In this paper, $\log n$ always refers to the binary logarithm of $n$, i.e., $\log_{2}n$. We write $\log^{k}n$ as a shorthand for $(\left\lceil\log n\right\rceil)^{k}$. A tuple of elements $(a_{1},\dots,a_{k})$ is sometimes written as $\bar{a}$. We then use $\bar{a}[i]$ to denote the $i$-th element of the tuple. Similarly, if $s$ is a finite string, we denote by $s[i]$ the $i$-th letter of this string.

3 Deterministic polylogarithmic time

The sequential access that Turing machines have to their tapes restrict sub-linear time computations to depend only on the first sub-linear bits of the input; there is now way to access an arbitrary bit of the input. Therefore, logarithmic time complexity classes are usually studied using models of computation that have random-access222The term random-access refers to the manner how random-access memory (RAM) is read and written. In contrast to sequential memory, the time it takes to read or write using RAM is almost independent of the physical location of the data in the memory. We want to emphasise that there is nothing random in random-access. to their input, i.e., that can access every input address directly. As this also applies to polylogarithmic time, we adopt a Turing machine model that has a random-access read-only input, similar to the logarithmic-time Turing machine in [12].

Our concept of a random-access Turing machine is that of a multi-tape Turing machine which consists of: (1) a finite set of states, (2) a read-only random access input-tape, (3) a sequential access address-tape, and (4) one or more (but a fixed number of) sequential access work-tapes. All tapes are divided into cells, each equipped with a tape head which scans the cells, and are “semi-infinite” in the sense that they have no rightmost cell, but have a leftmost cell. The tape heads of the sequential access address-tape and work-tapes can move left or right. When a head is in the leftmost cell, it is not allowed to move left. The address-tape alphabet only contains symbols [math], $1$ and $\sqcup$ (for blank). The position of the input-tape head is determined by the number $i$ stored in binary between the leftmost cell and the first blank cell of the address-tape (if the leftmost cell is blank, then $i$ is considered to be [math]) as follows: If $i$ is strictly smaller than the length $n$ of the input string, then the input-tape head is in the $(i+1)$-th cell. Otherwise, if $i\geq n$, then the input-tape head is in the $(n+1)$-th cell scanning the special end-marker symbol $\triangleleft$.

Formally, a random-access Turing machine $M$ with $k$ work-tapes is a five-tuple $(Q,\Sigma,\delta,q_{0},F)$. Here $Q$ is a finite set of states; $q_{0}\in Q$ is the initial state. $\Sigma$ is a finite set of symbols (the alphabet of $M$). For simplicity, we fix $\Sigma=\{0,1,\sqcup\}$. $F\subseteq Q$ is the set of accepting final states. The transition function of $M$ is of the form $\delta:Q\times(\Sigma\cup\{\triangleleft\})\times\Sigma^{k+1}\rightarrow Q\times(\Sigma\times\{\leftarrow,\rightarrow,-\})^{k+1}$. We assume that the tape head directions $\leftarrow$ for “left”, $\rightarrow$ for “right” and $-$ for “stay”, are not in $Q\cup\Sigma$.

Intuitively, $\delta(q,a_{1},a_{2},\ldots,a_{k+2})=(p,b_{2},D_{2},\ldots,b_{k+2},D_{k+2})$ means that, if $M$ is in the state $q$, the input-tape head is scanning $a_{1}$, the index-tape head is scanning $a_{2}$, and for every $i=1,\ldots,k$ the head of the $i$-th work-tape is scanning $a_{i+2}$, then the next state will be $p$, the index-tape head will write $b_{2}$ and move in the direction indicated by $D_{2}$, and for every $i=1,\ldots,k$ the head of the $i$-th work-tape will write $b_{i+2}$ and move in the direction indicated by $D_{i+2}$. Situations in which the transition function is undefined indicate that the computation must stop. Observe that $\delta$ cannot change the contents of the input tape.

A configuration of $M$ on a fixed input $w_{0}$ is a $k+2$ tuple $(q,i,w_{1},\ldots,w_{k})$, where $q$ is the current state of $M$, $i\in\Sigma^{*}\#\Sigma^{*}$ represents the current contents of the index-tape cells, and each $w_{j}\in\Sigma^{*}\#\Sigma^{*}$ represents the current contents of the $j$-th work-tape cells. We do not include the contents of the input-tape cells in the configuration since they cannot be changed. Further, the position of the input-tape head is uniquely determined by the contents of the index-tape cells. The symbol $\#$ (which we assume is not in $\Sigma$) marks the position of the corresponding tape head. By convention, the head scans the symbol immediately at the right of $\#$. All symbols in the infinite tapes not appearing in their corresponding strings $i,w_{0},\ldots,w_{k}$ are assumed to be the designated symbol for blank $\sqcup$.

At the beginning of a computation all work-tapes are blank, except the input-tape, that contains the input string, and the index-tape that contains a [math] (meaning that the input-tape head scans the first cell of the input-tape). Thus, the initial configuration of $M$ is $(q_{0},\#0,\#,\ldots,\#)$. A computation is a (possibly infinite) sequence of configurations which starts with the initial configuration and, for every two consecutive configurations, the latter is obtained by applying the transition function of $M$ to the former. An input string is accepted if an accepting configuration, i.e., a configuration in which the current state belongs to $F$, is reached.

Example 1**.**

Following a simple strategy, a random-access Turing machine $M$ can figure out the length $n$ of its input as well as $\lceil\log n\rceil$ in polylogarithmic time. In its initial step, $M$ checks whether the input-tape head scans the end-marker $\triangleleft$. If it does, then the input string is the empty string and its work is done. Otherwise, $M$ writes $1$ in the first cell of its address tape and keeps writing [math]’s in its subsequent cells right up until the input-tape head scans $\triangleleft$. It then rewrites the last [math] back to the blank symbol $\sqcup$. At this point the resulting binary string in the index-tape is of length $\lceil\log n\rceil$. Next, $M$ moves its address-tape head back to the first cell (i.e., to the only cell containing a $1$ at this point). From here on, $M$ repeatedly moves the index head one step to the right. Each time it checks whether the index-tape head scans a blank $\sqcup$ or a [math]. If $\sqcup$ then $M$ is done. If [math], it writes a $1$ and tests whether the input-tape head jumps to the cell with $\triangleleft$; if so, it rewrites a [math], otherwise, it leaves the $1$. The binary number left on the index-tape at the end of this process is $n-1$. Adding one in binary is now an easy task. ∎

The formal language accepted by a machine $M$, denoted $L(M)$, is the set of strings accepted by $M$. We say that $L(M)\in\mathrm{DTIME}[f(n)]$ if $M$ makes at most $O(f(n))$ steps before accepting or rejecting an input string of length $n$. We define the class of all formal languages decidable by (deterministic) random-access Turing machines in polylogarithmic time as follows:

[TABLE]

It follows from Example 1 that a $\mathrm{PolylogTime}$ random-access Turing machine can check any numerical property that is polynomial time in the size of its input in binary. For instance, it can check whether the length of its input is even, by simply looking at its least-significant bit.

When we want to give a finite structure as an input to a random-access Turing machine, we encode it as a string, adhering to the usual conventions in descriptive complexity theory [3]. Let $\sigma=\{R^{r_{1}}_{1},\ldots,R^{r_{p}}_{p},c_{1},\ldots,c_{q},f^{k_{1}}_{1},\ldots,f^{k_{s}}_{s}\}$ be a vocabulary, and let ${\bf A}$ with $A=\{0,1,{\dots},{n{-}1}\}$ be an ordered structure of vocabulary $\sigma$. Note that the order on $A$ can be used to define an order for tuples of elements of $A$ as well. Each relation $R_{i}^{\bf A}\subseteq A^{r_{i}}$ of $\bf A$ is encoded as a binary string $\mathrm{bin}(R^{\bf A}_{i})$ of length $n^{r_{i}}$, where $1$ in a given position $m$ indicates that the $m$-th tuple of $A^{r_{i}}$ is in $R_{i}^{\textbf{A}}$. Likewise, each constant number $c^{\bf A}_{j}$ is encoded as a binary string $\mathrm{bin}(c^{\bf A}_{j})$ of length $\lceil\log n\rceil$.

We also need to encode the functions of a structure. We view $k$-ary functions as consisting of $\lceil\log n\rceil$ many $k$-ary relations, where the $m$-th relation indicates whether the $m$-th bit of the value of the function is $1$. Thus, each function $f^{\bf A}_{i}$ is encoded as a binary string $\mathrm{bin}(f^{\bf A}_{i})$ of length $\lceil\log n\rceil n^{k_{i}}$.

The encoding of the whole structure $\mathrm{bin}(\textbf{A})$ is the concatenation of the binary strings encoding its relations, constants, and functions. The length $\hat{n}=|\mathrm{bin}(\textbf{A})|$ of this string is $n^{r_{1}}+\cdots+n^{r_{p}}+q\lceil\log n\rceil+\lceil\log n\rceil n^{k_{1}}+\cdots+\lceil\log n\rceil n^{k_{s}}$, where $n=|A|$ denotes the size of the input structure ${\bf A}$. Note that $\log\hat{n}\in O(\lceil\log n\rceil)$, and hence $\mathrm{DTIME}[\log^{k}\hat{n}]=\mathrm{DTIME}[\log^{k}n]$.

4 Direct-access Turing machines

In this section, we propose a new model of random-access Turing machines. In the standard model reviewed above, the entire input structure is assumed to be encoded as one binary string. In our new variant, the different relations and functions of the structure can be accessed directly. We then show that both variants are equivalent, in the sense that they lead to the same notion of $\mathrm{PolylogTime}$. The direct-access model will then be useful to give a transparent proof of our capturing result.

Let $\sigma=\{R^{r_{1}}_{1},\ldots,R^{r_{p}}_{p},c_{1},\ldots c_{q},f^{k_{1}}_{1},\ldots,f^{k_{s}}_{s}\}$ be a vocabulary. A direct-access Turing machine that takes $\sigma$-structures $\mathbf{A}$ as an input, is a multitape Turing machine with $r_{1}+\cdots+r_{p}+k_{1}+\dots+k_{s}$ distinguished work-tapes, called address-tapes, $s$ distinguished read-only (function) value-tapes, $q+1$ distinguished read-only constant-tapes, and one or more ordinary work-tapes.

Let us define a transition function $\delta_{l}$ for each tape $l$ separately. These transition functions take as an input the current state of the machine, the bit read by each of the heads of the machine, and, for each relation $R_{i}\in\sigma$, the answer (0 or 1) to the query $(n_{1},\dots,n_{r_{i}})\in R^{\mathbf{A}}_{i}$. Here, $n_{j}$ denotes the number written in binary in the $j$th distinguished tape of $R_{i}$.

Thus, with $m$ the total number of tapes, the state transition function has the form

[TABLE]

If $l$ corresponds to an address-tape or an ordinary work-tape, we get the form

[TABLE]

If $l$ corresponds to one of the read-only tapes, we have

[TABLE]

Finally we update the contents of the function value-tapes. If $l$ is the function value-tape for a function $f_{i}$, then the content of the tape $l$ is updated to $f^{\mathbf{A}}_{i}(n_{1},\dots n_{k_{i}})$ written in binary. Here, $n_{j}$ denotes the number written in binary in the $j$th distinguished address-tape of $f_{i}$ after the execution of the above transition functions. If one of the $n_{j}$ is too large, the tape $l$ is updated to contain only blanks. Note that the head of the tape remains in place; it was moved by $\delta_{l}$ already.

In the initial configuration, read-only constant-tapes for the constant symbols $c_{1},\ldots,c_{q}$ hold their values in ${\bf A}$ in binary. One additional constant-tape (there are $q+1$ of them) holds the size $n$ of the domain of ${\bf A}$ in binary. Each address-tape, each value-tape, and each ordinary work-tape holds only blanks.

Theorem 1**.**

A class of finite ordered structures $\cal C$ of some fixed vocabulary $\sigma$ is decidable by a random-access Turing machine working in $\mathrm{PolylogTime}$ with respect to $\hat{n}$, where $\hat{n}$ is the size of the binary encoding of the input structure, iff $\cal C$ is decidable by a direct-access Turing machine in $\mathrm{PolylogTime}$ with respect to $n$, where $n$ is the size of the domain of the input structure.

Proof.

We will first sketch how a random-access Turing machine $M_{r}$ simulates a direct-access Turing machine $M_{d}$ on an input $\mathbf{A}$. Let $n$ denote the cardinality of $A$ and $\hat{n}$ the length of $\mathrm{bin}(\mathbf{A})$. We dedicate a work-tape of $M_{r}$ to every tape of $M_{d}$. In addition, for each relation $R$, we add one extra tape that will always contain the answer to the query $?R(\vec{n})$. We also use additional work-tapes for convenience. We then encode the initial configuration of $M_{d}$ into the tapes of $M_{r}$:

On the 0th constant tape, write $n$ in binary. 2. 2.

On each tape for a constant $c_{i}$, write $c_{i}^{\mathbf{A}}$ in binary. 3. 3.

For the answer-tapes of relations $R_{i}$, write the bit [math].

For encoding the transitions of $M_{d}$, we will in addition need two more constructs:

1. a.

Updating the answer-tapes of relations after each transition. 2. b.

Updating the answer-tapes of functions after each transition.

We now need to verify that these procedures (3. is trivial) can be performed by $M_{r}$ in polylogarithmic time with respect to $\hat{n}$.

Step 1. On a fixed vocabulary $\sigma$, we have $\hat{n}=f(n)$, for some fixed function $f$ of the form

[TABLE]

We will find $n$ by executing a binary search between the numbers [math] and $\hat{n}$; note that checking whether a binary representation of a number is at most $\hat{n}$, can be checked by writing the representation to the index-tape and checking whether a bit or $\triangleleft$ is read from the input-tape. For each i between [math] and $\hat{n}$, $f(i)$ can be computed in polynomial time with respect to the length of $\hat{n}$ in binary, and thus in polylogarithmic time with respect to $\hat{n}$.

Step 2. The binary representation of a constant $c^{\mathbf{A}}_{i}$ is written in the input-tape between $g(n)$ and $g(n)+\lceil\log n\rceil$, where $g$ is a fixed function of the form $n^{r_{1}}+\cdots+n^{r_{p}}+(i-1)\lceil\log n\rceil.$ The numbers $n$ and $g(n)$ are obtained as in case 1. Then $g(n)$ is written on the index tape and the next $\lceil\log n\rceil$ bits of the input are copied to the tape corresponding to $c_{i}$.

Steps a. and b.  These cases are are handled similar to each other and to the case 2. above. The main difference for b. is that the bits of the output are not in successive positions of the input, but the location of each bit needs to be calculated separately.

We next sketch how a direct-access Turing machine $M_{d}$ simulates a random-access Turing machine $M_{r}$ on an input $\mathbf{A}$. First note that approach similar to the converse direction does not work here, as we do not have enough time to directly construct the initial configuration of $M_{r}$ inside $M_{d}$. For each work-tape of $M_{r}$, we dedicate a work-tape of $M_{d}$. For the index-tape of $M_{r}$, we dedicate a work-tape of $M_{d}$ and call it the index-tape of $M_{d}$. Moreover, we use some additional work-tapes for convenience. The idea of the simulation is that the dedicated work-tapes and the index-tape of $M_{d}$ copy exactly the behaviour of the corresponding tapes of $M_{r}$. The additional work-tapes are used to calculate to which part of the input of $M_{r}$ the index-tape refers to. After each transition of $M_{r}$ this is checked so that the machine $M_{d}$ can update its address-tapes accordingly.

Recall that given an input $\sigma=\{R^{r_{1}}_{1},\ldots,R^{r_{p}}_{p},c_{1},\ldots c_{q},f^{k_{1}}_{1},\ldots,f^{k_{s}}_{s}\}$ structure $\mathbf{A}$ of cardinality $n$, the input of $M_{r}$ is of length

[TABLE]

The number written in binary on the index-tape of $M_{r}$ determines the position of the input that is read by $M_{r}$. From (1) we obtain fixed functions on $n$, that we use in the simulation to check which part of the input is read when the index-tape holds a particular number. For example, if the index-tape holds $n^{r}_{1}+1$, we can calculate that the head of the input-tape of $M_{r}$ reads the bit answering the query: is $\vec{0}\in R_{2}^{\mathbf{A}}$. We can use an extra work-tape of $M_{d}$ to always store the bit that $M_{r}$ is reading from its input; the rest of the simulation is straightforward. ∎

5 Index logic

In this section, we introduce index logic, a new logic which over ordered finite structures captures $\mathrm{PolylogTime}$. Our definition of index logic is inspired by the second-order logic in [13], where relation variables are restricted to valuations on the sub-domain $\{0,\ldots,\lceil\log n\rceil-1\}$ ($n$ being the size of the interpreting structure), as well as by the well known counting logics as defined in [27].

Given a vocabulary $\sigma$, for every ordered $\sigma$-structure $\mathbf{A}$, we define a corresponding set of natural numbers $\textit{Num}(\mathbf{A})=\{0,\dots,\lceil\log n\rceil-1\}$ where $n=|A|$. Note that $\textit{Num}(\mathbf{A})\subseteq A$, since we assume that $A$ is an initial segment of the natural numbers. This simplifies the definitions, but it is otherwise unnecessary.

Index logic is a two-sorted logic. Individual variables of the first sort v range over the domain $A$ of $\mathbf{A}$, while individual variables of the second sort n range over $\textit{Num}(\mathbf{A})$. We denote variables of sort v with $x,y,z,\ldots$, possibly with a subindex such as $x_{0},x_{1},x_{2},\dots$, and variables of sort n with $\mathtt{x},\mathtt{y},\mathtt{z}$, also possibly with a subindex. Relation variables, denoted with uppercase letters $X,Y,Z,\ldots$, are always of sort n, and thus range over relations defined on $\textit{Num}(\mathbf{A})$.

Definition 1** (Numerical and first-order terms).**

The only terms of sort n are the variables of sort n. For a vocabulary $\sigma$, the $\sigma$-terms $t$ of sort v are generated by the following grammar:

[TABLE]

where $x$ is a variable of sort v, $c$ is a constant symbol in $\sigma$, and $f$ is a function symbol in $\sigma$.

Definition 2** (Syntax of index logic).**

Let $\sigma$ be a vocabulary. The formulae of index logic $\mathrm{IL(IFP)}$ is generated by the following grammar:

[TABLE]

where $t,t_{1},\ldots,t_{k}$ are $\sigma$-terms of sort v, ${\tt x},{\tt x}_{1},\ldots,{\tt x}_{k}$ are variables of sort n, $\bar{\mathtt{x}}$ and $\bar{{\tt y}}$ are tuples of variables of sort n whose length coincides with the arity of the relation variable $X$. Moreover, $\alpha({\tt x})$ is a formula where the variable $x$ of sort v does not occur as a free variable.

We also use the standard shorthand formulae $t_{1}=t_{2}$, ${\tt x}_{1}={\tt x}_{2}$, $(\varphi\lor\psi)$, and $\forall{\tt y}\varphi$ with the obvious meanings.

The concept of a valuation is the standard one for a two-sorted logic. Thus, a valuation over a structure $\mathbf{A}$ is any total function val from the set of all variables of index logic to values satisfying the following constraints:

• •

If $x$ is a variable of sort v, then $\mathit{val}(x)\in A$.

• •

If $\mathtt{x}$ is a variable of sort n, then $\mathit{val}(\mathtt{x})\in\textit{Num}(\mathbf{A})$.

• •

If $X$ is a relation variable with arity $r$, then $\mathit{val}(X)\subseteq(\textit{Num}(\mathbf{A}))^{r}$.

If $\chi$ is a variable and $B$ a legal value for that variable, we write $\it{val}(B/\chi)$ to denote the valuation that maps $\chi$ to $B$ and agrees with $\it{val}$ for all other variables. Valuations extend to terms and tuples of terms in the usual way.

Fixed points are defined in the standard way (see [28] and [29] among others). Given an operator $F:{\cal P}(B)\rightarrow{\cal P}(B)$, a set $S\subseteq B$ is a fixed point of $F$ if $F(S)=S$. A set $S\subseteq B$ is the least fixed point of $F$ if it is a fixed point and, for every other fixed point $S^{\prime}$ of $F$, we have $S\subseteq S^{\prime}$. We denote the least fixed point of $F$ as $\mathrm{lfp}(F)$. The inflationary fixed point of $F$, denoted by $\mathrm{ifp}(F)$, is the union of all sets $S^{i}$ where $S^{0}:=\emptyset$ and $S^{i+1}:=S^{i}\cup F(S^{i})$.

Let $\varphi(X,\bar{\mathtt{x}})$ be a formula of vocabulary $\sigma$, where $X$ is a relation variable of arity $k$ and $\mathtt{x}$ is a $k$-tuple of variables of sort n. Let $\bf A$ be a $\sigma$-structure and $\it{val}$ a variable valuation. The formula $\varphi(X,\bar{\mathtt{x}})$ gives rise to an operator $F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X}:{\cal P}((\textit{Num}(\mathbf{A}))^{k})\rightarrow{\cal P}((\textit{Num}(\mathbf{A}))^{k})$ defined as follows:

[TABLE]

Definition 3**.**

The formulae of $\mathrm{IL(IFP)}$ are interpreted as follows:

• •

$\mathbf{A},\mathit{val}\models{\tt x}_{1}\leq{\tt x}_{2}$* iff $\mathit{val}({\tt x}_{1})\leq\mathit{val}({\tt x}_{2})$.*

• •

$\mathbf{A},\mathit{val}\models t_{1}\leq t_{2}$* iff $\mathit{val}(t_{1})\leq\mathit{val}(t_{2})$.*

• •

$\mathbf{A},\mathit{val}\models R(t_{1},\dots,t_{k})$* iff $(\mathit{val}(t_{1}),\dots,\mathit{val}(t_{k}))\in R^{\mathbf{A}}$.*

• •

$\mathbf{A},\mathit{val}\models X({\tt x}_{1},\dots,{\tt x}_{k})$* iff $(\mathit{val}({\tt x}_{1}),\dots,\mathit{val}({\tt x}_{k}))\in\mathit{val}(X)$.*

• •

$\mathbf{A},\mathit{val}\models t=\mathit{index}\{\mathtt{x}:\varphi(\mathtt{x})\}$* iff $\mathit{val}(t)$ in binary is $b_{m}b_{m-1}\cdots b_{0}$, where $m={\lceil\log|A|\rceil}-1$ and $b_{j}=1$ iff $\mathbf{A},\mathit{val}(j/\mathtt{x})\models\varphi(\mathtt{x})$. *

• •

$\mathbf{A},\mathit{val}\models[\mathrm{IFP}_{\bar{\mathtt{x}},X}\varphi]\bar{{\tt y}}$* iff $\mathit{val}(\bar{{\tt y}})\in\mathrm{ifp}(F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X})$.*

• •

$\mathbf{A},\mathit{val}\models\neg\varphi$* iff $\mathbf{A},\mathit{val}\not\models\varphi$.*

• •

$\mathbf{A},\mathit{val}\models\varphi\wedge\psi$* iff $\mathbf{A},\mathit{val}\models\varphi$ and $\mathbf{A},\mathit{val}\models\psi$.*

• •

$\mathbf{A},\mathit{val}\models\exists\mathtt{x}\,\varphi$* iff $\mathbf{A},\mathit{val}(i/\mathtt{x})\models\varphi$, for some $i\in\textit{Num}(\mathbf{A})$.*

• •

$\mathbf{A},\mathit{val}\models\exists x(x=\mathit{index}\{\mathtt{x}:\alpha(\mathtt{x})\}\wedge\varphi)$* iff there exists $i\in A$ such that $\mathbf{A},\mathit{val}(i/\mathtt{x})\models x=\mathit{index}\{\mathtt{x}:\alpha(\mathtt{x})\}$ and $\mathbf{A},\mathit{val}(i/\mathtt{x})\models\varphi$.*

It immediately follows from the famous result by Gurevich and Shelah regarding the equivalence between inflationary and least fixed points [30], that an equivalent index logic can be obtained if we (1) replace $[\mathrm{IFP}_{\bar{\mathtt{x}},X}\varphi]\bar{{\tt y}}$ by $[\mathrm{LFP}_{\bar{\mathtt{x}},X}\varphi]\bar{{\tt y}}$ in the formation rule for the fixed point operator in Definition 2, adding the restriction that every occurrence of $X$ in $\varphi$ is positive333This ensures that $F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X}$ is a monotonic function and that the least fixed point $\mathrm{lfp}(F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X})$ exists., and (2) fix the interpretation $\mathbf{A},\mathit{val}\models[\mathrm{LFP}_{\bar{\mathtt{x}},X}\varphi]\bar{y}$ iff $\mathit{val}(\bar{y})\in\mathrm{lfp}(F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X})$.

Moreover, the convenient tool of simultaneous fixed points, which allows one to iterate several formulae at once, can also be used here, since it does not increase the expressive power of the logic. Following the syntax and semantics proposed by Ebbinghaus and Flum [28], a version of index logic with simultaneous inflationary fixed point operators can be obtained by replacing the clause corresponding to $\mathrm{IFP}$ in Definition 2 by the following:

• •

If $\bar{{\tt y}}$ is tuple of variables of sort n, and for $m\geq 0$ and $0\leq i\leq m$, we have that $\bar{\mathtt{x}}_{i}$ is also a tuple of variables of sort n, $X_{i}$ is a relation variable whose arity coincides with the length of $\bar{\mathtt{x}}_{i}$, the lengths of $\bar{{\tt y}}$ and $\bar{\mathtt{x}}_{0}$ are the same, and $\varphi_{i}$ is a formula, then $[\textrm{S-IFP}_{\bar{\mathtt{x}}_{0},X_{0},\ldots,\bar{\mathtt{x}}_{m},X_{m}}\varphi_{0},\ldots,\varphi_{m}]\bar{{\tt y}}$ is an atomic formula.

The interpretation is that $\mathbf{A},\mathit{val}\models[\textrm{S-IFP}_{\bar{\mathtt{x}}_{0},X_{0},\ldots,\bar{\mathtt{x}}_{m},X_{m}}\varphi_{0},\ldots,\varphi_{m}]\bar{{\tt y}}$ iff $\mathit{val}(\bar{{\tt y}})$ belongs to the first (here $X_{0}$) component of the simultaneous inflationary fixed point.

Thus, we can use index logic with the operators IFP, LFP, S-IFP or S-LFP interchangeably.

In the next two subsections, we give two worked-out examples that illustrate the power of index logic. After that, the exact characterization of its expressive power is presented in Subsection 5.3.

5.1 Finding the binary representation of a term

Let $t$ be a term of sort $\bf v$. In this example, we construct an index logic formula that expresses the well-known bit predicate $\mathrm{BIT}(t,{\tt x})$. The predicate $\mathrm{BIT}(t,{\tt x})$ states that the $(\it{val}({\tt x})+1)$-th bit of $\it{val}(t)$ in binary is set. Subsequently, the sentence $t=\mathit{index}\{{\tt x}:\mathrm{BIT}(t,{\tt x})\}$ is valid over the class of all finite ordered structures.

Informally, for a fixed term $t$, our implementation of $\mathrm{BIT}(t,{\tt x})$ works by iterating through the bit positions ${\tt y}$ from the most significant to the least significant. These bits are accumulated in a relation variable $Z$. For each ${\tt y}$ we set the corresponding bit, on the condition that the resulting number does not exceed $t$. The set bits are collected in a relation variable $Y$.

In the formal description of $\mathrm{BIT}(t,{\tt x})$ below, we use the following abbreviations. We use $M$ to denote the most significant bit position. Thus, formally, ${\tt z}=M$ abbreviates $\forall{\tt z}^{\prime}\,{\tt z}^{\prime}\leq{\tt z}$. Furthermore, for a unary relation variable $Z$, we use ${\tt z}=\min Z$ with the obvious meaning. We also use abbreviations such as ${\tt z}={\tt z}^{\prime}-1$ with the obvious meaning.

Now $\mathrm{BIT}(t,{\tt x})$ is a simultaneous fixed point $[\textrm{S-IFP}_{{\tt y},Y,{\tt z},Z}\,\varphi_{Y},\varphi_{Z}]({\tt x})$, where

[TABLE]

5.2 Binary search in an array of key values

In order to develop insight in how index logic works, we develop in detail an example showing how binary search in an array of key values can be expressed in the logic.

We represent the data structure as an ordered structure $\mathbf{A}$ over the vocabulary consisting of a unary function $K$, a constant symbol $N$, a constant symbol $T$, and a binary relation $\prec$. The domain of $\mathbf{A}$ is an initial segment of the natural numbers. The constant $l:=N^{\mathbf{A}}$ indicates the length of the array; the domain elements [math], $1$, …, $l-1$ represent the cells of the array. The remaining domain elements represent key values. Each array cell holds a key value; the assignment of key values to array cells is given by the function ${K}^{\mathbf{A}}$.

The simplicity of the above abstraction gives rise to two peculiarities, which, however, pose no problems. First, the array cells belong to the range of the function $K$. Thus, array cells are allowed to play a double role as key values. Second, the function $K$ is total, so it is also defined on the domain elements that are not array cells. We will simply ignore $K$ on that part of the domain.

We still need to discuss about $\prec$ and $T$. We assume $\prec^{\mathbf{A}}$ to be a total order, used to compare key values. So $\prec^{\mathbf{A}}$ can be different from the built-in order $<^{\mathbf{A}}$. For the binary search procedure to work, the array needs to be sorted, i.e., $\mathbf{A}$ must satisfy \forall x\forall y\Big{(}x<y<N\to\big{(}K(x)\preceq K(y)\big{)}\Big{)}. Finally, the constant $t:=T^{\mathbf{A}}$ is the test value. Specifically, we are going to exhibit an index logic formula that expresses that $t$ is a key value stored in the array. In other words, we want to express the condition

[TABLE]

Note that, we express here the condition $(\gamma)$ by a first-order formula that is not an index logic formula. So, our aim is to show that $(\gamma)$ is still expressible, over all sorted arrays, by a formula of index logic.

We recall the procedure for binary search [31] in the following form, using integer variables $L$, $R$ and $I$:

[TABLE]

We are going to express the above procedure as a simultaneous fixed point, using binary relation variables $L$ and $R$, and a unary relation variable $Z$. We collect the iteration numbers in $Z$, thus counting until the logarithm of the size of the structure. Relation variables $L$ and $R$ are used to store the values, in binary representation, of the integer variables $L$ and $R$ during all iterations. Specifically, for each $i\in\mathit{Num}(\mathbf{A})$, the value of the term $\mathit{index}\{{\tt x}:L(i,{\tt x})\}$ will be the value of the integer variable $L$ before the $(i+1)$-th iteration of the while loop (and similarly for $R$).

In the formal expression of $(\gamma)$ below, we use the bit predicate from Section 5.1. We also assume the following formulas:

• •

A formula ${\it avg}(X,Y,{\tt x})$ that expresses, for unary relation variables $X$ and $Y$, and a numeric variable ${\tt x}$, that the bit ${\tt x}$ is set in the binary representation of $\lfloor(x+y)/2\rfloor$, where $x$ and $y$ are the numbers represented in binary by $X$ and $Y$.

• •

A formula ${\it minusone}(X,{\tt y})$, expressing that the bit ${\tt y}$ is set in the binary representation of $x-1$, where $x$ is the number represented in binary by $X$.

These formulas surely exist because index logic includes full inflationary fixed point logic on the numeric sort; inflationary fixed point logic captures PTIME on the numeric sort, and computing the average, or subtracting one, are PTIME operations on binary numbers.

We are going to apply the formula $\it avg(X,Y,{\tt x})$, where $X$ and $Y$ are given by $L({\tt z},.)$ and $R({\tt z},.)$. So, formally, below, we use $\it avg^{\prime}({\tt z},{\tt x})$ for the formula obtained from the formula $\it avg$ by replacing each subformula of the form $X({\tt u})$ by $L({\tt z},{\tt u})$, and $Y({\tt u})$ by $R({\tt z},{\tt u})$.

Furthermore, we are going to apply the formula $\it minusone(X,{\tt u})$, where $X$ is given by $\it avg^{\prime}({\tt z})$. So, formally, $\it minusone^{\prime}({\tt z},{\tt u})$ will denote the formula obtained from $\it minusone(X,u)$ by replacing each subformula of the form $X({\tt u})$ by ${\it avg}^{\prime}({\tt z},{\tt u})$.

A last abbreviation we will use is $\it test({\tt z})$, which will denote the formula $\exists e(e=\mathit{index}\{{\tt x}:{\it avg}^{\prime}({\tt z},{\tt x})\}\land K(e)\succ T)$.

Now $(\gamma)$ is expressed by $\exists x(x=\mathit{index}\{{\tt l}:\psi({\tt l})\}\land K(x)=T)$, where

[TABLE]

5.3 The logical characterization theorem for $\mathrm{PolylogTime}$

The following result confirms that our logic serves our original purpose.

Theorem 2**.**

Over ordered structures, index logic captures $\mathrm{PolylogTime}$.

Proof.

Formulas of index logic can be evaluated in polylogarithmic time

Let $\mathrm{VAR}$ be a finite set of variables (of sort n, v, and relational). We stipulate a Turing machine model that has a designated work-tape for each of the variables in $\mathrm{VAR}$. The idea here is that the tape designated for a variable contains the value of that variable encoded as a binary string. We use induction on the structure of formulas to show that, for every sentence $\varphi$ of index logic, whose variables are from the set $\mathrm{VAR}$, there exists a direct-access Turing machine $M_{\varphi}$ that, for every ordered structure $\bf A$ with $|A|=n$, and every valuation $\mathit{val}$, decides in time $O(\lceil\log n\rceil^{O(1)})$ whether ${\bf A},\mathit{val}\models\varphi$. Since $\mathrm{VAR}$ is an arbitrary finite set, this suffices.

In the proof, variables $v$ of sort n and v are treated in a similar way as constant symbols, meaning that their value $\mathit{val}(v)$ is written in binary in the first $\lceil\log n\rceil$ cells of their designated work-tapes. The work-tape designated to a relation variable $X$ of arity $k$ contains $\mathit{val}(X)\subseteq\mathit{Num}({\bf A})^{k}$ encoded as a binary string in its first $\lceil\log n\rceil^{k}$ cells, where a $1$ in the $i$-th cell indicates that the $i$-th tuple in the lexicographic order of $\mathit{Num}({\bf A})^{k}$ is in $\mathit{val}(X)$.

We will show first, by induction on the structure of terms, that, if $t$ is term, $M$ a direct-access Turing machine, and $\mathit{val}$ a valuation such that, for every variable $\chi$ that occurs in $t$, the value $\mathit{val}(\chi)$ is written in binary in the designated work-tape of $\chi$, then $\mathit{val}(t)$ can be computed by $M$ in time $O(\lceil\log n\rceil^{O(1)})$. If $t$ is a variable of sort n or v, or a constant symbol, then $M$ only needs to read the first $\lceil\log n\rceil$ cells of the appropriate work-tape or constant-tape, respectively. If $t$ is a term of the form $f_{i}(t_{1},\ldots,t_{k})$, we access and copy each $\mathit{val}(t_{j})$ in binary in the corresponding address-tapes of $f_{i}$. By the induction hypothesis, this takes time $O(\lceil\log n\rceil^{O(1)})$ each. Using $\lceil\log n\rceil$ additional steps the result of length $\lceil\log n\rceil$ will then be accessible in the value-tape of $f_{i}$.

We will next use induction to prove our main claim. Note that, the cases for quantifiers assure that the assumptions needed for the calculation of the values of terms are met. We will show by induction that, if $\varphi$ is a formula with variables in $\mathrm{VAR}$, ${\it{val}}$ a valuation, and $M$ a direct-access Turing machine, such that, for every variable $\chi$ that occurs free in $\varphi$, the value $\mathit{val}(\chi)$ is written in binary in the designated work-tape of $\chi$, then ${\bf A},\mathit{val}\models\psi$ can be decided by $M$ in time $O(\lceil\log n\rceil^{O(1)})$.

If $\varphi$ is an atomic formula of the form $t_{1}\leq t_{2}$, $M$ can evaluate $\varphi$ in polylogarithmic time by accessing the values of $t_{1}$ and $t_{2}$ in binary and then comparing their $\lceil\log n\rceil$ bits.

If $\varphi$ is an atomic formula of the form $R_{i}(t_{1},\dots,t_{k})$, $M$ can evaluate $\varphi$ in polylogarithmic time by simply computing the values of the terms $t_{1},\dots,t_{k}$ and copying the values to the corresponding address-tapes of $R_{i}$. By the proof for terms above, computing the values of the terms take polylogarithmic time each, and since the values have $\lceil\log n\rceil$ bits, also the copying can be done in polylogarithmic time.

If $\varphi$ is an atomic formula of the form $X({\tt x}_{1},\dots,{\tt x}_{k})$, $M$ can evaluate $\varphi$ in polylogarithmic time by accessing the values ${\tt x}_{1},\dots,{\tt x}_{k}$ in binary, computing the position $i$ of the tuple $({\tt x}_{1},\dots,{\tt x}_{k})$ in the lexicographic order of $\mathit{Num}({\bf A})^{k}$ in binary, and then accessing the $i$-th cell of the work-tape which contains the encoding of $\mathit{val}(X)$ of length $\lceil\log n\rceil^{k}$. Computing $i$ in binary involves simple arithmetic operations on binary numbers of length bounded by $\log(\lceil\log n\rceil^{k})$, which can clearly be done in time polynomial in $\log n$.

If $\varphi$ is an atomic formula of the form $t=\mathit{index}\{\mathtt{x}:\psi(\mathtt{x})\}$, $M$ proceeds as follows. Let $s=\lceil\log n\rceil-1$ and let $b_{s}b_{s-1}\cdots b_{0}$ be $\mathit{val}(t)$ in binary. For every $i$, $0\leq i\leq s$, $M$ writes $i$ in binary in the work-tape designated for the variable $\mathtt{x}$ and checks whether ${\bf A},\mathit{val}(i/\mathtt{x})\models\psi(\mathtt{x})$ iff $b_{i}=1$. Since, by the induction hypothesis, this check can be done in polylogarithmic time, and $\mathit{val}(t)$ can be computed in polylogarithmic time, we get that $M$ decides $t=\mathit{index}\{\mathtt{x}:\varphi(\mathtt{x})\}$ in polylogarithmic time as well.

If $\varphi$ is a formula of the form $[\mathrm{IFP}_{\bar{\mathtt{x}},X}\psi]\bar{y}$, where the arity of $X$ is $k$, let $F^{\bf A,\it{val}}_{\psi,\bar{\mathtt{x}},X}:{\cal P}((\textit{Num}(\mathbf{A}))^{k})\rightarrow{\cal P}((\textit{Num}(\mathbf{A}))^{k})$ denote the related operator, $F^{0}:=\emptyset$, and $F^{i+1}:=F^{i}\cup F^{\bf A,\it{val}}_{\psi,\bar{\mathtt{x}},X}(F^{i})$, for each $i\geq 0$. The inflationary fixed point is reached on stage $\lvert\textit{Num}(\mathbf{A})^{k}\rvert$, at the latest, and thus $\mathrm{ifp}(F^{\bf A,\it{val}}_{\psi,\bar{\mathtt{x}},X})=F^{\log^{k}n}.$ Recall that

[TABLE]

We calculate $F^{i+1}$ from $F^{i}$ as follows. Note that on each stage, the value of $F^{i}$ is written in binary on the work-tape designated for $X$. We first calculate the value of $F^{i+1}$ in binary on another work-tape, and then reformat the contents of the work-tape designated for $X$ to contain the value of $F^{i+1}$. For $i=0$, we format the work-tape designated for $X$ to contain a string of [math]s of length $\log^{k}n$. In order to calculate $F^{i+1}$ from $F^{i}$, we go through all $k$-tuples $\bar{a}\in(\textit{Num}(\mathbf{A}))^{k}$ in the lexicographic order. For $1\leq j\leq k$, we write $\bar{a}[j]$ in binary on the designated work-tape for $\bar{{\tt x}}[j]$ and check whether

[TABLE]

holds. By induction hypothesis, this can be checked in time $O(\lceil\log n\rceil^{O(1)})$. If $\eqref{eq:1}$ holds and $\bar{a}$ is the $l$-th k-tuple in the lexicographic ordering, we write $1$ to the $l$-th cell of the work-tape, where the value of $F^{i+1}$ is being constructed, otherwise we write [math] to this cell. Hence the computation of $F^{i+1}$ from $F^{i}$ can be done in time $\log^{k}n\times O(\lceil\log n\rceil^{O(1)})$ which is still $O(\lceil\log n\rceil^{O(1)})$. It is now clear that $\mathrm{ifp}(F^{\bf A,\it{val}}_{\psi,\bar{\mathtt{x}},X})=F^{\log^{k}n}$ can be computed in time $O(\lceil\log n\rceil^{O(1)})$ as well. Finally, determining whether ${\it val}(\bar{y})$ is included in the fixed point is clearly computable in $O(\lceil\log n\rceil^{O(1)})$, for one must just calculate the position of ${\it val}(\bar{y})$ in the lexicographic order of $k$-tuples, and then check whether that position has a [math] or $1$ in the work-tape corresponding to $X$.

If $\varphi$ is a formula of the form $\exists x(x=\mathit{index}\{\mathtt{x}:\alpha(\mathtt{x})\}\wedge\psi(x))$, $M$ proceeds as follows. For each $i\in\{0,\ldots,\lceil\log n\rceil-1\}$, $M$ writes $i$ in binary in the work-tape designated for $\mathtt{x}$ and checks whether ${\bf A},\mathit{val}(i/\mathtt{x})\models\alpha(\mathtt{x})$. Since, by definition, $x$ does not appear free in $\alpha(\mathtt{x})$, it follows by the induction hypothesis that $M$ can perform each of these checks in polylogarithmic time. In parallel, $M$ writes the bit string $b_{s}b_{s-1}\cdots b_{0}$, defined such that $b_{i}=1$ iff ${\bf A},\mathit{val}(i/\mathtt{x})\models\alpha(\mathtt{x})$, to the work-tape designated to the variable $x$. Let the content of this work-tape at the end of this process be $t$ in binary. $M$ can now check whether $t<n$ (recall that by convention, $M$ has the value $n$ in binary in one of its constant-tapes and thus this can be done in polylogarithmic time). If $t\geq n$ then ${\bf A},\mathit{val}\not\models\varphi$. If $t<n$, then $M$ checks whether ${\bf A},\mathit{val}(t/x)\models\psi$, which by the induction hypothesis can also be done in polylogarithmic time.

Finally, if $\varphi$ is a formula of the form $\exists\mathtt{x}\,\psi$, then for each $i\in\{0,\ldots,\lceil\log n\rceil-1\}$, $M$ writes $i$ in binary to the work-tape designated for $\mathtt{x}$ and checks whether ${\bf A},\mathit{val}(i/\mathtt{x})\models\psi$. It follows by the induction hypothesis that $M$ can perform each of these checks in polylogarithmic time. If the test is positive for some $i$ then ${\bf A},\mathit{val}\models\varphi$. The remaining cases are those corresponding to Boolean connectives and follow trivially from the induction hypothesis.

Every polylogarithmic time property can be expressed in index logic

Suppose we are given a class $\cal C$ of ordered $\sigma$-structures, which can be decided by a deterministic polylogarithmic time direct-access Turing machine $M=(Q,\Sigma,\delta,q_{0},F,\sigma)$, that has $m$ tapes, including ordinary work-tapes, address-tapes, (function) value-tapes and constant-tapes. We assume, w.l.o.g., that $F=\{q_{a}\}$ (i.e., there is only one accepting state), $|Q|=a+1$, and $Q=\{q_{0},q_{1},\ldots,q_{a}\}$.

Let $M$ run in time $O(\lceil\log n\rceil^{k})$. Note that, only small inputs (up to some fixed constant) may require more time than $\lceil\log n\rceil^{k}$. Those finite number of small input structures can be dealt separately, for each finite structure can be easily defined by an index logic sentence. Hence, from now on, we only consider those inputs for which $M$ runs in time $\lceil\log n\rceil^{k}$. Using the order relation $\leq^{\bf A}$ of the ordered structure $\bf{A}$, we can define the lexicographic order $\leq^{\mathbf{A}}_{k}$ for the $k$-tuples in $\mathit{Num}(\mathbf{A})^{k}$, and then use this order to model time and positions of the tape heads of $M$. Note that this can be done, since the number of $k$-tuples in $\mathit{Num}(\mathbf{A})^{k}$ is $\lceil\log n\rceil^{k}$. In our proof, we use expressions of the form $\bar{t}\sim t^{\prime}$, where $\bar{t}$ is a $k$-tuple of variables of sort $\bf n$ and $t^{\prime}$ is a single variable also of sort $\bf n$, with the intended meaning that $\it{val}(\bar{t})$ is the $(\it{val}(t^{\prime})+1)$-th tuple in the order $\leq^{\mathbf{A}}_{k}$. This is clearly expressible in index logic, since it is a polynomial time property on the $\bf n$ sort.

Next we introduce, together with their intended meanings, the relations we use to encode the configurations of polylogarithmic time direct-access Turing machines. Consider:

• •

A $k$-ary relation $S_{q}$, for every state $q\in Q$, such that $S_{q}(\bar{t})$ holds iff $M$ is in state $q$ at time $\bar{t}$.

• •

$2k$-ary relations $T_{i}^{0},T_{i}^{1},T_{i}^{\sqcup}$, for every tape $i=1,\ldots,m$, such that $T_{i}^{s}(\bar{p},\bar{t})$ holds iff at the time $\bar{t}$ the cell $\bar{p}$ of the tape $i$ contains the symbol $s$.

• •

$2k$-ary relations $H_{i}$, for every tape $i=1,\ldots,m$, such that $H_{i}(\bar{p},\bar{t})$ holds iff at the time $\bar{t}$ the head of the tape $i$ is on the cell $\bar{p}$.

We show that these relations are definable in index logic by means of a simultaneous inflationary fixed point formula. The following sentence is satisfied by a structure $\bf A$ iff ${\bf A}\in{\cal C}$. The idea of the formula is that it uses the simultaneous fixed point operator to construct the whole computation of $M$ iteration by iteration, and states that there exists a time step in which $M$ accepts. We define the formula

[TABLE]

where

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Note that here $\bar{p}$ and $\bar{t}$ denote $k$-tuples of variables of sort $\bf n$.

The formula builds the required relations $S_{q_{i}}$, $T^{0}_{i}$, $T^{1}_{i}$, $T^{\sqcup}_{i}$ and $H_{i}$ (for $1\leq i\leq m$) in stages, where the $j$-th stage represents the configuration at time steps up to $j-1$. The subformulae $\varphi_{q_{i}}$, $\psi_{0i}$, $\psi_{1i}$, $\psi_{\sqcup i}$ and $\gamma_{i}$ define $S_{q_{i}}$, $T^{0}_{i}$, $T^{1}_{i}$, $T^{\sqcup}_{i}$ and $H_{i}$, respectively.

To simplify the presentation of the subformulae and w.l.o.g., we assume that, in every non-initial state of a computation, each address-tape contains a single binary number between [math] and $n-1$ and nothing else. This number has at most $\log n$ bits, and hence we encode positions of address-tapes (and function value-tapes) with a single variable of sort $\bf n$ (instead of a tuple of variables).

We will now give the idea how the formulae $\varphi_{q_{i}}$, $\psi_{0i}$, $\psi_{1i}$, $\psi_{\sqcup i}$, and $\gamma_{i}$ are constructed from $M$. We first describe the construction of $\psi_{0i}$ in detail; the formulae $\psi_{1i}$ and $\psi_{\sqcup i}$ are constructed in a similar fashion. The rough idea behind all the formulas is the following: the formulas encode directly the initial configuration of the computation, and for a non-initial time step, how the configuration at that time step is computed from the previous configuration. The formula $\psi_{0i}(\bar{p},\bar{t})$, for example, encodes whether the $i$-th tape at the cell position $\bar{p}$ at the time $\bar{t}$ contains the symbol [math]. If $i$ is an address-tape or an ordinary work-tape, then in the initial configuration of the computation, the tape $i$ contains the blank symbol $\sqcup$ on all its cells. In this case, the formula $\psi_{0i}$ is of the form:

[TABLE]

where $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$ list conditions under which at the following time instant, $\bar{t}$, the position $\bar{p}$ of the tape $i$ will contain [math]. In the more general case, the formula has the form $(\bar{t}\sim 0\land\xi_{T^{0}_{i}})\lor(\neg(\bar{t}\sim 0)\wedge\alpha^{0}_{i}(\bar{p},\bar{t}-1))$, where $\xi_{T^{0}_{i}}$ is used to encode the initial configuration related to the relation $T^{0}_{i}$.

We will next describe the construction of $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$. Suppose, $i$ refers to an address-tape or to an ordinary work-tape. The formula $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$ is a disjunction over all the possible reasons, for why at the time $\bar{t}$ the position $\bar{p}$ of tape $i$ contains the symbol [math]. There are two possibilities: (1) at the time $\bar{t}-1$ the head of the tape $i$ was not in the position $\bar{p}$ and the position $\bar{p}$ of the tape $i$ contained the symbol [math], (2) at the time $\bar{t}-1$ the head of the tape $i$ was in the position $\bar{p}$ and the head wrote the symbol [math]. Below, we display a disjunct of $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$ that is due to a reason of the second kind by one possible transition $\delta_{i}(q,a_{1},\ldots,a_{m},b_{1},\ldots,b_{p})=(0,\rightarrow)$. The disjunct of $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$, which takes care of this case is obtained from the following formula by substituting $\bar{p}_{i}$ with $\bar{p}$:

[TABLE]

At time $\bar{t}-1$, $M$ is in the state $q$ and the head of the tape $j$ is in the position $\bar{p}_{j}$ reading $a_{j}$.

At time $\bar{t}-1$, the tuple of values in the address-tapes of $R_{l}$ is in $R^{\mathbf{A}}$ iff $b_{l}=1$.

where $\tau^{R}_{l,1},\ldots,\tau^{R}_{l,r_{l}}$ denote the $r_{l}$ address-tapes corresponding to the $r_{l}$-ary relation $R_{l}$, and $\mathrm{check}(R_{l}(x_{1},\ldots,x_{r_{l}}),b_{l})$ is a shorthand for $R_{l}(x_{1},\ldots,x_{r_{l}})$, if $b_{l}=1$, and a shorthand for $\neg R_{l}(x_{1},\ldots,x_{r_{l}})$, if $b_{l}=0$.

Assume then that $i$ refers to a value-tape of a function $f_{j}$ of arity $k_{j}$, and let $\tau^{f}_{j,1},\ldots,\tau^{f}_{j,k_{j}}$ refer to its address-tapes. Recall that the contents of a value-tape of a function at a time $\bar{t}$ depends only on the contents of its address-tapes at the time $\bar{t}$. Below, we write $\psi_{0i}(p,\bar{t})$ using the contents of the related address-tapes at time $\bar{t}$. This is fine, for we do not introduce circularity of definitions (technically, we obtain the contents of the related address-tapes at time $\bar{t}$ using the corresponding formulas that define them from the configuration of the machine at time $\bar{t}-1$). Now $\psi_{0i}(p,\bar{t})$ refers to the following formula:

[TABLE]

where $\mathrm{BIT}(f_{j}(x_{1},\ldots,x_{k_{j}}),p)$ expresses that the bit of position $p$ of $f_{j}(x_{1},\ldots,x_{k_{j}})$ in binary is $1$; we showed, in Section 5.1, how the bit predicate is expressed in index logic.

The formula $\varphi_{q_{0}}$ is of the form $\bar{t}\sim 0\vee(\neg(\bar{t}\sim 0)\wedge\alpha_{q_{0}}(\bar{t}-1))$ and other $\varphi_{q}$’s are of the form $\neg(\bar{t}\sim 0)\wedge\alpha_{q}(\bar{t}-1)$, where $\alpha_{q}(\bar{t}-1)$ list conditions under which $M$ will enter state $q$ at the next time instant, $\bar{t}$.

Finally, the formulae $\gamma_{i}$ are of the form

[TABLE]

where $\alpha_{i}(\bar{p},\bar{t}-1)$ list conditions under which, at the following time instant $\bar{t}$, the head of the tape $i$ will be in the position $\bar{p}$.

We omit writing the remaining subformulae, since it is an easy but tedious task. It is also not difficult to see that in the $j$-th stage of the simultaneous inflationary fixed point computation, the relations $S_{q}$, $(T_{i}^{0},T_{i}^{1},T_{i}^{\sqcup})_{1\leq i\leq m}$ and $(H_{i})_{1\leq i\leq m}$ encode the configuration of $M$ for times $\leq j-1$, which completes our proof. ∎

6 Definability in Deterministic PolylogTime

We observe here that very simple properties of structures are nondefinable in index logic. Moreover, we provide an answer to a fundamental question on the primitivity of the built-in order predicate (on terms of sort $\bf v$) in our logic. Indeed, we are working with ordered structures, and variables of sort $\bf v$ can only be introduced by binding them to an index term. Index terms are based on sets of bit positions which can be compared as binary numbers. Hence, it is plausible to suggest that the built-in order predicate can be removed from our logic without losing expressive power. We prove, however, that this does not work in the presence of constant or function symbols in the vocabulary.

Proposition 1**.**

Assume that the vocabulary includes a unary relation symbol $P$. Checking emptiness (or non-emptiness) of $P^{\mathbf{A}}$ in a given structure $\mathbf{A}$ is not computable in $\mathrm{PolylogTime}$.

Proof.

We will show that emptiness is not computable in $\mathrm{PolylogTime}$. For a contradiction, assume that it is. Consider first-order structures over the vocabulary $\{P\}$, where $P$ is a unary relation symbol. Let $M$ be some Turing machine that decides in $\mathrm{PolylogTime}$, given a $\{P\}$-structure $\mathbf{A}$, whether $P^{\mathbf{A}}$ is empty. Let $f$ be a polylogarithmic function that bounds the running time of $M$. Let $n$ be a natural number such that $f(n)<n$.

Let $\mathbf{A}_{\emptyset}$ be the $\{P\}$-structure with domain $\{0,\dots,n-1\}$, where $P^{\mathbf{A}}=\emptyset$. The encoding of $\mathbf{A}_{\emptyset}$ to the Turing machine $M$ is the sequence s:=\underbrace{0\dots 0}_{\text{n times}}. Note that the running time of $M$ with input $s$ is strictly less than $n$. This means that there must exist an index $i$ of $s$ that was not read in the computation $M(s)$. Define

[TABLE]

Clearly the output of the computations $M(s)$ and $M(s^{\prime})$ are identical, which is a contradiction since $s^{\prime}$ is an encoding of a $\{P\}$-structure where the interpretation of $P$ is a singleton. ∎

The technique of the above proof can be adapted to prove a plethora of undefinability results, e.g., it can be shown that $k$-regularity of directed graphs cannot be decided in $\mathrm{PolylogTime}$, for any fixed $k$.

We can develop this technique further to show that the order predicate on terms of sort $\bf v$ is a primitive in the logic. The proof of the following lemma is quite a bit more complicated though.

Lemma 1**.**

Let $P$ and $Q$ be unary relation symbols. There does not exist an index logic formula $\varphi$ such that for all $\{P,Q\}$-structures $\mathbf{A}$ such that $P^{\mathbf{A}}$ and $Q^{\mathbf{A}}$ are disjoint singleton sets $\{l\}$ and $\{m\}$, respectively, it holds that

[TABLE]

Proof.

We will show that the property described above cannot be decided in $\mathrm{PolylogTime}$; the claim then follows from Theorem 2. For a contradiction, suppose that the property can be decided in $\mathrm{PolylogTime}$, and let $M$ and $f:\mathbb{N}\rightarrow\mathbb{N}$ be the related random-access Turing machine and polylogarithmic function, respectively, such that, for all $\{P,Q\}$-structures $\mathbf{A}$ that satisfy the conditions of the claim, $M(\mathrm{bin}(\mathbf{A}))$ decides the property in at most $f(|\mathrm{bin}(\mathbf{A})\rvert)$ steps. Let $k$ be a natural number such that $f(2k)<k-1$.

Consider a computation $M(s)$ of $M$ with an input string $s$. We say that an index $i$ is inspected in the computation, if at some point during the computation $i$ is written in the index tape in binary. Let $\mathrm{Ins}_{M}(s)$ denote the set of inspected indices of the computation of $M(s)$ and $\mathrm{Ins}^{j}_{M}(s)$ denote the set of inspected indices during the first $j$ steps of the computation. We say that $s$ and $t$ are $M$-$j$-equivalent if the lengths of $t$ and $s$ are equal and $t[i]=s[i]$, for each $i\in\mathrm{Ins}^{j}_{M}(s)$. We say that $\mathbf{A}$ and $\mathbf{B}$ are $M$-$j$-equivalent whenever $\mathrm{bin}(\mathbf{A})$ and $\mathrm{bin}(\mathbf{B})$ are. Note that if two structures $\mathbf{A}$ and $\mathbf{B}$ are $M$-$j$-equivalent, then the computations $M(\mathrm{bin}(\mathbf{A}))$ and $M(\mathrm{bin}(\mathbf{B}))$ are at the same configuration after $j$ steps of computation. Hence if $\mathbf{A}$ and $\mathbf{B}$ are M-$f(|\mathrm{bin}(\mathbf{A})\rvert)$-equivalent, then outputs of $M(\mathbf{A})$ and $M(\mathbf{B})$ are identical.

Let $\mathfrak{C}$ be the class of all $\{P,Q\}$-structures $\mathbf{A}$ of domain $\{0,\dots k-1\}$, for which $P^{\mathbf{A}}$ and $Q^{\mathbf{A}}$ are disjoint singleton sets. The encodings of these structures are bit strings of the form $b_{1}\dots b_{k}c_{1}\dots c_{k}$, where exactly one $b_{i}$ and one $c_{j}$, $i\neq j$, is $1$. The computation of $M(\mathrm{bin}(\mathbf{A}))$ takes at most $f(2k)$ steps.

We will next construct a subclass $\mathfrak{C}^{*}$ of $\mathfrak{C}$ that consists of exactly those structures $\mathbf{A}$ in $\mathfrak{C}$ for which the indices in $\mathrm{Ins}(\mathrm{bin}(\mathbf{A}))$ hold only the bit [math]. We present an inductive process that will in the end produce $\mathfrak{C}^{*}$. Each step $i$ of this process produces a subclass $\mathfrak{C}_{i}$ of $\mathfrak{C}$ for which the following hold:

1. a)

The structures in $\mathfrak{C}_{i}$ are $M$-$i$-equivalent. 2. b)

There exists $\mathbf{A}_{i}\in\mathfrak{C}_{i}$ and

[TABLE]

Define $\mathfrak{C}_{0}:=\mathfrak{C}$; clearly $\mathfrak{C}_{0}$ satisfies the properties above. For $i<f(2k)$, we define $\mathfrak{C}_{i+1}$ to be the subclass of $\mathfrak{C}_{i}$ consisting of those structures $\mathbf{A}$ that on time step $i+1$ inspects an index that holds the bit [math].444If the machine already halted on an earlier time step $t$, we stipulate that the machine inspects on time step $i+1$ the same index that it inspected on time step $t$.

Assume that a) and b) hold for $\mathfrak{C}_{i}$, we will show that the same holds for $\mathfrak{C}_{i+1}$. Proof of a): Let $\mathbf{A},\mathbf{B}\in\mathfrak{C}_{i+1}$. By construction and by the induction hypothesis, $\mathbf{A}$ and $\mathbf{B}$ are $M$-$i$-equivalent, and on step $i+1$ $M(\mathrm{bin}(\mathbf{A}))$ and $M(\mathrm{bin}(\mathbf{B}))$ inspect the same index that holds [math]. Thus $\mathbf{A}$ and $\mathbf{B}$ are $M$-$(i+1)$-equivalent. Proof of b): It suffices to show that $\mathfrak{C}_{i+1}$ is nonempty; the claim then follows by construction and the property b) of $\mathfrak{C}_{i}$. By the induction hypothesis, there is a structure $\mathbf{A}_{i}\in\mathfrak{C}_{i}$. Let $j$ be the index that $M(\mathrm{bin}(\mathbf{A}_{i}))$ inspects on step $i+1$. Since $i+1\leq f(2k)<k-1$, there exists a structure $\mathbf{A}_{i}^{\prime}\in\mathfrak{C}_{i}$ such that the $j$th bit of $\mathrm{bin}(\mathbf{A}_{i}^{\prime})$ is [math]. Clearly $\mathbf{A}^{\prime}_{i}\in\mathfrak{C}_{i+1}$.

Consider the class $\mathfrak{C}_{k-2}$ (this will be our $\mathfrak{C}^{*}$) and $\mathbf{B}\in\mathfrak{C}_{k-2}$ and recall that $\mathrm{bin}(\mathbf{B})$ is of the form $b_{1}\dots b_{k}c_{1}\dots c_{k}$. Since $\lvert\mathrm{Ins}^{k-2}(\mathbf{B})\rvert\leq k-2$, there exists two distinct indices $i$ and $j$, $0\leq i<j\leq k-1$, such that $i,j,i+k,j+k\notin\mathrm{Ins}^{k-2}(\mathrm{bin}(\mathbf{A}))$. Let $\mathbf{B}_{P<Q}$ denote the structure such that $\mathrm{bin}(\mathbf{B}_{P<Q})$ is a bit string where the $i$th and $j+k$th bits are $1$ and all other bits are [math]. Similarly, let $\mathbf{B}_{Q<P}$ denote the structure such that $\mathrm{bin}(\mathbf{B}_{Q<P})$ is a bit string where the $j$th and $i+k$th bits are $1$ and all other bits are [math]. Clearly the structures $\mathbf{B}_{P<Q}$ and $\mathbf{B}_{Q<P}$ are in $\mathfrak{C}_{k-2}$ and $M$-$(k-2)$-equivalent. Since $(k-2)$ bounds above the length of computations of $M(\mathrm{bin}(\mathbf{B}_{P<Q}))$ and $M(\mathrm{bin}(\mathbf{B}_{Q<P}))$, it follows that the outputs of the computations are identical. This is a contradiction, for $\mathbf{B}_{P<Q}$ and $\mathbf{B}_{Q<P}$ are such that $M$ should accept the first and reject the second. ∎

Theorem 3**.**

Let $c$ and $d$ be constant symbols in a vocabulary $\sigma$. There does not exist an index logic formula $\varphi$ that does not use the order predicate $\leq$ on terms of sort $\bf v$ and that is equivalent with the formula $c\leq d$.

Proof.

For the sake of a contradiction, assume that $\varphi$ is such a formula. We will derive a contradiction with Lemma 1. Without loss of generality, we may assume that the only symbols of $\sigma$ that occur in $\varphi$ are $c$ and $d$, and that $\varphi$ is a sentence (i.e., $\varphi$ has no free variables).

We define the translation $\varphi^{*}$ of $\varphi$ inductively. In addition to the cases below, we also have the cases where the roles of $c$ and $d$ are swapped.

• •

For $\psi$ that does not include $c$ or $d$, let $\psi^{*}:=\psi$.

• •

For Boolean connectives and quantifiers the translation is homomorphic.

• •

For $\psi$ of the form $\left[\mathrm{IFP}_{\bar{\tt x},X}{\theta}\right]{\bar{y}}$, let $\psi^{*}:=\left[\mathrm{IFP}_{\bar{\tt x},X}{\theta^{*}}\right]{\bar{y}}$.

• •

For $\psi$ of the form $c=d$, let $\psi^{*}:=\bot$.555By $\bot$ we denote some formula that is always false, e.g, $\exists{\tt x}\,{\tt x}\neq{\tt x}$.

• •

For $\psi$ of the form $c=x$ or $x=c$, let $\psi^{*}:=C(x)$.

• •

For $\psi$ of the form $x=\mathit{index}\{\tt{x}:\theta(\tt{x})\}$, define $\psi^{*}$ as $x=\mathit{index}\{{\tt x}:\theta^{*}({\tt x})\}.$

• •

For $\psi$ of the form $c=\mathit{index}\{\tt{x}:\theta(\tt{x})\}$, let

[TABLE]

where $z$ is a fresh variable.

If $\mathbf{A}$ is a $\{C,D\}$-structure such that $C^{\mathbf{A}}$ and $D^{\mathbf{A}}$ are disjoint singleton sets, we denote by $\mathbf{A}^{\prime}$ the $\{c,d\}$-structure with the same domain such that $\{c^{\mathbf{A}^{\prime}}\}=C^{\mathbf{A}}$ and $\{d^{\mathbf{A}^{\prime}}\}=D^{\mathbf{A}}$. We claim that for every $\{C,D\}$-structure $\mathbf{A}$ such that $C^{\mathbf{A}}$ and $D^{\mathbf{A}}$ are disjoint singleton sets $\{l\}$ and $\{m\}$ and every valuation $\mathit{val}$ the following holds:

[TABLE]

This is a contradiction with Lemma 1. It suffices to proof the last equivalence as the first two are reformulations of our assumptions. The proof is by induction on the structure of $\varphi$. The cases that do not involve the constants $c$ and $d$ are immediate. Note that by assumption, $c^{\mathbf{A}}$ and $d^{\mathbf{A}}$ are never equal and thus the subformula $c=d$ is equivalent to $\bot$. The case $c=x$ is also easy:

[TABLE]

The case for $c=\mathit{index}\{x:\theta(x)\}$ is similar:

[TABLE]

All other cases are homomorphic and thus straightforward. ∎

We conclude this section by affirming that, on purely relational vocabularies, the order predicate on sort $\bf v$ is redundant. The intuition for this result was given in the beginning of this section.

Theorem 4**.**

Let $\sigma$ be a vocabulary without constant or function symbols. For every sentence $\varphi$ of index logic of vocabulary $\sigma$ there exists an equivalent sentence $\varphi^{\prime}$ that does not use the order predicate on terms of sort $\bf v$.

Proof.

We will define the translation $\varphi^{\prime}$ of $\varphi$ inductively. Without loss of generality, we may assume that each variable that occurs in $\varphi$ is quantified exactly once (for this purpose, we stipulate that the variable ${\tt x}$ is quantified by the term $\mathit{index}\{\tt{x}:\alpha(\tt{x})\}$). For every variable $x$ of sort $\bf v$ that occurs in $\varphi$, let $\alpha_{x}({\tt x})$ denote the unique subformula such that $\exists x(x=\mathit{index}\{{\tt x}:\alpha_{x}({\tt x})\}\land\psi)$ is a subformula of $\varphi$ for some $\psi$. Note that ${\tt x}$ occurs only in $\mathit{index}\{{\tt x}:\alpha_{x}({\tt x})\}$. We define the following shorthands for variables ${\tt x}$ and ${\tt y}$ of sort $\bf n$:

[TABLE]

where ${\tt z}$ and ${\tt z}^{\prime}$ are fresh distinct variables of sort $\bf n$. In the formulas above, $\psi({\tt z}/{\tt x})$ denotes the formula that is obtained from $\psi$ by substituting each free occurrence of ${\tt x}$ in $\psi$ by ${\tt z}$. The translation $\varphi\mapsto\varphi^{\prime}$ is defined as follows:

• •

For formulae that do not include variables of sort $\bf v$, the translation is the identity.

• •

For Boolean connectives and quantifiers of sort $\bf n$, the translation is homomorphic.

• •

For $\psi$ of the form $\left[\mathrm{IFP}_{\bar{\tt x},X}{\theta}\right]{\bar{y}}$, let $\psi^{\prime}:=\left[\mathrm{IFP}_{\bar{\tt x},X}{\theta^{\prime}}\right]{\bar{y}}$.

• •

For $\psi$ of the form $x\leq y$, let $\psi^{\prime}:=\varphi_{{\tt x}={\tt y}}(\alpha_{x}({\tt x}),\alpha_{y}({\tt y}))\lor\varphi_{{\tt x}<{\tt y}}(\alpha_{x}({\tt x}),\alpha_{y}({\tt y}))$.

• •

For $\psi$ of the form $x=\mathit{index}\{{\tt y}:\theta({\tt y})\}$, define $\psi^{\prime}:=\varphi_{{\tt x}={\tt y}}(\alpha_{x}({\tt x}),\theta({\tt y}))$.

• •

For $\psi$ of the form $\exists x(x=\mathit{index}\{\tt{x}:\alpha(\tt{x})\land\theta\}$, define $\psi^{\prime}:=\theta^{\prime}$.

By a straightforward inductive argument it can be verified that the translation preserves equivalence. ∎

7 Index logic with partial fixed points

In this section, we introduce a variant of index logic defined in Section 5. This logic, which we denote as IL(PFP), is defined by simply replacing the inflationary fixed point operator IFP in the definition of index logic by the partial fixed point operator PFP. We stick to the standard semantics of the PFP operator. We define that

[TABLE]

where $\mathrm{pfp}(F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X})$ denotes the partial fixed point of the operator $F^{\bf A,\it{val}}_{\varphi,\bar{\mathtt{x}},X}$ (see the description above Definition 3). The partial fixed point $\mathrm{pfp}(F)$ of an operator $F:{\cal P}(B)\rightarrow{\cal P}(B)$ is defined as the fixed point of $F$ obtained from the sequence $(S^{i})_{i\in\mathbb{N}}$, where $S^{0}:=\emptyset$ and $S^{i+1}:=F(S^{i})$, if such a fixed point exists. If such a fixed point does not exist, then $\mathrm{pfp}(F):=\emptyset$.

It is well known that first-order logic extended with partial fixed point operators captures $\mathrm{PSPACE}$. As a counterpart for this result, we will show that IL(PFP) captures the complexity class polylogarithmic space ($\mathrm{PolylogSpace}$). Recall that in IL(PFP) the relation variables bounded by the PFP operators range over (tuples of) $\mathit{Num}(\mathbf{A})$, where $\mathbf{A}$ is the interpreting structure. Thus, the maximum number of iterations before reaching a fixed point (or concluding that it does not exist), is not exponential in the size $n$ of $\mathbf{A}$, as in FO(PFP). Instead, it is quasi-polynomial, i.e., of size $O(2^{\log^{k}n})$, for some constant $k$. This observation is, in part, the reason why IL(PFP) characterizes $\mathrm{PolylogSpace}$. Finally, by an analogous argument that proves the well-known relationship $\mathrm{PSPACE}\subseteq\mathrm{DTIME}(2^{n^{O(1)}})$, it follows that $\mathrm{PolylogSpace}\subseteq\mathrm{DTIME}(2^{\log^{O(1)}n})$.

7.1 The Complexity Class $\mathrm{PolylogSpace}$

Let $L(M)$ denote the class of structures of a given signature $\sigma$ accepted by a direct-access Turing machine $M$. We say that $L(M)\in\mathrm{DSPACE}[f(n)]$ if $M$ visits at most $O(f(n))$ cells in each work-tape before accepting or rejecting an input structure whose domain is of size $n$. We define the class of all languages decidable by a deterministic direct-access Turing machines in polylogarithmic space as follows:

[TABLE]

Note that it is equivalent whether we define the class $\mathrm{PolylogSpace}$ by means of direct-access Turing machines or random-access Turing machines. Indeed, by Theorem 1 and by the fact that the (standard) binary encoding of a structure $\mathbf{A}$ is of size polynomial with respect to the cardinality of its domain $A$, the following corollary is immediate.

Corollary 1**.**

A class of finite ordered structures $\cal C$ of some fixed vocabulary $\sigma$ is decidable by a random-access Turing machine working in $\mathrm{PolylogSpace}$ with respect to $\hat{n}$, where $\hat{n}$ is the size of the binary encoding of the input structure, iff $\cal C$ is decidable by a direct-access Turing machine in $\mathrm{PolylogSpace}$ with respect to $n$, where $n$ is the size of the domain of the input structure.

Moreover, in the context of $\mathrm{PolylogSpace}$, there is no need for random-access address-tape for the input; $\mathrm{PolylogSpace}$ defined with random-access Turing machines coincide with $\mathrm{PolylogSpace}$ defined with (standard) Turing machines that have sequential access to the input.

Proposition 2**.**

A class of finite ordered structures $\cal C$ of some fixed vocabulary $\sigma$ is decidable by a random-access Turing machine working in $\mathrm{PolylogSpace}$ with respect to $\hat{n}$ iff $\cal C$ is decidable by a standard (sequential-access) Turing machine in $\mathrm{PolylogSpace}$ with respect to $\hat{n}$, where $\hat{n}$ is the size of the binary encoding of the input structure.

Proof.

We give the idea behind the proof; the proof itself is straightforward. We take as the definition of the standard (sequential-access) Turing machine the definition of the random-access Turing machine given in Section 3, except that we suppose a sequential-access read-only-head for the input tape, and remove the address-tape.

A random-access Turing machine $M_{r}$ can simulate a sequential-access Turing machine $M_{s}$ directly by using its address-tape to simulate the movement of the head of the sequential-access input-tape. In the simulation, when the head of the input-tape of $M_{s}$ is on the $i+1$-th cell, the address-tape of $M_{r}$ holds the number $i$ in binary, and hence refers to the $i+1$-th cell of the input. When the head of the input-tape of $M_{s}$ moves right, the machine $M_{r}$ will increase the binary number in its address-tape by one. Similarly, when the head of the input-tape of $M_{s}$ moves left, the machine $M_{r}$ will decrease the binary number in its address-tape by one. A total of $\lceil\log n\rceil$ bits suffices to access any bit of an input of length $n$. Clearly increasing or decreasing a binary number of length at most $\lceil\log n\rceil$ by one can be done in $\mathrm{PolylogSpace}$. The rest of the simulation is straightforward.

The simulation of the other direction is a bit more complicated, as after each time the content of the address-tape of the random-access machine is updated, we need to calculate the corresponding position of the head of the input-tape of the sequential-access machine. However, this computation can be clearly done in $\mathrm{PolylogSpace}$: We use a work-tape of the sequential-access machine to mimic the address-tape of the sequential-access machine, and an additional work-tape as a binary counter. After each computation step of the random-access machine, the sequential-access machine moves the head of its input tape to its leftmost cell, formats the work-tape working as a binary counter to contain exactly the binary number that is written on the address-tape. Then the sequential-access machine moves the head of its input-tape right step-by-step simultaneously decreasing the binary counter by $1$. Once the binary counter reaches [math], the head of the input tape is in correct position. The rest of the simulation is straightforward. ∎

Since the function $\left\lceil\log n\right\rceil$ is space constructible (s.c. for short) (see [16], where these functions are denoted as proper), and for any two s.c. functions their product is also s.c., we get that for any $k\geq 1$ the function $(\left\lceil\log n\right\rceil)^{k}$ is s.c. Hence, by Savitch’s theorem, we obtain the following result.

Fact 1**.**

For any $k\geq 1$, it holds that $\mathrm{NSPACE}[(\left\lceil\log n\right\rceil)^{k}]\subseteq\mathrm{DSPACE}[(\left\lceil\log n\right\rceil)^{2k}]$. Thus, nondeterministic and deterministic $\mathrm{PolylogSpace}$ coincide.

7.2 Index logic with partial fixed point operators captures $\mathrm{PolylogSpace}$

To encode a configuration of polylogarithmic size, we follow a similar strategy as in Theorem 2, i.e., in the proof of the characterization of $\mathrm{PolylogTime}$ by $\mathrm{IL(IFP)}$. The difference here is that there is no reason to encode the whole history of a computation in the fixed point. At a time step $t$ it suffices that the configuration of the machine at time step $t-1$ is encoded; hence, we may drop the variables $\bar{t}$, from the fixed point formula defined on page 5.3. Moreover, we make a small alteration to the Turing machines so that acceptance on an input structure will correspond to the existence of a partial fixed point.

Theorem 5**.**

Over ordered finite structures, $\mathrm{IL(PFP)}$ captures $\mathrm{PolylogSpace}$.

Proof.

The direction of the proof that argues that IL(PFP) can indeed be evaluated in $\mathrm{PolylogSpace}$ is straightforward. Let $\psi$ be an IL(PFP)-sentence, we only need to show that there exists a direct-access Turing machine $M_{\psi}$ working in $O(\log^{d}n)$ space, for some constant $d$, such that for every structure $\mathbf{A}$ and valuation $\it{val}$, it holds that $\mathbf{A}\in L(M_{\psi})$ iff $\mathbf{A},\it{val}\models\psi$. Note that, in an induction on the structure of $\psi$, all the cases, except the case for the $\mathrm{PFP}$ operator, are as in the proof of Theorem 2. Clearly if a formula can be evaluated in $\mathrm{PolylogTime}$ it can also be evaluated in $\mathrm{PolylogSpace}$. For the case of the $\mathrm{PFP}$ operator (using a similar strategy as in [28]), we set a counter to $2^{\log^{r}n}$, using exactly $\log^{r}n$ cells in a work-tape, where $r$ is the arity of the relation variable $X$ bounded by the $\mathrm{PFP}$ operator. To evaluate the $\mathrm{PFP}$ operator, say on a formula $\varphi(\bar{\mathtt{x}},X)$, $M$ will iterate evaluating $\varphi$, decreasing the counter in each iteration. When the counter gets to [math], $M$ checks whether the contents of the relation $X$ is equal to its contents in the following cycle, and whether the tuple given in the $\mathrm{PFP}$ application belongs to it. If both answers are positive, then $M$ accepts, otherwise, it rejects. This suffices to find the fixed point (or to conclude that it does not exist), as there are $2^{\log^{r}n}$ many relations of arity $r$ with domain $\{0,\dots,\lceil\log n\rceil-1\}$.

For the converse, let $M=(Q,\Sigma,\delta,q_{0},F,\sigma)$ be an $m$-tape direct-access Turing machine that works in $\mathrm{PolylogSpace}$. As in the proof of Theorem 2, we assume w.l.o.g., that $F=\{q_{a}\}$ (i.e., there is only one accepting state), $|Q|=a+1$, and $Q=\{q_{0},q_{1},\ldots,q_{a}\}$. In addition to the assumptions made in the proof of Theorem 2, we assume that once the machine reaches an accepting state, it will not change its configuration any longer; that is, all of its heads stay put, and write the same symbol as the head reads. Note that the machine $M$ accepts if and only if $M$ is in the same accepting configuration during two consecutive time steps.

We build an IL(PFP)-sentence $\psi_{M}$ such that for every structure $\mathbf{A}$ and valuation $\it{val}$, it holds that $\mathbf{A}\in L(M)$ iff $\mathbf{A},\it{val}\models\psi_{M}$. The formula is a derivative of that of Theorem 2 and is defined using a simultaneous PFP operator. In the formula below, $S_{q_{0}},\ldots,S_{q_{a}}$ denote [math]-ary relation variables that range over the values true and false. We define

[TABLE]

where

[TABLE]

[TABLE]

[TABLE]

[TABLE]

The formulae used in the PFP operator are defined in the same way as in Theorem 2; with the following two exceptions.

The formulae of the form $\alpha^{0}_{i}(\bar{p},\bar{t}-1)$ are replaced with the analogous formulae $\alpha^{0}_{i}(\bar{p})$ obtained, by simply removing the variables referring to time steps. 2. 2.

Subformulas of the form $\bar{t}\sim 0$ are replaces with $\neg S_{q_{0}}\land\ldots\land\neg S_{q_{a-1}}$, which will be true only on the first iteration of the fixed point calculation.

Following the proof of Theorem 2, it is now easy to show that $\mathbf{A},\it{val}\models\psi_{M}$ if and only if $M$ accepts $\mathbf{A}$. ∎

8 Discussion

An interesting open question concerns order-invariant queries. Indeed, while index logic is defined to work on ordered structures, it is natural to try to understand which queries about ordered structures that are actually invariant of the order, are computable in PolylogTime. Results of the kind given by Proposition 1 already suggest that very little may be possible. Then again, any polynomial-time numerical property of the size of the domain is clearly computable. We would love to have a logical characterization of the order-invariant queries computable in PolylogTime.

Another natural direction is to get rid of Turing machines altogether and work with a RAM model working directly on structures, as proposed by Grandjean and Olive [32]. Plausibly by restricting their model to numbers bounded in value by a polynomial in $n$ (the size of the structure), we would get an equivalent PolylogTime complexity notion.

In this vein, we would like to note that extending index logic with numeric variables that can hold values up to a polynomial in $n$, with arbitrary polynomial-time functions on these, would be useful syntactic sugar that would, however, not increase the expressive power.