Pith. sign in

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 →

arxiv 2501.16543 v2 pith:6ZWDXZ4C submitted 2025-01-27 cs.LO

classification cs.LO MSC 68P1503B70
keywords semiringdatabasesCodd'stheoremrelationalalgebracalculusmonussupportoperationbagexpressivepower
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper generalizes Codd's theorem, the classic equivalence between relational algebra and relational calculus, from ordinary Boolean databases to databases whose tuples are annotated with values from an arbitrary semiring. The authors prove two versions of the equivalence. Over every zero-sum-free semiring with monus and support, basic relational algebra (union, difference, Cartesian product, selection, projection, support) has exactly the expressive power of domain-independent basic relational calculus built with conjunction, disjunction, 'but not', the support operator ∇, and existential quantification. Over every positive semiring, the same holds when the algebra is expanded with a division operation and the calculus with universal quantification. A separate theorem shows that, unlike the Boolean case, division is not expressible from the five basic algebra operations on bag databases, which is why the second version is needed. If these results are correct, the procedural-versus-declarative equivalence at the heart of database theory carries over to bag, fuzzy, and other weighted database models.

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.

Watch

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

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

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)
  1. [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.
  2. [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)
  1. [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'.
  2. [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.
  3. [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.
  4. [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.
  5. [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_χ).
  6. [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

0 steps flagged · score 1.0 of 10

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 0 free parameters · 6 assumptions · 3 invented entities

The paper rests on standard mathematics plus domain assumptions about non-triviality, finiteness, and the class of semirings (zero-sum-free for Theorem 1, positive for Theorem 3). It introduces support, ∇, and division as new operations or connectives, justified by necessity results within the paper, but without external empirical handles.

assumptions (6)
  • standard math Standard mathematical foundations (set theory, induction).
    All proofs are ordinary mathematical proofs; no formal system is used.
  • domain assumption Blanket assumption: all K-databases are non-trivial (at least one relation has non-empty support).
    Definition 8; used to ensure active domain is non-empty, which is needed for the η sentence and the universal quantifier case (Theorem 3). Empty databases are excluded from the scope.
  • domain assumption Blanket assumption: all K-structures considered have finite universe.
    Definition 10; required for the finite-sum and finite-product semantics of ∃ and ∀. Infinite universes would require additional closure properties.
  • domain assumption The ambient domain D is a fixed denumerable set.
    Definition 5; standard in database theory.
  • domain assumption Theorem 1 assumes K is zero-sum-free; Theorem 3 assumes K is positive (commutative, zero-sum-free, no zero divisors).
    Sections 3.3 and 4.2; used in Proposition 3 (active domain) and the η sentence. Remark 5 shows zero-sum-freeness is necessary for the given active-domain construction.
  • domain assumption The difference operation is the monus; negation is the 'but not' connective; these are assumed as the semantics.
    Sections 2 and 3; a modeling choice defended in the introduction. The theorem is conditional on this choice; other difference operations may not yield the equivalence.
invented entities (3)
  • Support operation s
    purpose: Unary operation returning 1 for nonzero annotations and 0 otherwise; used in BRA to define active domain and in BRC via ∇.
    Introduced in Definition 3. The paper proves (Remark 2) that support is not expressible using the other five operations on the fuzzy semiring, so it is a necessary addition, but this evidence is internal, not an external falsifiable handle.
  • Division operation ÷
    purpose: Binary operation that generalizes relational division to semiring-annotated relations; added to BRA to obtain RA and to restore equivalence with the calculus fragment with universal quantification.
    Introduced in Definition 17. The paper proves (Theorem 2) that division is not expressible in BRA over the bag semiring, which motivates adding it, but again the evidence is internal.
  • ∇ connective ('it is not false that')
    purpose: Unary connective in BRC/RC corresponding to support; allows formulas to test whether a subformula value is nonzero.
    Introduced in Definition 9. It is the calculus counterpart of the support operation.

how reviews work

0 comments
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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 25 canonical work pages

  1. [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

  2. [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. [3]

    K. Amer. Equationally complete classes of commutative m onoids with monus. Algebra Universalis, 18:129–131, 1984. 2, 2

  4. [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...

  5. [5]

    Kolaitis

    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. [6]

    Kolaitis

    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. [7]

    Edgar F. Codd. A relational model of data for large shared data banks. Communications of the ACM , 13(6):377–387, 1970. doi:10.1145/362384.362685. 2

  8. [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

Show all 29 references
  1. [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...

  2. [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

  3. [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

  4. [12]

    Nicolas D. Goodman. The logic of contradiction. Mathematical Logic Quarterly, 27(8–10):119–126,

  5. [13]

    Todd J. Green. Containment of conjunctive queries on an notated relations. Theory of Computing Systems, 49:429–459, 2011. 1

  6. [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

  7. [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

  8. [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

  9. [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

  10. [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

  11. [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

  12. [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

  13. [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

  14. [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

  15. [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

  16. [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

  17. [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

  18. [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...

  19. [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

  20. [28]

    Jeffrey D. Ullman. Principles of Database Systems, 1st Edition . Computer Science Press, 1980. 4.1

  21. [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

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.