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/