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 [math]\displaystyle{ i }[/math]th order and non-deterministic algorithms the time of which is bounded by [math]\displaystyle{ i-1 }[/math] levels of exponentials.

Definitions and notations

We define higher-order variable, a variable of order [math]\displaystyle{ i\gt 1 }[/math] has got an arity [math]\displaystyle{ k }[/math] and represent any set of [math]\displaystyle{ k }[/math]-tuples of elements of order [math]\displaystyle{ i-1 }[/math]. 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[math]\displaystyle{ ^i }[/math] is the set of formulae where variable's order are at most [math]\displaystyle{ i }[/math]. HO[math]\displaystyle{ ^i_j }[/math] is the subset of the formulae of the form [math]\displaystyle{ \phi=\exists \overline{X^i_1}\forall\overline{X_2^i}\dots Q \overline{X_j^i}\psi }[/math] where [math]\displaystyle{ Q }[/math] is a quantifier, [math]\displaystyle{ Q \overline{X^i} }[/math] means that [math]\displaystyle{ \overline{X^i} }[/math] is a tuple of variable of order [math]\displaystyle{ i }[/math] with the same quantification. So it is the set of formulae with [math]\displaystyle{ j }[/math] alternations of quantifiers of [math]\displaystyle{ i }[/math]th order, beginning by and [math]\displaystyle{ \exists }[/math], followed by a formula of order [math]\displaystyle{ i-1 }[/math].

Using the tetration's standard notation, [math]\displaystyle{ \exp_2^0(x)=x }[/math] and [math]\displaystyle{ \exp_2^{i+1}(x)=2^{\exp_2^{i}(x)} }[/math]. [math]\displaystyle{ \exp_2^{i+1}(x)=2^{2^{2^{2^{\dots^{2^{x}}}}}} }[/math] with [math]\displaystyle{ i }[/math] times [math]\displaystyle{ 2 }[/math]

Property

Normal form

Every formula of [math]\displaystyle{ i }[/math]th order is equivalent to a formula in prenex normal form, where we first write quantification over variable of [math]\displaystyle{ i }[/math]th order and then a formula of order [math]\displaystyle{ i-1 }[/math] in normal form.

Relation to complexity classes

HO is equal to ELEMENTARY functions. To be more precise, [math]\displaystyle{ \mathsf{HO}^i_0 = \mathsf{NTIME}(\exp_2^{i-2}(n^{O(1)})) }[/math], it means a tower of [math]\displaystyle{ (i-2) }[/math] 2s, ending with [math]\displaystyle{ n^c }[/math] where [math]\displaystyle{ c }[/math] is a constant. A special case of it is that [math]\displaystyle{ \exists\mathsf{SO}=\mathsf{HO}^2 0=\mathsf{NTIME}(n^{O(1)})={\color{Blue}\mathsf{NP}} }[/math], which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, [math]\displaystyle{ \mathsf{HO}^i j={\color{Blue}\mathsf{NTIME}}(\exp 2^{i-2}(n^{O(1)})^{\Sigma j^{\mathsf P}}) }[/math]

See also

• FO (complexity)
• SO (complexity)

External links

• zoo about HO.