HO (complexity)

From Wikipedia, the free encyclopedia
Jump to: navigation, search

High-order logic is an extension of first-order and second-order with high order quantifiers. In descriptive complexity we can see that it is equal to the ELEMENTARY functions.[1] There is a relation between the ith order and non determinist algorithm the time of which is with i-1 level of exponentials.

Definitions and notations[edit]

We define high-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. High 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^i_j is the subset of the formulae of the form \phi=\exists \overline{X^i_1}\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 ith order, beginning by and \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


Normal form[edit]

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

Relation to complexity classes[edit]

HO is equal to ELEMENTARY functions. To be more precise, \text{HO}^i_0 = \text{NTIME}(\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 \exists{}SO=HO^2_0=NTIME(n^{O(1)})=NP, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, HO^i_j=NTIME(\exp_2^{i-2}(n^{O(1)})^{\Sigma_j^{\rm P}})


  1. ^ Lauri Hella and José María Turull-Torres (2006), "Computing queries with higher-order logics", Theoretical Computer Science ((what is called "number" in bibtex) ed.) (Essex, UK: Elsevier Science Publishers Ltd.) 355 (2): 197–214, doi:10.1016/j.tcs.2006.01.009, ISSN 0304-3975 

External links[edit]