Nonelementary problem

In computational complexity theory, a nonelementary problem ^[1] 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 ^[2]
• the decision problem for monadic second-order logic over trees (see S2S) ^[3]
• the decision problem for term algebras ^[4]
• satisfiability of W. V. O. Quine's fluted fragment of first-order logic ^[5]
• deciding β-convertibility of two closed terms in typed lambda calculus ^[6]
• reachability in vector addition systems; it is Ackermann-complete. ^{[7] [8]}
• reachability in Petri nets; it is Ackermann-complete. ^{[9] [8]}

References

1. Vorobyov, Sergei; Voronkov, Andrei (1998), "Complexity of Nonrecursive Logic Programs with Complex Values", Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS '98), New York, NY, USA: ACM, pp. 244–253, CiteSeerX   10.1.1.39.8822 , doi:10.1145/275487.275515, ISBN   978-0-89791-996-8, S2CID   15631793 .
2. Stockmeyer, Larry J. (1974), The Complexity of Decision Problems in Automata Theory and Logic (PDF), Ph.D. dissertation, Massachusetts Institute of Technology
3. Libkin, Leonid (2006), "Logics for unranked trees: an overview", Logical Methods in Computer Science, 2 (3) 2244: 3:2, 31, arXiv: cs.LO/0606062 , doi:10.2168/LMCS-2(3:2)2006, MR   2295773 .
4. Vorobyov, Sergei (1996), "An improved lower bound for the elementary theories of trees", Automated Deduction — CADE-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 – August 3, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1104, Springer, pp. 275–287, CiteSeerX   10.1.1.39.1499 , doi:10.1007/3-540-61511-3_91, ISBN   978-3-540-61511-8 .
5. Pratt-Hartmann, Ian; Szwast, Wieslaw; Tendera, Lidia (2016), "Quine's fluted fragment is non-elementary", in Talbot, Jean-Marc; Regnier, Laurent (eds.), 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, LIPIcs, vol. 62, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 39:1–39:21, doi: 10.4230/LIPIcs.CSL.2016.39 , ISBN   978-3-95977-022-4
6. Statman, Richard (1979), "The typed λ-calculus is not elementary recursive", Theoretical Computer Science , 9: 73–81, doi:10.1016/0304-3975(79)90007-0, hdl: 2027.42/23535 .
7. Czerwiński, Wojciech; Orlikowski, Łukasz (2021). Reachability in Vector Addition Systems is Ackermann-complete. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.13866 .
8. Brubaker, Ben (4 December 2023). "An Easy-Sounding Problem Yields Numbers Too Big for Our Universe". Quanta Magazine .
9. Leroux, Jerome (February 2022). "The Reachability Problem for Petri Nets is Not Primitive Recursive". 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). IEEE. pp. 1241–1252. arXiv: 2104.12695 . doi:10.1109/FOCS52979.2021.00121. ISBN   978-1-6654-2055-6.