Logic and Computation through the Lens of Semirings
Timon Barlag, Nicolas Fröhlich, Teemu Hankala, Miika Hannula, Minna Hirvonen, Vivian Holzapfel, Juha Kontinen, Arne Meier, Laura Strieker
TL;DR
The paper investigates the expressivity and computation of first-order logic under semiring semantics, connecting logical definability with semiring-based computation. It introduces generalized computation models over semirings, notably the $\,\mathrm{BSS}_K\,$ machine and the $\,K\-$Turing machine, and develops a framework for interpreting FO formulas with semiring values, including formula inequalities and built-in $K$-relations. It then provides complexity-theoretic characterizations: model checking and evaluation align with generalized BSS-like machines and with the circuit class $\mathrm{FAC}^0_{K}$, culminating in a logical characterization of constant-depth semiring circuits via an extension of ${\mathrm{FO}}$ suitable for commutative, positive semirings. The results pave the way for a unified understanding of semiring provenance in logic, circuits, and complexity, and suggest avenues for uniformity and broader circuit hierarchies in semiring settings.
Abstract
We study the expressivity and computational aspects of first-order logic and its extensions in the semiring semantics developed by Grädel and Tannen. We characterize the complexity of model checking and data complexity of first-order logic both in terms of a generalization of Blum-Shub-Smale machines and arithmetic circuits defined over a semiring. In particular, we give a logical characterization of constant-depth arithmetic circuits by an extension of first-order logic that holds for any semiring that is both commutative and positive.