💻 computer science

Characterization and Decidability of FC-Definable Regular Languages

This paper demonstrates that not all regular languages are definable in the first-order logic FC and provides a decidable characterization of the FC-definable regular languages using algebraic, automata-theoretic, and concise regular expression criteria.

Original authors: Sam M. Thompson, Nicole Schweikardt, Dominik D. Freydenberger

Published 2026-07-31

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Sam M. Thompson, Nicole Schweikardt, Dominik D. Freydenberger

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Secret Life of Words and the Logic of Patterns

Imagine you are a detective trying to solve a mystery, but instead of fingerprints or alibis, your clues are made entirely of letters and words. In the world of computer science, there is a branch called "logic" that acts like a super-powered magnifying glass. It helps us ask questions about strings of text (like "Does this sentence contain a secret code?") and get a definite yes or no answer. For a long time, the most common tool for this job was a logic that treated words like a row of lockers, where you could check if locker #5 had a 'B' or if locker #10 was empty. This worked great for simple patterns.

But then, researchers invented a new, more adventurous tool called FC. Instead of looking at individual lockers, FC looks at the words themselves as building blocks. It can say things like, "Take this chunk of text, stick it next to that chunk, and see if they match." This is like having a magic glue that can snap pieces of a puzzle together to see if they form a specific shape. This is incredibly useful for modern technology, especially for "document spanners"—the smart systems that scan through massive piles of documents (like legal contracts or medical records) to pull out specific tables of information. The big question was: Is this new magic glue powerful enough to find every regular pattern we might want to look for, or are there some patterns it simply cannot see?

The Paper's Big Discovery: The "Loop-Step" Trap

In this paper, authors Sam Thompson, Nicole Schweikardt, and Dominik Freydenberger tackle that exact question. They wanted to know exactly which regular patterns (the kind of patterns computers are really good at spotting) can be described using this new FC logic. Their answer is a mix of "yes," "no," and "here is exactly how to tell the difference."

First, they proved that FC is not all-powerful. There are perfectly normal, regular patterns that FC simply cannot define. To visualize this, imagine a maze. Some mazes are simple loops you can walk through easily. But FC has a specific weakness: it gets confused by a very specific type of maze trap they call a "loop-step cycle."

Think of a "loop-step cycle" like a dance floor with a group of dancers standing in a circle.

