HO (complexity)

In descriptive complexity, a branch of computational complexity, HO is the complexity class of structures that can be recognized by formulas of higher-order logic. Higher-order logic is an extension of first-order logic and second-order logic with higher-order quantifiers. The class HO is equal to the time complexity class ELEMENTARY. There is a relation between the $i$th order and non-deterministic algorithms the time of which is bounded by $i-1$ levels of exponentials.

Definitions and notations

We define higher-order variable, a variable of order $i>1$ has got an arity $k$ and represent any set of $k$-tuples of elements of order $i-1$. They are usually written in upper-case and with a natural number as exponent to indicate the order. Higher-order logic is the set of FO formulae where we add quantification over higher-order variables, hence we will use the terms defined in the FO article without defining them again.

HO$i^{}$ is the set of formulae where variable's order are at most $i$. HO$\underset{i}{\overset{}{j}}$ is the subset of the formulae of the form $\varphi =\mathrm{\exists }\overline{X_1^i}\mathrm{\forall }\overline{X_2^i}\dots Q\overline{X_j^i}\psi$ where $Q$ is a quantifier, $Q\overline{X^i}$ means that $\overline{X^i}$ is a tuple of variable of order $i$ with the same quantification. So it is the set of formulae with $j$ alternations of quantifiers of $i$th order, beginning by and $\mathrm{\exists }$, followed by a formula of order $i-1$.

Using the tetration's standard notation, ${\exp }_2^0(x)=x$ and ${\exp }_2^{i+1}(x)=2^{{\exp }_2^i(x)}$. ${\exp }_2^{i+1}(x)=2^{2^{2^{2^{{\dots }^{2^x}}}}}$ with $i$ times $2$

Property

Normal form

Every formula of $i$th order is equivalent to a formula in prenex normal form, where we first write quantification over variable of $i$th order and then a formula of order $i-1$ in normal form.

Relation to complexity classes

HO is equal to ELEMENTARY functions. To be more precise, ${\mathsf{H}\mathsf{O}}_0^i=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}({\exp }_2^{i-2}(n^{O(1)}))$, it means a tower of $(i-2)$ 2s, ending with $n^c$ where $c$ is a constant. A special case of it is that $\mathrm{\exists }\mathsf{S}\mathsf{O}={\mathsf{H}\mathsf{O}}^{2}0=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}(n^{O(1)})=\mathsf{N}\mathsf{P}$, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, ${\mathsf{H}\mathsf{O}}^{i}j=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}(\exp 2^{i-2}(n^{O(1)}{)}^{\mathrm{\Sigma }{j}^{\mathsf{P}}})$

See also

• FO (complexity)
• SO (complexity)

External links

• zoo about HO.