Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.04346

Languages and Recognition in a Category with Factorisation

Harsh Beohar·Mike Cruchten·Georg Struth
View original source ↗Read source document ↗Export metadata ↓

Abstract

Language recognition by homomorphisms is a central construction of algebraic language theory. Initially studied for monoids and semigroups, it has subsequently been expanded to other algebraic structures. Our new categorical account is based on fibrations, which have already seen other applications in automata theory. Languages and surjective homomorphisms give indeed rise to two fibrations, and the notion of language recognition is stable under reindexing. We develop this framework in a category with a factorisation system and address two main technical questions in the fibrational setting. First, we provide sufficient conditions under which languages have syntactic quotients (which is a generalisation of syntactic congruences) and we show how such quotients can be described in some concrete cases using a result by Slomiński. Second, we introduce sufficient conditions under which (regular) languages are closed under certain J-limits and J-colimits.

Explore related subjects

cs.FLcs.LO

Keep this discovery

BibTeXRIS

Harsh Beohar, Mike Cruchten, Georg Struth. 2026-09-03. Languages and Recognition in a Category with Factorisation. https://arxiv.org/abs/2609.04346

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.FL subjectcs.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

Exponential Gaps Between Intuitionistic Linear Extended Frege Systems

In this paper, we establish exponential separations between Extended Frege systems for a range of intuitionistic substructural and linear logics. More precisely, for any logic $L$ below the intuitionistic logic obtained by extending $\mathbf{ILL}$ with structural rules, and any logic $M$ not contained in $L$, we construct a family of $\mathsf{FL_e}$-provable formulas that have short proofs in $M$-Frege but require proofs of exponential size in $L$-Extended Frege. The same result holds in the $!$-free settings, using $\mathbf{IMALL}$ and $\mathbf{FL_e}$ in place of $\mathbf{ILL}$. The key ingredient in proving these separations is a variant of the feasible disjunction property for $L$-Frege, which may be of independent interest.

cs.LO↗
arXiv2026

A note on the reduction from LTLf to LTL

LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words that the original LTLf formula was considering. Such a reduction was originally proposed by De Giacomo and Vardi (IJCAI'13). However, while any LTL formula reduced from LTLf describes an obligation property in the hierarchy of Manna and Pnueli (PODC'90), the aforementioned reduction does not provide an LTL formula that belongs to the syntactic obligation fragment of LTL. This note shows how the reduction was fixed in Spot in order to ensure that the resulting LTL formula is always a syntactic obligation. Doing so allows algorithms specialized to syntactic obligation to be used on LTLf formulas. For instance, in previous work (CAV'26) we described a specialized translation from syntactic obligations to minimal, weak, deterministic Büchi automata that would not be usable with the original reduction.

cs.FL↗
arXiv2026

From Ramsey-Based to Congruence-Based Constructions for Büchi Complementation

The very first construction by J. Richard Büchi himself for complementing a Büchi automaton relies on a fundamental lemma about the division of an arbitrary infinite word into consecutive finite words, which was cleanly proven by invoking a specialized theorem of Ramsey. For that reason, constructions of similar nature have subsequently been labeled as Ramsey-based. Nevertheless, it suffices to have a weaker form of the lemma where the finite words come from a finite number of congruence classes, rather than arbitrary classes, that form a partition of the set of all finite words. The weaker lemma, with support of nicer properties from a congruence, can be proven without Ramsey's theorem. A commonly adopted improvement on such complementation constructions also requires the working of a congruence. This paper recounts the history and reviews using more contemporary terminology wherever possible the relevant concepts and results, to advocate renaming of Ramsey-based constructions as congruence-based constructions.

cs.FL↗