The Loop: If you play a specific song (let's call it "Song A"), every dancer spins in place and ends up exactly where they started.
The Step: If you play a different song ("Song B"), every dancer moves one spot to the right, passing the person next to them.
The Trap: If the "Song A" and "Song B" are made of different basic rhythms (meaning they aren't just repeats of the same beat), FC logic gets stuck. It can't tell the difference between a word that follows this dance pattern and one that doesn't. The authors proved that if a pattern's underlying machine (a Minimal DFA) has this specific "loop-step" dance, FC cannot describe it.

The Three Ways to Spot the Difference

The authors didn't just say "some are impossible"; they gave us three different ways to check if a pattern is safe for FC or if it's trapped in the loop-step cycle. It's like having three different keys to the same door:

The Algebra Key (Group Primitive): This is a mathematical way of looking at the pattern's "fingerprint." If the pattern's fingerprint is "group primitive," it means it's safe. If the fingerprint is too messy or complex, it's not safe.
The Expression Key (Star-Free Closure): This is about how you write the pattern down. The authors found that FC can describe any pattern that can be built using "star-free" expressions (patterns without the infinite "repeat forever" star symbol, but with "not" and "and" allowed) plus the ability to repeat specific, fixed words. It's like saying you can build any valid FC pattern using Lego bricks, but you can only use the "repeat" button on specific, pre-made bricks, not on custom shapes you build yourself.
The Machine Key (The Loop-Step Cycle): This is the most visual one. If you draw the machine that recognizes the pattern, and you see that "loop-step" dance (where one word keeps you in place and another moves you around a circle), then FC cannot define it.

Why This Matters and What's Next

The paper proves that these three keys are actually the same thing. If a pattern fails one test, it fails all three. This is a huge deal because it gives computer scientists a clear rulebook. If you are building a system to search through documents, you now know exactly which patterns you can write in this new FC language and which ones you'll need to use a different tool for.

The authors also showed that checking if a pattern has this "loop-step" trap is a very hard problem for computers to solve—it takes a lot of computing power (specifically, it is PSPACE-complete). This means that while we have a rulebook, actually checking a huge, complex pattern might be like trying to solve a massive jigsaw puzzle in the dark.

Finally, the paper settles a debate about whether we need "regular constraints" (extra rules that force a variable to be a specific type of word) to make FC useful. The answer is a definitive yes. Since FC can't even handle all the simple regular patterns on its own, those extra constraints are absolutely necessary for it to work as a powerful tool for text searching.

In short, the authors didn't just find a new toy; they mapped the entire playground. They showed us where the swings are, where the slides are, and exactly where the "do not enter" signs are for this new logic, ensuring that future developers don't waste time trying to build a rollercoaster on a foundation that can't support it.

Technical Summary: Characterization and Decidability of FC-Definable Regular Languages

Problem Statement

The paper addresses the fundamental question of characterizing the class of regular languages that are definable in FC (First-Order logic over Concatenation). FC is a logic introduced by Freydenberger and Peterfreund that reasons over the set of factors of a finite word using concatenation ( $x \doteq y \cdot z$ ), constant symbols for terminals, and the empty word. Unlike standard first-order logic over words ($FO[<]$), which treats words as sequences of positions, FC treats words as algebraic structures generated by concatenation.

While FC is known to define non-regular languages (e.g., the language of squares $\{ww \mid w \in \Sigma^*\}$ ), it remains unclear which regular languages fall within its expressive power. Specifically, the authors investigate whether the class of FC-definable regular languages constitutes the entire set of regular languages or a proper subset, and if the latter, whether this subset can be effectively characterized and decided.

Methodology

The authors employ a multi-faceted approach combining finite model theory, automata theory, and algebraic language theory to establish a decidable characterization.

Logic and Formalism: The study utilizes the standard definitions of FC-formulas, where atomic formulas represent concatenation relations. The authors distinguish between FC-definable languages and those definable in $FO[<]$.
Algebraic Characterization: The paper introduces the concept of group primitive languages. A regular language $L$ is group primitive if its syntactic morphism $\eta_L$ maps the inverse of any periodic element in the syntactic monoid to a set of words sharing the same primitive root (i.e., $\eta_L^{-1}(g) \subseteq w^*$ for some $w$ ).
Automata Characterization: The authors define a structural property for minimal Deterministic Finite Automata (DFA) called a loop-step cycle. A minimal DFA has a loop-step cycle if there exist two words $w$ and $v$ (with distinct primitive roots) and a sequence of distinct states such that $w$ acts as a loop (returning to the same state) and $v$ acts as a step (advancing the state cyclically).
Regular Expression Characterization: The paper utilizes the star-free closure operator, denoted $SF(\mathcal{C})$ , introduced by Place and Zeitoun. This operator generates the smallest class of languages containing a base class $\mathcal{C}$ , singletons, and closed under union, concatenation, and complement. The authors focus on $SF(\mathcal{R})$ , where $\mathcal{R} = \{w^* \mid w \in \Sigma^*\}$ .
Inexpressibility Proofs: To prove that certain regular languages are not FC-definable, the authors adapt Ehrenfeucht-Fraïssé games. They leverage a result by Lynch regarding structures with addition $(\mathbb{N}, +, A)$ and encode finite sets of natural numbers as words. By constructing a uniform morphism $h$ that maps these encodings to the target alphabet, they demonstrate that if a minimal DFA has a loop-step cycle, the Duplicator can win the game for any number of rounds, implying the language is not definable in FC.

Key Contributions and Results

1. Decidable Characterization

The central result of the paper (Theorem 3.8) establishes the equivalence of four conditions for a regular language $L$ :

$L$ is definable in FC ( $L \in L(FC)$ ).
$L$ belongs to the star-free closure of the class of word powers, $SF(\mathcal{R})$ .
$L$ is a group primitive language.
The minimal DFA for $L$ does not contain a loop-step cycle.

This characterization implies that the class of FC-definable regular languages is a proper subset of the regular languages (for non-unary alphabets). Consequently, extending FC with regular constraints is necessary for it to capture all regular languages in the context of document spanners.

2. Decidability and Complexity

The paper proves that determining whether a regular language (given as a minimal DFA) is FC-definable is PSPACE-complete (Theorem 3.9). This is achieved by showing that the problem of detecting a loop-step cycle in a minimal DFA is PSPACE-complete (Theorem 3.7).

3. Specific Classifications

Star-Free Closure: The authors show that $L(FC) \cap \text{Regular} = SF(\mathcal{R})$ . This class extends star-free languages (definable in $FO[<]$) by allowing the Kleene star of terminal words.
AC0 Relationship: The paper demonstrates that for a binary alphabet, the class $SF(\mathcal{R})$ is a strict subclass of the regular languages in the complexity class $AC^0$ . Specifically, the language of words with an even number of a specific symbol (which is in $AC^0$ ) is not FC-definable because its minimal DFA possesses a loop-step cycle.

4. Proof Techniques

From Algebra to Automata: The proof that "No Loop-Step Cycle $\implies$ Group Primitive" involves constructing specific words based on the periodic elements of the syntactic monoid to show that if a language is not group primitive, a loop-step cycle must exist.
From Automata to Logic: The proof that "Loop-Step Cycle $\implies$ Not FC-Definable" relies on a sophisticated reduction. The authors encode sets of natural numbers into words, use Lynch's theorem to show indistinguishability in addition-based structures, and then map these indistinguishable structures to words via a uniform morphism. This allows them to construct pairs of words that are indistinguishable by FC formulas of bounded quantifier rank but differ in acceptance by the target DFA.

Significance

The paper provides a comprehensive answer to the question of the expressive power of FC over regular languages. Its significance lies in:

Completing the Characterization: It fills a gap in the literature by providing the first decidable characterization of FC-definable regular languages, paralleling the classical characterization of $FO[<]$-definable languages (star-free languages) via aperiodic monoids.
Practical Implications for Document Spanners: By establishing that FC-definable regular languages are a proper subset of all regular languages, the paper justifies the necessity of regular constraints in the generalized core spanner framework. Without these constraints, FC cannot express all regular patterns required for text querying.
Theoretical Bridge: The work connects finite model theory (FC logic), algebraic automata theory (syntactic monoids and group primitive morphisms), and combinatorics on words (primitive roots and loop-step cycles), offering new tools like the loop-step cycle criterion for analyzing the limitations of concatenation-based logics.

The authors conclude that while FC is powerful enough to define non-regular languages, its restriction to regular languages is strictly limited by algebraic and automata-theoretic properties, specifically the absence of certain cyclic behaviors in the minimal automaton.