The Descriptive Complexity of Decision Problems through Logics with Relational Fixed-Point and Capturing Results
Márcia Farias, Ana Teresa Martins, Francicleber Martins Ferreira · Electronic Notes in Theoretical Computer Science · 2017
In this work, we generalize the classical fixed-point logics using relations instead of operators in order to capture the notion of nondeterminism. The basic idea is that we use loops in a relation instead of fixed-points of a function, that is, X is a fixed-point of the relation R in case the pair ( X , X ) belongs to R . We introduce the notion of initial fixed-point of an inflationary relation R and the associated operator rifp . We denote by RIFP the first-order logic with the inflationary relational fixed-point operator rifp and show that it captures the polynomial hierarchy using a translation to second-order logic. We also consider the fragment RIFP 1 with the restriction that the rifp operator can be applied at most once. We show that RIFP 1 captures the class NP and compare our logic with the nondeterministic fixed-point logic proposed by Abiteboul, Vianu and Vardi in [S. Abiteboul, M. Vardi, and V. Vianu. Fixpoint logics, relational machines, and computational complexity. Journal of the ACM , 44-1:30–56, 1997].