First-Order Quantifiers and the Syntactic Monoid of Height Fragments of Picture Languages

TL;DR

This paper explores the expressive limits of first-order quantifiers in monadic second-order logic over picture languages, linking logical complexity to algebraic properties of associated word languages' syntactic monoids.

Contribution

It introduces a novel method to measure the complexity of picture languages via height fragments and their syntactic monoids, revealing new separation results based on quantifier alternation.

Findings

Higher quantifier alternations increase expressive power.

Complexity of picture languages relates to the algebraic structure of their fragments.

Lower bounds are established using algebraic characterizations of monoids.

Abstract

We investigate the expressive power of first-order quantifications in the context of monadic second-order logic over pictures. We show that k+1 set quantifier alternations allow to define a picture language that cannot be defined using k set quantifier alternations preceded by arbitrarily many first-order quantifier alternations. The approach uses, for a given picture language L and an integer m > 0 the height-m fragment of L, which is defined as the word language obtained by considering each picture p of height m in L as a word, where the letters of that word are the columns of p. A key idea is to measure the complexity of a regular word language by the group complexity of its syntactic monoid. Given a picture language L, such a word language measure may be applied to each of its height fragments, so that the complexity of the picture language is a function that maps each m to the complexity of the height-m fragment of L. The asymptotic growth rate of that function may be bounded based on the structure of a monadic second-order formula that defines L. The core argument for that lower bound proof is based on Straubing's algebraic characterization of the effect of first-order quantifiers on the syntactic monoid of word languages by means of Rhodes' and Tilson's block product.