pith. sign in

arxiv: 2507.18375 · v2 · submitted 2025-07-24 · 💻 cs.CC · cs.LO

Fagin's Theorem for Semiring Turing Machines

Guillermo Badia , Manfred Droste , Thomas Eiter , Rafael Kiesel , Carles Noguera , Erik Paul This is my paper

Pith reviewed 2026-05-19 03:17 UTC · model grok-4.3

classification 💻 cs.CC cs.LO
keywords Fagin's theoremsemiring Turing machinesweighted logicexistential second-order logicquantitative complexitycommutative semiringsNP_infinity(R)
0
0 comments X

The pith

A refined semiring Turing machine model equates weighted existential second-order logic with non-deterministic polynomial time over commutative semirings.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper establishes an equivalence between a quantitative complexity class and a form of logic. Specifically, it shows that problems solvable in non-deterministic polynomial time by improved semiring Turing machines over a commutative semiring R correspond exactly to properties expressible in weighted existential second-order logic with semiring-annotated predicates. A reader would care because this provides a logical way to describe and analyze weighted computations that arise in optimization and AI reasoning, extending the classical Fagin theorem to semiring settings. The work also argues for the superiority of the new machine model and recovers prior results.

Core claim

We introduce an improved SRTM model that enables proving a Fagin theorem: the class NP_∞(R) of non-deterministic polynomial-time computable functions in this model over commutative semiring R is captured by weighted existential second-order logic where predicates are interpreted as semiring-annotated relations over R. The model reclaims important results from earlier work that were flawed in the original SRTM model.

What carries the argument

Improved semiring Turing machine (SRTM) model, which uses semiring-weighted transitions and allows the proof of equivalence to weighted ESO logic by providing the necessary computational properties.

If this is right

  • The new model restores previously flawed results on the complexity of semiring reasoning frameworks.
  • Weighted existential second-order logic now serves as a precise logical counterpart to NP_∞(R) computations.
  • Logical methods can be applied to study the expressiveness of quantitative polynomial-time problems over semirings.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This characterization might help in developing decision procedures for weighted problems by leveraging logical tools.
  • Similar extensions could be attempted for other machine models or complexity classes in quantitative computing.
  • Practical semiring applications in AI could benefit from this dual view of machines and logic for verification or synthesis.

Load-bearing premise

The modifications to the original semiring Turing machine model are necessary and sufficient to enable the machine-logic equivalence without altering the underlying computational power.

What would settle it

A concrete computation problem that can be decided by an improved SRTM in non-deterministic polynomial time over a commutative semiring but cannot be expressed by any formula in the weighted existential second-order logic would falsify the theorem.

read the original abstract

In recent years, quantitative complexity over semirings has been intensively investigated. In this context, Eiter and Kiesel (Semiring Reasoning Frameworks in AI and Their Computational Complexity, J. Artif. Intell. Res., 2023) introduced non-deterministic Turing Machines with semiring-weighted transitions (SRTMs) to capture the complexity of a manifold of semiring frameworks. Beyond computational complexity, they posed the question of how we can relate the computational power of SRTMs to logical expressiveness. While this question was partially addressed for a more limited machine model by Badia et al.\ (Logical characterizations of weighted complexity classes, MFCS, 2024), the full question remained open. To answer it, we present an improved version of Eiter and Kiesel's SRTM model of computation. First and foremost, this enables us to prove a Fagin Theorem for the SRTM model, i.e., we show that the quantitative complexity class $\text{NP}_\infty(R)$, which comprises non-deterministic polynomial time computability in the improved SRTM model over a commutative semiring $R$, is captured by a version of weighted existential second-order logic that allows for predicates interpreted as semiring-annotated relations over $R$. Furthermore, we argue that the new SRTM model is preferable over the original one and show that it reclaims some important results from Eiter and Kiesel (2023) that were flawed with respect to the latter.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces an improved model of Semiring Turing Machines (SRTMs) and proves a Fagin theorem establishing that the quantitative complexity class NP_∞(R) — non-deterministic polynomial-time computation over a commutative semiring R in the improved model — is captured by a weighted existential second-order logic in which predicates are interpreted as semiring-annotated relations. The authors additionally argue that the improved SRTM is preferable to the original model of Eiter and Kiesel and that it reclaims certain results from that prior work.

Significance. If the central equivalence holds and the model improvements preserve the intended computational power, the result supplies a logical characterization for semiring-weighted complexity classes, directly addressing the open question left by Eiter and Kiesel. This extends classical descriptive complexity results to the quantitative setting and could support new techniques for analyzing semiring reasoning frameworks in AI. The reclamation of prior results is a secondary strength, provided the model changes are shown not to alter the class NP_∞(R).

major comments (2)
  1. [§3] §3 (Improved SRTM definition): The central claim that NP_∞(R) in the improved model equals the weighted ESO logic rests on the improvements neither increasing nor decreasing the non-deterministic polynomial-time power relative to the original SRTM. No explicit simulation or power-equivalence argument between the two machine models is referenced in the provided sections; without it, it is unclear whether the logic characterizes the class the authors originally set out to capture.
  2. [§5.2] §5.2 (Logic-to-machine direction): The construction that turns a weighted ESO sentence into an improved SRTM must preserve the exact semiring weights and the polynomial time bound. The current sketch does not detail how the semiring-annotated relations are encoded into transition weights without introducing additional factors or changing the acceptance condition; this step is load-bearing for the claimed equivalence.
minor comments (2)
  1. [§4] The notation for semiring multiplication and addition in the weighted logic definitions should be made uniform with the machine transition weights to avoid reader confusion.
  2. A short table comparing the original SRTM, the improved SRTM, and the logic would help readers track which features were added or removed.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for highlighting these points about the model comparison and proof details. We address each major comment below.

read point-by-point responses

  1. Referee: [§3] §3 (Improved SRTM definition): The central claim that NP_∞(R) in the improved model equals the weighted ESO logic rests on the improvements neither increasing nor decreasing the non-deterministic polynomial-time power relative to the original SRTM. No explicit simulation or power-equivalence argument between the two machine models is referenced in the provided sections; without it, it is unclear whether the logic characterizes the class the authors originally set out to capture.

    Authors: We agree that the manuscript would benefit from an explicit argument showing that the improved SRTM model preserves the same NP_∞(R) class as the original model of Eiter and Kiesel. In the revised version we will add a dedicated subsection to §3 containing mutual simulation arguments: one direction shows how any original SRTM computation can be simulated by an improved SRTM without changing the polynomial time bound or the semiring value, and the converse direction shows the reverse simulation. This will establish that the two models define identical classes and therefore that the logic characterizes the intended quantitative complexity class. revision: yes

  2. Referee: [§5.2] §5.2 (Logic-to-machine direction): The construction that turns a weighted ESO sentence into an improved SRTM must preserve the exact semiring weights and the polynomial time bound. The current sketch does not detail how the semiring-annotated relations are encoded into transition weights without introducing additional factors or changing the acceptance condition; this step is load-bearing for the claimed equivalence.

    Authors: We accept that the current sketch in §5.2 is insufficiently detailed for the encoding step. In the revision we will expand the construction to explicitly describe the encoding of each semiring-annotated predicate into a finite set of weighted transitions. The description will include the precise weight assignment rules that ensure the product of transition weights along accepting paths equals the semiring value of the formula, with no extraneous multiplicative constants, and will verify that the nondeterministic acceptance condition matches the existential quantification in the logic while remaining within polynomial time. revision: yes

Circularity Check

0 steps flagged

Direct equivalence proof between independently defined machine and logic classes

full rationale

The paper defines an improved SRTM model and proves that its NP_∞(R) class equals a weighted ESO logic with semiring-annotated relations. This is presented as a new characterization enabled by the model changes, with separate arguments that the new model reclaims prior results and is preferable. No equations or definitions reduce the claimed equivalence to a fit, self-definition, or load-bearing self-citation chain; the central derivation is a direct proof rather than a renaming or imported uniqueness result. Self-citations to overlapping prior work (Eiter-Kiesel 2023 and Badia et al. 2024) supply context but are not invoked to justify the new equivalence itself.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the definition of the improved SRTM model and the precise syntax and semantics of the weighted existential second-order logic; both are introduced or modified within the paper rather than taken from prior independent sources.

axioms (1)
  • domain assumption The semiring R is commutative
    Explicitly required in the abstract for the NP_∞(R) class and the logic equivalence to hold.

