REVIEW 2 major objections 6 minor 29 references
Codd's Theorem for Databases over Semirings
T0 review · 2 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash
Pith's one-line read Relational algebra and relational calculus have the same expressive power on databases over any zero-sum-free semiring with monus and support, and likewise, with division and universal quantification, over positive semirings.
desk verdict First real Codd-theorem result for semiring-annotated databases, with a solid bag-inexpressibility proof, but Theorem 3 has a genuine 0-ary universal-quantifier gap that may make it false as stated. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The proof rides on three interconnected mechanisms. (1) The monus operation — truncated subtraction on the natural numbers, residuated difference on lattices — serves as relational difference, and the new support operation s(a)=1 if a≠0 is added to the algebra; together they allow a single expression, supp(π₁(R)∪π₂(R)), to define the active domain on every zero-sum-free semiring, a step used throughout the algebra-to-calculus translation. (2) The calculus side mirrors these with the binary 'but not' connective, interpreted as monus, and the unary ∇ (it is not false that), interpreted as support. (3) Division is defined as R₁÷R₂(a) = s(Σ_b R₁(a,b)) · ∏_{R₂(b)≠0} R₁(a,b), and the direction from calculus to algebra simulates universal quantification by dividing by the active-domain relation, using an η-sentence built on ∇ and ∃ to control the finite-support condition.
What would settle it
Exhibit a zero-sum-free semiring with monus and support — for instance the fuzzy semiring ([0,1], max, min) — and a query expressible by a domain-independent basic relational calculus formula that is not expressible by any basic relational algebra expression; Theorem 1 predicts that no such query can exist.
Extended reading notes
Core claim
The central claim is that Codd's equivalence holds for semiring-annotated relations provided the right primitives are used. Theorem 1 states that on any zero-sum-free commutative semiring expanded with monus and support, a query is expressible in basic relational algebra if and only if it is definable by a domain-independent basic relational calculus formula using ∧, ∨, the 'but-not' connective, ∇, and ∃. Theorem 3 states that on any positive semiring the equivalence continues to hold when the algebra is given division and the calculus is given universal quantification. The paper also proves Theorem 2: over the bag semiring of natural numbers, relational division cannot be expressed using union, difference, product, selection, projection, and support, in sharp contrast with ordinary relational databases.
Load-bearing premise
The entire equivalence rests on the semiring being zero-sum-free in the first version (no two non-zero elements add to zero) and positive in the second (also no zero divisors); without zero-sum-freeness, the uniform expression for the active domain can fail, and with it the translation.
Editorial extensions
If this is right
- On bag, fuzzy, and Łukasiewicz databases, relational algebra and relational calculus become interchangeable, so optimizers can freely rewrite queries between the procedural and the declarative form.
- Relational division over bags requires a dedicated primitive operator, since no expression built from union, difference, product, selection, projection, and support can compute it.
- The two equivalences supply a new relational-completeness benchmark for query languages over annotated data, in the spirit of the original Boolean benchmark.
- The RC calculus coincides with a fragment of dual intuitionistic logic under Goodman's algebraic semantics, opening a channel between database-expressive-power results and non-classical proof theory.
Reading between the lines
- The zero-sum-free condition is probably necessary, not just sufficient: on rings, where a + (−a) = 0, the paper's own active-domain argument breaks, suggesting the stated theorem cannot extend to rings as written.
- The bag-semiring inexpressibility of division may be the tip of a structural phenomenon: on semirings with a polynomial-bounding size measure, every basic algebra expression has polynomially growing multiplicities, while division can grow exponentially, so a characterization of exactly which semirings can express division (a question the paper asks) should connect to growth-rate arguments.
- A testable extension is to replace monus by the alternative difference operations surveyed in the paper's cited literature and check which of them preserve Codd's theorem; the equivalence established here suggests that only differences admitting a uniformly definable active domain will work.
- For polynomial provenance semirings, the version of Codd's theorem implies that provenance computed by the full algebra can be converted to equivalent logical forms, which may simplify static analysis of query provenance.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. Badia, Kolaitis, and Noguera extend Codd's theorem to databases over semirings. They work with semirings equipped with a monus operation (for difference) and a support operation (to isolate the Boolean skeleton of a relation). Theorem 1 shows that over any zero-sum-free semiring with monus and support, basic relational algebra BRA (union, difference, Cartesian product, selection, projection, support) has the same expressive power as domain-independent basic relational calculus BRC (using conjunction, disjunction, the 'but not' connective, the operator ∇, and existential quantification). Theorem 2 gives a combinatorial proof that division is not expressible in BRA over the bag semiring. Theorem 3 shows that over positive semirings, the algebra RA obtained by adding division to BRA is equivalent to the calculus RC obtained by adding universal quantification to BRC. The proofs are by mutual induction, with the active domain uniformly definable via support and zero-sum-freeness; the division simulation in Theorem 3 uses a sentence η that forces a product over the active domain.
Significance. The paper makes a convincing case for monus and support as the right semantic primitives for a semiring-based Codd theorem, and the bag inexpressibility result (Theorem 2) is a clean and persuasive combinatorial argument. The two equivalence theorems, if fully repaired, would provide a solid foundation for comparing query languages over annotated databases and connect the area to dual intuitionistic logic. The paper is generally well-structured, with careful definitions and mostly rigorous proofs; the active-domain construction (Proposition 3) and the η-sentence trick in Theorem 3 are elegant. The main reservation is the 0-ary universal quantification gap, which is local and fixable but currently leaves Theorem 3 unproven (and, without the fix, false on the bag semiring) for sentence queries.
major comments (2)
- [Section 4.3, proof of Theorem 3, direction (3)⇒(1), universal-quantification case] The construction for ∀y_n ψ takes E_φ = E_ψ ÷ E_adom, which has arity n−1. When n = 1, both E_ψ and E_adom are unary, so Definition 17 requires n1 > n2 and the division expression E_ψ ÷ E_adom is not a well-formed RA expression. Since Theorem 3 is stated for all n ≥ 0 and the paper explicitly allows 0-ary queries (Definition 14, Remark 1), the proof has a concrete gap for sentences such as ∀x R(x). This is not merely a presentational issue: over the bag semiring, the sentence ∀x R(x) evaluates to the product of all multiplicities in R, and the only 0-ary operation in RA, π_[], computes a sum, so no expression built from the allowed operations (with strict-inequality division) can produce this value in general. The fix is to relax Definition 17 to allow n1 ≥ n2, treating the equal-arity case as producing a 0-ary relation, and to re-check the (1)⇒(2) direction accordingly; alternatively, Theorem 3 should be restricted to queries of positive arity.
- [Section 4.3, proof of Theorem 3, direction (1)⇒(2), division case] The formula φ_E constructed for E_1 ÷ E_2 is written under the assumption n1 > n2, using the block of variables y_{n1−n2+1},...,y_{n1} for the existential and universal quantifiers. If Definition 17 is extended to allow n1 = n2, as suggested above, this block becomes empty and φ_E is a sentence; the domain-independence proof (Cases 1–3) must then be re-examined for the empty tuple. The calculations appear to carry over using the same sentence η, but the paper should handle this case explicitly rather than relying on the current strict-inequality notation.
minor comments (6)
- [Section 4.1, proof of Theorem 2] The proof text says 'Let E be an expression of the basic relational calculus BRC', but Theorem 2 is about BRA expressions; this should be 'basic relational algebra BRA'.
- [Section 4.3, proof of Theorem 3, direction (3)⇒(1), Case 2] The text states 'It follows that ∑_{b∈D} E_ψ^I(a,b) = 1' after observing that at least one summand is nonzero; the displayed equality should be '≠ 0', since the sum of nonzero semiring values is not necessarily 1.
- [Section 3.3, proof of Theorem 1, direction (1)⇒(2), selection case] The displayed equation uses φ_θ where the constructed formula is ∇φ_θ; the proof should consistently write ∇φ_θ, since φ_θ alone need not be Boolean-valued.
- [Section 3.3, proof of Theorem 1, direction (3)⇒(1), conjunction case] The explanation of the witness tuple is inconsistent: the text says w = (a1,a2,a3,a4,a2), but the correct tuple satisfying the projection and selection is (a1,a2,a4,a2,a3). The expression E_φ itself is correct, so this is a typo in the proof narrative.
- [Section 3.3, proof of Theorem 1, direction (3)⇒(1)] In the but-not, conjunction, and disjunction cases, the subcases where φ has no free variables are deferred with 'The details are left to the reader.' Since the theorem includes 0-ary queries and the general variable-renaming constructions are not directly applicable to sentences, these degenerate cases should be spelled out (e.g., conjunction of sentences is simply E_ψ × E_χ).
- [Section 3.2, Proposition 4, part 3] The sentence 'By the domain independence of φ, we have that φ^{A(I)} = φ^B' appears twice in the proof; the repetition should be removed, and the proof should explicitly invoke Proposition 2(4).
Circularity Check
No significant circularity: the equivalence proofs are explicit translations between independently defined languages; the only self-citations are background and not load-bearing. A non-circular proof gap exists for 0-ary universal queries.
full rationale
The paper's central claim is an equivalence between two independently defined formalisms. BRA/BRC and RA/RC are given separate syntax and semantics (Definitions 6-12, 17, and Section 4.2), and the proof of Theorems 1 and 3 proceeds by explicit inductive translations. In the division direction, the formula (∇∃yφ1) ∧ (∀y((η ∇ φ2) ∨ (∇φ2 ∧ φ1))) is not assumed to have the division semantics; its value is computed from the semiring operations and shown to equal the product over the support of φ2 of φ1 using monus identities and the support operation. Similarly, the universal-quantifier direction builds Eψ ÷ Eadom and then verifies, via Proposition 3 and Definition 17, that its evaluation equals the product defining ∀. These are genuine derivations rather than definitions of one language in terms of the other. Theorem 2 is an external lower-bound argument on all BRA expressions over the bag semiring and does not depend on the calculus side. The only self-citations are to prior work by one of the authors (Atserias-Kolaitis [5,6]) and they are used as background motivation, not as the justification of the main theorems. One non-circular concern should be flagged: in the proof of Theorem 3, direction (3)⇒(1), the universal case constructs Eψ ÷ Eadom, which has arity n-1, but Definition 17 requires n1 > n2; when n=1 this is unary ÷ unary, which is not a valid RA expression. The paper explicitly says 'The details are left to the reader' for the no-free-variable cases. This is a proof-completeness or correctness issue, not a circularity, so it does not raise the circularity score. Overall, the derivation chain is self-contained and the equivalence is proved rather than assumed.
Assumptions & free parameters
assumptions (6)
- standard math Standard mathematical foundations (set theory, induction).
- domain assumption Blanket assumption: all K-databases are non-trivial (at least one relation has non-empty support).
- domain assumption Blanket assumption: all K-structures considered have finite universe.
- domain assumption The ambient domain D is a fixed denumerable set.
- domain assumption Theorem 1 assumes K is zero-sum-free; Theorem 3 assumes K is positive (commutative, zero-sum-free, no zero divisors).
- domain assumption The difference operation is the monus; negation is the 'but not' connective; these are assumed as the semantics.
invented entities (3)
-
Support operation s
-
Division operation ÷
-
∇ connective ('it is not false that')
Cite this review
Pith. "Pith review of Codd's Theorem for Databases over Semirings." pith.science (2026). https://pith.science/paper/6ZWDXZ4C
@misc{pith2026250116543,
author = {Pith},
title = {Pith review of: Codd's Theorem for Databases over Semirings},
year = {2026},
howpublished = {\url{https://pith.science/paper/6ZWDXZ4C}},
note = {Machine review of arXiv:2501.16543}
}
read the original abstract
Codd's Theorem, a fundamental result of database theory, asserts that relational algebra and relational calculus have the same expressive power on relational databases. We explore Codd's Theorem for databases over semirings and establish two different versions of this result for such databases: the first version involves the five basic operations of relational algebra, while in the second version the division operation is added to the five basic operations of relational algebra. In both versions, the difference operation of relations is given semantics using semirings with monus, while on the side of relational calculus a limited form of negation is used. The reason for considering these two different versions of Codd's theorem is that, unlike the case of ordinary relational databases, the division operation need not be expressible in terms of the five basic operations of relational algebra for databases over an arbitrary positive semiring; in fact, we show that this inexpressibility result holds even for bag databases.
Reference graph
Works this paper leans on
-
[1]
F oundations of Databases, volume 1
Serge Abiteboul, Richard Hull, and Viktor Vianu. F oundations of Databases, volume 1. Addison- Wesley, 1995. 1, 1
work page 1995
-
[2]
Relational databases and Bell’s theor em
Samson Abramsky. Relational databases and Bell’s theor em. In V al Tannen, Limsoon Wong, Leonid Libkin, Wenfei Fan, Wang-Chiew Tan, and Michae l P . Fourman, editors, In Search of Elegance in the Theory and Practice of Computation - Essays Dedicated to Peter Buneman, volume 8000 of Lecture Notes in Computer Science , pages 13–35. Springer, 2013. doi:10.10...
-
[3]
K. Amer. Equationally complete classes of commutative m onoids with monus. Algebra Universalis, 18:129–131, 1984. 2, 2
work page 1984
-
[4]
On the l imitations of provenance for queries with difference
Y ael Amsterdamer, Daniel Deutch, and V al Tannen. On the l imitations of provenance for queries with difference. In Peter Buneman and Juliana Freire, editors, 3rd Workshop on the Theory and Practice of Provenance, TaPP’11, Heraklion, Crete, Greece, June 20-21, 2011. USENIX Association, 2011. URL: https://www.usenix.org/conference/tapp11/limitations-prove...
work page 2011
-
[5]
Albert Atserias and Phokion G. Kolaitis. Acyclicity, co nsistency, and positive semirings. In Alessandra Palmigiano and Mehrnoosh Sadrzadeh, editors, Samson Abramsky on Logic and Structure in Computer Science and Beyond , volume 25 of Outstanding Contributions to Logic , pages 623–668. Springer,
-
[6]
Albert Atserias and Phokion G. Kolaitis. Consistency of relations over monoids. Proceedings of the ACM on Management of Data , 2(2):107, 2024. doi:10.1145/3651608. 1
- [7]
-
[8]
Edgar F. Codd. Relational completeness of data base subl anguages. In R. Rustin, editor, Proceedings of 6th Courant Computer Science Symposium (May 24–25, 1971: New York, N.Y.) , pages 65–98. Prentice-Hall, 1972. 1, 1
work page 1971
Show all 29 references
-
[9]
Dannert, Erich Gr¨ adel, Matthias Naaf, and V al Tannen
Katrin M. Dannert, Erich Gr¨ adel, Matthias Naaf, and V al Tannen. Semiring provenance for fixed-point logic. In Christel Baier and Jean Goubault-Larr ecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25- 28, 2021, Ljubljana, Slove- nia (Vi...
2021 doi
-
[10]
On database query la nguages for K-relations
Floris Geerts and Antonella Poggi. On database query la nguages for K-relations. Journal of Applied Logic, 8(2):173–185, 2010. 1, 2, 6 31
2010
-
[11]
Allen V an Gelder and Rodney W. Topor. Safety and transla tion of relational calculus queries. ACM Transactions on Database Systems , 16(2):235–278, 1991. doi:10.1145/114325.103712. 1
1991
-
[12]
Nicolas D. Goodman. The logic of contradiction. Mathematical Logic Quarterly, 27(8–10):119–126,
-
[13]
Todd J. Green. Containment of conjunctive queries on an notated relations. Theory of Computing Systems, 49:429–459, 2011. 1
2011
-
[14]
Green, Grigoris Karvounarakis, and V al Tannen
Todd J. Green, Grigoris Karvounarakis, and V al Tannen. Provenance semirings. In PODS 2007 Pro- ceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART sym posium on Principles of Database Systems, pages 31–40. ACM Press, 2007. 1
2007
-
[15]
Semiring provenance for fi rst-order model checking
Erich Gr¨ adel and V al Tannen. Semiring provenance for fi rst-order model checking. Available at https://arxiv.org/abs/1712.01980, 2017. 1, 6
2017 arXiv
-
[16]
Provenance analysis and s emiring semantics for first-order logic
Erich Gr¨ adel and V al Tannen. Provenance analysis and s emiring semantics for first-order logic. To appear in a volume in honor of J´ anos Makowsky, published by Birkh¨ auser, 2024.1
2024
-
[17]
Hajdinjak and A
M. Hajdinjak and A. Bauer. K-relations and beyond. In C. R. Guti´ errez, editor,Advances in Knowl- edgeRepresentation, pages 19–40. InTech, 2012. 5
2012
-
[18]
Die formalen regeln der intuitionistis chen logik
Arend Heyting. Die formalen regeln der intuitionistis chen logik. Sitzungsbericht PreuBische Akademie der Wissenschaften Berlin, physikalisch-mathematische K lasse II, pages 42–56, 1930. 4.2
1930
-
[19]
Ngo, Reinhard Pichler, Dan S uciu, and Yisu Remy Wang
Mahmoud Abo Khamis, Hung Q. Ngo, Reinhard Pichler, Dan S uciu, and Yisu Remy Wang. Convergence of Datalog over (pre-) semirings. Journal of the ACM , 71(2):8:1–8:55, 2024. doi:10.1145/3643027. 1
2024 doi
-
[20]
Kostylev, Juan L
Egor V . Kostylev, Juan L. Reutter, and Andr´ as Z. Salamon. Classification of annotation semirings over containment of conjunctive queries. ACM Transactions of Database Systems , 39(1):1:1–1:39, 2014. doi:10.1145/2556524. 1
2014 doi
-
[21]
McKinsey
J.C.C. McKinsey. Proof of the independence of the primi tive symbols of Heyting’s calculus of propo- sitions. Journal of Symbolic Logic , 4(4):155–158, 1939. 4
1939
-
[22]
McKinsey and Alfred Tarski
J.C.C. McKinsey and Alfred Tarski. On closed elements i n closure algebras. Annals of Mathematics , 47(2):122–162, 1946. 1, 3
1946
-
[23]
Example of a naturally ordered semiring which is not an m-semiring
Mika¨ el Monet. Example of a naturally ordered semiring which is not an m-semiring. https://math.stackexchange.com/questions/1966858/example-of-a-naturally-ordered-semiring-which- is-not-an-m-semiring, 2016. StackExchange. 2
2016
-
[24]
Semi-Boolean algebras and their appl ications to intuitionistic logic with dual operations
Cecylia Rauszer. Semi-Boolean algebras and their appl ications to intuitionistic logic with dual operations. Fundamenta Mathematicae , 83(3):219–249, 1974. URL: http://eudml.org/doc/214696. 1
1974
-
[25]
The independence of connectives
Timothy Smiley. The independence of connectives. Journal of Symbolic Logic , 40(2):250–251, 1975. doi:10.2307/2271931. 4 32
1975 doi
-
[26]
Different differences in semirings
Dan Suciu. Different differences in semirings. In Anto ine Amarilli and Alin Deutsch, editors, The Provenance of Elegance in Computation - Essays Dedicate d to V al Tan- nen, Tannen’s Festschrift, May 24-25, 2024, University of P ennsylvania, Philadelphia, PA, USA , volume 119...
2024 doi
-
[27]
A naturally ordered semiring that cannot be e xpanded to a semiring with monus, 2025
Dan Suciu. A naturally ordered semiring that cannot be e xpanded to a semiring with monus, 2025. Private Communication. 2
2025
-
[28]
Jeffrey D. Ullman. Principles of Database Systems, 1st Edition . Computer Science Press, 1980. 4.1
1980
-
[29]
Evaluating datalog over semirings: A grounding-based approach
Hangdong Zhao, Shaleen Deep, Paraschos Koutris, Sudee pa Roy, and V al Tannen. Evaluating datalog over semirings: A grounding-based approach. Proceedings of the ACM on Management of Data , 2(2):90, 2024. doi:10.1145/3651591. 1 33
2024 doi
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.