A sorting network in bounded arithmetic (Q638498)

From the text: ``Sorting is one of the most fundamental algorithmic operations, thus it is not surprising that much effort in theoretical computer science was invested in investigation of its computational complexity in various contexts. In particular, its exact parallel complexity was open for a long time. It has been known since the 1960s that it is fairly easy to construct parallel sorting algorithms using \(O(\log^2 n)\) steps [\dots], but it proved quite difficult to further improve on this upper bound. It was only in 1983 when Ajtai et al. [\dots] devised an ingenious algorithm achieving \(O(\log n)\) parallel operations. The algorithm and its analysis were subsequently simplified by Paterson [\dots]. An important feature of the AKS algorithm is that the pattern of comparisons and swaps is fixed in advance independent of the data, hence the construction in fact gives a \textit{sorting network} of depth \(O(\log n)\). (This result is asymptotically optimal, as there is an obvious \(\Omega(\log n)\) depth lower bound.) A sorting network is a structure consisting of comparators connected by wires, where a comparator is a device which takes two inputs and outputs them in sorted order. In the present paper we are going to formalize the core of the AKS sorting network (or rather its version by Paterson) in the theory \(\mathrm{VNC}^1_\ast\) of bounded arithmetic. More precisely, the basic building blocks of the AKS network, the so-called \(\epsilon\)-halvers, are constructed using a certain kind of expander graphs. Construction of the expanders is a separate issue rather tangential to analysis of the main part of the network, we thus leave it out completely: we simply assume that \(\mathrm{VNC}^1_\ast\) proves the existence of appropriate expanders, and all our results are conditional on this assumption. We note that some research towards formalization of expanders in bounded arithmetic is in progress [\dots]. Our formalization is carried out in a not quite standard theory \(\mathrm{VNC}^1_\ast\) introduced for this very purpose in [the author, Ann. Pure Appl. Logic 162, No. 4, 322--340 (2011; Zbl 1239.03035)]. This theory was chosen to satisfy two conflicting goals. On the one hand, the application to monotone sequent calculus described above requires that propositional translations of \(\Pi_1^B\)-formulas provable in the theory have polynomial-size proofs in LK or, equivalently, in Frege systems, hence we need some kind of an \(\mathrm{NC}^1\)-theory. On the other hand, successful formalization of the AKS network requires at the very least that the theory proves that the network can be evaluated. We thus need the ability to evaluate (sufficiently uniformly described) circuits of logarithmic depth. The standard \(\mathrm{NC}^1\)-theory \(\mathrm{VNC}^1\) is too weak for this purpose, as evaluation of log-depth circuits is not known to be possible in uniform \(\mathrm{NC}^1\) (i.e., ALOGTIME). \(\mathrm{VNC}^1\) can only evaluate log-depth circuits described by their extended connection language [\dots], which is however not available for the AKS network [\dots]. The network is defined as a sequence of steps, each of which is described locally: the \(n\) elements are organized in a tree-like structure (varying in each step), and constant-depth subnetworks are applied to parts of this structure. A longer sequence of steps can move an element quite far in the structure in a hard to predict way (this is, after all, one of the reasons why the network can sort), and there does not seem to be any way of globally describing the ECL of the network other than to follow the path through the circuit step by step. (Note that this is unrelated to the complexity of description of expanders used in the construction: in fact, the expander-based gadgets have constant depth, hence their ECL is no harder than their direct connection language.)''