On Higher Order Query Languages which on Relational Databases Collapse to Second Order Logic

TL;DR

This paper investigates higher-order query languages in relational databases, showing that certain fragments of third-order and higher-order logics can be effectively translated into second-order logic, simplifying their expressive complexity.

Contribution

It defines a polynomial fragment of third-order and higher-order logics and proves these fragments collapse to second-order logic, simplifying their expressive power.

Findings

Polynomial third-order logic fragments collapse to SO

Higher-order logic fragments with polynomial bounds also collapse to SO

Constructive translations from higher-order to second-order logic are provided

Abstract

In the framework of computable queries in Database Theory, there are many examples of queries to (properties of) relational database instances that can be expressed by simple and elegant third order logic ($\mathrm{TO}$) formulae. In many of those properties the expressive power of $\mathrm{TO}$ is not required, but the equivalent second order logic ($\mathrm{SO}$) formulae can be very complicated or unintuitive. From the point of view of the study of highly expressive query languages, it is then relevant to identify fragments of $\mathrm{TO}$ (and, in general, of higher-order logics of order $\geq 3$) which do have an $\mathrm{SO}$ equivalent formula. In this article we investigate this precise problem as follows. Firstly, we define a general schema of $\exists$TO formulas which consists of existentially quantifying a third-order linear digraph of polynomial length, that is, a sequence of structures that represents a computation, by explicitly stating which operations are the ones which can be involved in the construction of a given structure in the sequence, when applied to the previous one. Then we give a constructive proof of the fact that all $\exists$TO sub formulas of that schema can be translated into an equivalent SO formula. Secondly, aiming to formally characterize the fragment of TO which can be translated to SO, we define a restriction of TO, which we denote TO$^{P}$, for polynomial TO, and we give a constructive proof on the fact that it collapses to SO. We define TO$^{P}$ as the fragment of TO where valuations can assign to TO relation variables only TO relations whose cardinalities are bounded by a polynomial that depends on the quantifier. Moreover, we define a similar restriction for every higher order logic of order $i \geq 4$, which we denote $\mathrm{HO}^{i,P}$, and give a constructive proof of the fact that for all $i \geq 4$, $\mathrm{HO}^{i,P}$ collapses to SO.