FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

Authors: Yijia Chen, Moritz Mueller and Keita Yokoyama

Paper Information

Title:A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Authors:Yijia Chen, Moritz Mueller and Keita Yokoyama
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:halting problem, parameterized AC^0, linear time hierarchy, the MRDP theorem
Abstract:

ABSTRACT. The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [Chen and Flum, 2012]. Among others, if p-Halt is in para-AC^0, the parameterized version of the circuit complexity class AC^0, then AC^0, or equivalently, (+,\times)-invariant FO, has a logic. Although it is widely believed that p-Halt\notin para-AC^0, we show that the problem is hard to settle by establishing a connection to the question in classical complexity of whether NE\not\subseteq LINH. Here, LINH denotes the linear time hierarchy.

On the other hand, we suggest an approach toward proving NE\not\subseteq LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson-Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE\not\subseteq LINH. Interestingly, central to this result is a para-AC^0 lower bound for the parameterized model-checking problem for FO on arithmetical structures.

Pages:10
Talk:Jul 09 12:00 (Session 47D)
Paper: