The amazing mixed polynomial closure and its applications to two-variable first-order logic

TL;DR

This paper introduces a new restriction called mixed polynomial closure (MPol) and explores its applications to decision problems and hierarchies in two-variable first-order logic, showing decidability results for membership and separation.

Contribution

It defines and studies the new mixed polynomial closure (MPol), demonstrating its ability to define hierarchies and establish decidability of membership and separation in two-variable first-order logic.

Findings

MPol preserves decidability of membership under mild conditions.

MPol allows defining language hierarchies mostly using this operator.

Decidability of separation is established for the hierarchy with linear order.

Abstract

Polynomial closure is a standard operator which is applied to a class of regular languages. In the paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). The first two were known while MPol is new. We look at two decision problems that are defined for every class C. Membership takes a regular language as input and asks if it belongs to C. Separation takes two regular languages as input and asks if there exists a third language in C including the first one and disjoint from the second. We prove that LPol, RPol and MPol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of separation under much stronger hypotheses. We apply these results to natural hierarchies. First, we look at several language theoretic hierarchies that are built by applying LPol, RPol and MPol recursively to a single input class. We prove that these hierarchies can actually be defined using almost exclusively MPol. We also consider quantifier alternation hierarchies for two-variable first-order logic and prove that one can climb them using MPol. The result is generic in the sense that it holds for most standard choices of signatures. We use it to prove that for most of these choices, membership is decidable for all levels in the hierarchy. Finally, we prove that separation is decidable for the hierarchy of two-variable first-order logic equipped with only the linear order.