Characterizing the Exponential-Space Hierarchy Via Partial Fixpoints

TL;DR

This paper extends the classical descriptive complexity characterization of PSPACE-queries to k-EXPSPACE-queries, using higher-order logic with partial fixpoints, showing increased expressiveness without ordering restrictions for k>1.

Contribution

It generalizes the characterization of space-bounded queries to higher exponential space classes using higher-order logic with partial fixpoints.

Findings

Characterizes k-EXPSPACE-queries with higher-order logic.

Removes ordering restrictions for k>1.

Establishes a hierarchy of logical expressiveness.

Abstract

The characterization of PSPACE-queries over ordered structures as exactly those expressible in first-order logic with partial fixpoints (Vardi'82) is one of the classical results in the field of descriptive complexity. In this paper, we extend this result to characterizations of k-EXPSPACE-queries for arbitrary k, characterizing them as exactly those expressible in order-k+1-higher-order logic with partial fixpoints. For k>1, the restriction to ordered structures is no longer necessary due to the high expressive power of higher-order logic.