The Expressiveness of Looping Terms in the Semantic Programming

TL;DR

This paper investigates the complexity of reasoning in extended $ abla_0$-formulas with list terms over hereditarily finite list structures, revealing non-elementary complexity for certain recursive formulas.

Contribution

It analyzes the complexity of model checking and satisfiability for $ abla_0$-formulas with bounded recursive and iterative list terms, establishing non-elementary bounds.

Findings

Set of $ abla_0$-formulas with recursive terms is non-elementary.

Complexity varies with restrictions on iterative and recursive terms.

Results apply to reasoning over hereditarily finite list structures.

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 kEXPTIME, for all $k\geqslant 1$). For $\Delta_0$-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity.