RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Sib. Èlektron. Mat. Izv.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


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

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Number of views:
    This page:76
    Full text:12

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020