Аннотация:
We consider the language of $\Delta_0$-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of $\Delta_0$-formulas with non-standard list terms, which represent bounded list search, bounded iteration, and bounded recursion. We prove a number of results on the complexity of model checking and satisfiability for these formulas. In particular, we show that the set of $\Delta_0$-formulas with bounded recursive terms true in a given list superstructure $HW(\mathcal{M})$ is non-elementary (it contains the class $\mathrm{kExpTime}$, for all $k\geqslant 1$). For $\Delta_0$-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity.
Ключевые слова:
semantic programming, list structures, bounded quantification, reasoning complexity.
Образец цитирования:
S. Goncharov, S. Ospichev, D. Ponomaryov, D. Sviridenko, “The expressiveness of looping terms in the semantic programming”, Сиб. электрон. матем. изв., 17 (2020), 380–394
\RBibitem{GonOspPon20}
\by S.~Goncharov, S.~Ospichev, D.~Ponomaryov, D.~Sviridenko
\paper The expressiveness of looping terms in the semantic programming
\jour Сиб. электрон. матем. изв.
\yr 2020
\vol 17
\pages 380--394
\mathnet{http://mi.mathnet.ru/semr1218}
\crossref{https://doi.org/10.33048/semi.2020.17.024}
\isi{https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=Publons&SrcAuth=Publons_CEL&DestLinkType=FullRecord&DestApp=WOS_CPL&KeyUT=000518787600001}
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/semr1218
https://www.mathnet.ru/rus/semr/v17/p380
Эта публикация цитируется в следующих 4 статьяx:
А. В. Нечёсов, “Некоторые вопросы полиномиально вычислимых представлений для порождающих грамматик и форм Бэкуса – Наура”, Матем. тр., 25:1 (2022), 134–151
А. В. Нечёсов, “Семантическое программирование и полиномиально вычислимые представления”, Матем. тр., 25:2 (2022), 174–202; A. V. Nechesov, “Semantic programming and polynomially computable representations”, Siberian Adv. Math., 33:1 (2023), 66–85
S. Goncharov, A. Nechesov, “Polynomial analogue of Gandy's fixed point theorem”, Mathematics, 9:17 (2021), 2102
Nikolay Bazhenov, Lecture Notes in Computer Science, 12159, Computer Science – Theory and Applications, 2020, 142