|
Sib. Èlektron. Mat. Izv., 2020, Volume 17, Pages 380–394
(Mi semr1218)
|
|
|
|
Mathematical logic, algebra and number theory
The expressiveness of looping terms in the semantic programming
S. Goncharovab, S. Ospichevab, D. Ponomaryovacb, D. Sviridenkoab a Sobolev Institute of Mathematics, 4, Koptyuga ave., Novosibirsk, 630090, Russia
b Novosibirsk State University, 2, Pirogova str., Novosibirsk, 630090, Russia
c Ershov Institute of Informatics Systems, 6, Lavrentyeva ave., Novosibirsk, 630090, Russia
Abstract:
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, list structures, bounded quantification, reasoning complexity.
Funding Agency |
Grant Number |
Russian Science Foundation  |
17-11-01176 |
The authors were supported by the Russian Science Foundation (Grant No. 17-11-01176). |
DOI:
https://doi.org/10.33048/semi.2020.17.024
Full text:
PDF file (193 kB)
References:
PDF file
HTML file
Bibliographic databases:
UDC:
510.5
MSC: 03D15, 68Q15 Received November 19, 2019, published March 10, 2020
Language:
Citation:
S. Goncharov, S. Ospichev, D. Ponomaryov, D. Sviridenko, “The expressiveness of looping terms in the semantic programming”, Sib. Èlektron. Mat. Izv., 17 (2020), 380–394
Citation in format AMSBIB
\Bibitem{GonOspPon20}
\by S.~Goncharov, S.~Ospichev, D.~Ponomaryov, D.~Sviridenko
\paper The expressiveness of looping terms in the semantic programming
\jour Sib. \`Elektron. Mat. Izv.
\yr 2020
\vol 17
\pages 380--394
\mathnet{http://mi.mathnet.ru/semr1218}
\crossref{https://doi.org/10.33048/semi.2020.17.024}
\isi{http://gateway.isiknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&DestLinkType=FullRecord&DestApp=ALL_WOS&KeyUT=000518787600001}
Linking options:
http://mi.mathnet.ru/eng/semr1218 http://mi.mathnet.ru/eng/semr/v17/p380
Citing articles on Google Scholar:
Russian citations,
English citations
Related articles on Google Scholar:
Russian articles,
English articles
|
Number of views: |
This page: | 128 | Full text: | 43 | References: | 1 |
|