HO (complexity)

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 th order and non determinist algorithm the time of which is with level of exponentials.

Definitions and notations

We define high-order variable, a variable of order has got an arity and represent any set of -tuples of elements of order . 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 is the set of formulae where variable's order are at most . HO is the subset of the formulae of the form where is a quantifier, means that is a tuple of variable of order with the same quantification. So it is the set of formulae with alternations of quantifiers of th order, beginning by and , followed by a formula of order .

Using the tetration's standard notation, and . with times

Property

Normal form

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

Relation to complexity classes

HO is equal to ELEMENTARY functions. To be more precise, , it means a tower of 2s, ending with where is a constant. A special case of it is that , which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy,

References

  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
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.