Nominal Topology for Data Languages
Fabian Birkmann, Stefan Milius, Henning Urbat
TL;DR
This work extends profinite/topological methods to data languages by introducing $k$-bounded nominal Stone spaces and pro-orbit-finite words, establishing a robust topological-algebraic framework for recognizability by orbit-finite nominal monoids. It proves a duality between locally $k$-atomic nominal boolean algebras and $k$-bounded nominal Stone spaces, and shows recognizable data languages correspond to clopen subsets of pro-orbit-finite word spaces, via a nominal version of Stone duality. A nominal Reiterman theorem is developed, characterizing classes of orbit-finite nominal monoids that are closed under natural operations as precisely those presented by pro-equations (MSR quotients), with explicit proequations capturing the aperiodic case through $x^{ullet ext{ω}}$-style equations. The framework generalizes classical regular-language theory to data words and suggests extensions to data trees, nominal ω-semigroups, and algebras with binders, providing a unified topological-algebraic lens for data languages.
Abstract
We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces. Assuming globally bounded support sizes, they coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations by establishing a nominal version of Reiterman's pseudovariety theorem.