Lune

LICS2022Top-tier venue

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

Thomas Place

2022Year
3Citations
2Top-tier citations

Abstract

Polynomial closure is a standard operator. It takes as input a class of regular languages and builds a new one. In this paper, we investigate three restrictions: left (LP ol), right (RP ol) and mixed polynomial closure (M P ol). The first two were known while M P ol is new. We look at three decision problems that one may associate to each class C: membership (decide if an input regular language belongs to C), separation (decide if two input regular languages can be separated by a third one in C) and covering (which generalizes separation to arbitrarily many inputs). We prove that LP ol, RP ol and M P ol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of covering under much stronger hypotheses.

We apply our results to natural hierarchies that are built from a single input class by applying LP ol, RP ol and M P ol recursively. We prove that these hierarchies can actually be defined using almost exclusively M P ol. We also consider quantifier alternation hierarchies for two-variable first-order logic (FO 2 ) and prove that one can climb them using M P ol. This 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 and covering are decidable for the hierarchy of two-variable first-order logic equipped with only the linear order (FO 2 (<)).

Ask about this paper

Your agent reads all of it.

Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.

Questions to start from

Your agent calls

Luneget_paper_fulltext

Ask in Lune

Free to start. No credit card required.

lune papers fulltext 91d127cc-b908-4725-8c51-34861acb1b4e

Cited by top-tier papers2

Ask how each one uses it

Builds on1

Related papers

Dusk over the sea between two cliffs drawn in fine vertical lines