Geodesic
The expressiveness of looping terms in the semantic programming
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 380-394.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: semantic programming, bounded quantification, reasoning complexity.
Mots-clés : list structures 
@article{SEMR_2020_17_a7,
     author = {S. Goncharov and S. Ospichev and D. Ponomaryov and D. Sviridenko},
     title = {The expressiveness of looping terms in the semantic programming},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {380--394},
     publisher = {mathdoc},
     volume = {17},
     year = {2020},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2020_17_a7/}
}
TY  - JOUR
AU  - S. Goncharov
AU  - S. Ospichev
AU  - D. Ponomaryov
AU  - D. Sviridenko
TI  - The expressiveness of looping terms in the semantic programming
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2020
SP  - 380
EP  - 394
VL  - 17
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2020_17_a7/
LA  - en
ID  - SEMR_2020_17_a7
ER  - 
%0 Journal Article
%A S. Goncharov
%A S. Ospichev
%A D. Ponomaryov
%A D. Sviridenko
%T The expressiveness of looping terms in the semantic programming
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2020
%P 380-394
%V 17
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2020_17_a7/
%G en
%F SEMR_2020_17_a7
S. Goncharov; S. Ospichev; D. Ponomaryov; D. Sviridenko. The expressiveness of looping terms in the semantic programming. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 380-394. http://geodesic.mathdoc.fr/item/SEMR_2020_17_a7/

[1] S. Goncharov, D. Sviridenko, “$\Sigma$-Programming”, Transl., Ser. 2, Am. Math. Soc., 142 (1989), 101–121 | Zbl

[2] S. Goncharov, D. Sviridenko, “Theoretical Aspects of $\Sigma$-programming”, Lect. Notes Comp. Sci., 215, 1986, 169–179 | MR | Zbl

[3] S. Aleksandrova, N. Bazhenov, “On Decidability of List Structures”, Sib. Math. J., 60:3 (2019), 377–388 | MR | Zbl

[4] S. Goncharov, “Conditional Terms in Semantic Programming”, Sib. Math. J., 58:5 (2017), 794–800 | MR | Zbl

[5] S. Arora, B. Barak, Computational Complexity. A Modern Approach, Cambridge University Press, Cambridge, 2009 | MR | Zbl

[6] C. Papadimitriou, Computational Complexity, Addison-Wesley, Amsterdam, 1994 | MR | Zbl

[7] S. Goncharov, D. Sviridenko, “The Logic Language of Polynomial Computability”, Dokl. Math., 99:2 (2019), 121–124 | Zbl

[8] S. Goncharov, D. Sviridenko, “Recursive Terms in Semantic Programming”, Sib. Math. J., 59:6 (2018), 1014-–1023 | MR | Zbl

[9] A. Mantsivoda, D. Ponomaryov, “A Formalization of Document Models with Semantic Modelling”, Izv. Irkutsk. Gos. Univ., Ser. Mat., 27 (2019), 36–54 | MR

[10] S. Ospichev, D. Ponomarev, “On the Complexity of Formulas in Semantic Programming”, Sib. Electron. Math. Izv., 15 (1918), 987–995 | MR | Zbl

[11] L. Stockmeyer, A. Meyer, “Word Problems Requiring Exponential Time: Preliminary Report”, Proc. 5th ann. ACM Symp. Theor. Comput. (Austin, 1973), 1–9 | MR | Zbl

[12] E. B{ö}rger, E. Gr{ä}del, Y. Gurevich, The Classical Decision Problem, Perspectives in Mathematical Logic, Springer, Berlin, 1997 | MR | Zbl