pith-pipeline@v0.9.0 · 5807 in / 1442 out tokens · 48823 ms · 2026-05-19T03:17:20.133025+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [1]

    7.¬Ti,j,k⊕Ti,j,k⊗¬Ti,j′,k+1⊕Ti,j,k⊗Ti,j′,k+1⊗Hi,k Variable ranges:−p(n)≤i≤p(n),j≠j′∈Σ,0≤k<p(n) Tape remains unchanged unless written

    ⊕j∈ΣTi,j,k Variable ranges:−p(n)≤i≤p(n),0≤k≤p(n) There is at least one symbol per tape cell. 7.¬Ti,j,k⊕Ti,j,k⊗¬Ti,j′,k+1⊕Ti,j,k⊗Ti,j′,k+1⊗Hi,k Variable ranges:−p(n)≤i≤p(n),j≠j′∈Σ,0≤k<p(n) Tape remains unchanged unless written. 8.¬Qq,k⊕Qq,k⊗¬Qq′,k Variable ranges:q≠q′∈Q,0≤k≤p(n) There is at most one state at a time. 9.¬Hi,k⊕Hi,k⊗¬Hi′,k Variable ranges:i≠i′...

    work page

  2. [2]

    there exist q′,σ′,d,r s.t

    ¬Hi,k⊕Hi,k⊗¬Qq,k⊕Hi,k⊗Qq,k⊗¬Ti,σ,k⊕ Hi,k⊗Qq,k⊗Ti,σ,k⊗Σ((q,σ),(q′,σ′),d,r)∈δHi+d,k+1⊗Qq′,k+1⊗Ti,σ′,k+1⊗surrr Variable ranges:−p(n)≤i≤p(n),0≤k<p(n) andq∈Q,σ∈Σs.t. there exist q′,σ′,d,r s.t. ((q,σ),(q′,σ′),d,r)∈δ. Possible weighted transitions with a fixed weight at computation stepk when head is at positioni

    work page

  3. [3]

    there exist q′,σ′,d s.t

    ¬Hi,k⊕Hi,k⊗¬Qq,k⊕Hi,k⊗Qq,k⊗¬Ti,σ,k⊕ Hi,k⊗Qq,k⊗Ti,σ,k⊗Σ((q,σ),(q′,σ′),d,X)∈δHi+d,k+1⊗Qq′,k+1⊗Ti,σ′,k+1⊗surrith Variable ranges: −p(n)≤i≤p(n),0≤k<p(n) andq∈Q,σ∈Σs.t. there exist q′,σ′,d s.t. ((q,σ),(q′,σ′),d,X)∈δ. Possible weighted transitions with weight from the tape at computation stepk when head is at positioni

    work page

  4. [4]

    there do not existq′,σ′,d,r s.t.((q,σ),(q′,σ′),d,r)∈δ

    ¬Hi,k⊕Hi,k⊗¬Qq,k⊕Hi,k⊗Qq,k⊗¬Ti,σ,k ⊕Hi,k⊗Qq,k⊗Ti,σ,k⊗Hi,k+1⊗Qq,k+1⊗Ti,σ,k+1 Variable ranges:−p(n)≤i≤p(n),0≤k<p(n) andq∈Q,σ∈Σs.t. there do not existq′,σ′,d,r s.t.((q,σ),(q′,σ′),d,r)∈δ. The machine computation has ended. This is included so that when the machine has reached a final state it stays the same untilkreachesp(n). XX:30 REFERENCES In order to prov...

    work page

  5. [5]

    For each interpretation I of the variablesTi,j,k,Hi,k,Qq,k for−p(n)≤i≤p(n),0≤k<p(n) and q∈Q such that I does not correspond to a computation path of M on x, it holds that JαKR(I)=e ⊕

    work page

  6. [6]

    r (πn(π)−1) →c π n(π)it holds that JαKR(I)= ⊕ π′,s.t.cπ i =cπ′ i r(π′ 1)⊗...⊗r(π′ n(π′)−1)

    For each interpretation I of the variablesTi,j,k,Hi,k,Qq,k for−p(n)≤i≤p(n),0≤k<p(n) andq∈Q such that I corresponds to a computation path πofM onx along configurations cπ 1 r(π1) →... r (πn(π)−1) →c π n(π)it holds that JαKR(I)= ⊕ π′,s.t.cπ i =cπ′ i r(π′ 1)⊗...⊗r(π′ n(π′)−1). If both claims hold, then it follows that J⊕T ⊕H ⊕QαKR(∅)is equal to the sum of Jα...

    work page

  7. [7]

    enforce their given purpose. For 1. to 4. this is clear: In order for JαKR(I) to be unequal to e⊕, the variables need to be included in the interpretation

    work page

  8. [8]

    together ensure that at each time step there is exactly one symbol in each tape cell

    and 6. together ensure that at each time step there is exactly one symbol in each tape cell. So assume thatTi,j,k andTi,j′,k are inI. Then J¬Ti,j,k⊕Ti,j,k⊗¬Ti,j′,kKR(I)=e ⊕⊕e⊕=e ⊕, and so JαKR(I)=e ⊕. Assume alternatively that there arei,k such that for noj the variableTi,j,k is inI. Then J⊕ j∈Σ Ti,j,kKR(I)=e ⊕

    work page

  9. [9]

    So assume that Hi,k is not in I butTi,j,k andTi,j′,k forj≠j ′are inI

    ensures that the tape remains unchanged unless written, i.e., unless the head is at positioni at stepk the value of the tape celli stays the same. So assume that Hi,k is not in I butTi,j,k andTi,j′,k forj≠j ′are inI. Then J¬Ti,j,k⊕Ti,j,k⊗¬Ti,j′,k+1⊕Ti,j,k⊗Ti,j′,k+1⊗Hi,kKR(I)=e ⊕⊕(e⊗⊗e⊕)⊕(e⊗⊗e⊗⊗e⊕)=e ⊕

    work page

  10. [10]

    ensures that there is at most one state at a time by analogous reasoning to 5

    work page

  11. [11]

    ensures that there is at most one head position at a time by analogous reasoning to 5

    work page

  12. [12]

    and 11. model the possible transitions at computation step k when the head is at position i including their respective weightsif there is such a transitionfor the given state and tape cell entry. Note for this that the formulas are the same except for the weight, expressed by the surrogate Otherwise, this subformula is not added but the one in 12. is. So ...

    work page

  13. [13]

    Otherwise, this subformula is not added but one in 10

    models that if at computation step k when the head is at position i there is no possible transitionfor the given state q and tape cell entry σ, then the head position, state and tape cell entries stay the same. Otherwise, this subformula is not added but one in 10. is. So assume that Hi,k,Qq,k,Ti,σ,k∈I. Then the value of the subformula is J¬Hi,k⊕Hi,k⊗¬Qq,...

    work page