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]
References
- 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.
- Stockmeyer, Larry J. (1974), The Complexity of Decision Problems in Automata Theory and Logic (PDF), Ph.D. dissertation, Massachusetts Institute of Technology
- Libkin, Leonid (2006), "Logics for unranked trees: an overview", Logical Methods in Computer Science, 2 (3): 3:2, 31, arXiv:cs.LO/0606062, doi:10.2168/LMCS-2(3:2)2006, MR 2295773.
- 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.
- 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
- 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.
- 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.