nonelementary problem
In computational complexity theory, a nonelementary problem{{citation
| last1 = Vorobyov | first1 = Sergei
| last2 = Voronkov | first2 = Andrei|author2link = Andrei Voronkov
| contribution = Complexity of Nonrecursive Logic Programs with Complex Values
| doi = 10.1145/275487.275515
| isbn = 978-0-89791-996-8
| location = New York, NY, USA
| pages = 244–253
| publisher = ACM
| title = Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS '98)
| year = 1998| citeseerx = 10.1.1.39.8822
| s2cid = 15631793
}}. is a problem that is not a member of the class ELEMENTARY. As a class it is sometimes denoted as NONELEMENTARY.
Examples of nonelementary problems that are nevertheless decidable include:
- the problem of regular expression equivalence with complementation{{citation|first=Larry J.|last=Stockmeyer|authorlink=Larry Stockmeyer|title=The Complexity of Decision Problems in Automata Theory and Logic|series=Ph.D. dissertation|year=1974|url=http://people.csail.mit.edu/meyer/Stockmeyer-thesis.pdf|publisher=Massachusetts Institute of Technology}}
- the decision problem for monadic second-order logic over trees (see S2S){{citation
| last = Libkin | first = Leonid|authorlink = Leonid Libkin
| arxiv = cs.LO/0606062
| doi = 10.2168/LMCS-2(3:2)2006
| issue = 3
| journal = Logical Methods in Computer Science
| mr = 2295773
| page = 3:2, 31
| title = Logics for unranked trees: an overview
| volume = 2
| year = 2006}}.
- the decision problem for term algebras{{citation
| last = Vorobyov | first = Sergei
| contribution = An improved lower bound for the elementary theories of trees
| doi = 10.1007/3-540-61511-3_91
| pages = 275–287
| publisher = Springer
| series = Lecture Notes in Computer Science
| title = Automated Deduction — CADE-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 – August 3, 1996, Proceedings
| volume = 1104
| year = 1996| isbn = 978-3-540-61511-8
| citeseerx = 10.1.1.39.1499
}}.
- satisfiability of W. V. O. Quine's fluted fragment of first-order logic{{citation
| last1 = Pratt-Hartmann | first1 = Ian
| last2 = Szwast | first2 = Wieslaw
| last3 = Tendera | first3 = Lidia
| editor1-last = Talbot | editor1-first = Jean-Marc
| editor2-last = Regnier | editor2-first = Laurent
| contribution = Quine's fluted fragment is non-elementary
| doi = 10.4230/LIPIcs.CSL.2016.39 | doi-access = free
| pages = 39:1–39:21
| publisher = Schloss Dagstuhl - Leibniz-Zentrum für Informatik
| series = LIPIcs
| title = 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France
| volume = 62
| year = 2016}}
- deciding β-convertibility of two closed terms in typed lambda calculus{{citation
| last = Statman | first = Richard|authorlink = Richard Statman
| title = The typed λ-calculus is not elementary recursive
| doi = 10.1016/0304-3975(79)90007-0
| journal = Theoretical Computer Science
| volume = 9
| pages = 73–81
| year = 1979
| hdl = 2027.42/23535
| hdl-access = free
}}.
- reachability in vector addition systems; it is Ackermann-complete.{{cite conference |last1=Czerwiński |first1=Wojciech |last2=Orlikowski |first2=Łukasz |title=Reachability in Vector Addition Systems is Ackermann-complete | date=2021 | conference=2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) | arxiv=2104.13866}}{{Cite web |last=Brubaker |first=Ben |date=4 December 2023 |title=An Easy-Sounding Problem Yields Numbers Too Big for Our Universe |url=https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/ |website=Quanta Magazine}}
- reachability in Petri nets; it is Ackermann-complete.{{Cite book |last=Leroux |first=Jerome |chapter=The Reachability Problem for Petri Nets is Not Primitive Recursive |date=February 2022 |title=2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) |chapter-url=https://ieeexplore.ieee.org/document/9719763 |publisher=IEEE |pages=1241–1252 |doi=10.1109/FOCS52979.2021.00121 |isbn=978-1-6654-2055-6|arxiv=2104.12695 }}