{"id":"67dd77a2-7d09-464a-9f89-c467c9caffa2","arxiv_id":"2501.16543","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Codd's theorem, the equivalence of relational algebra and relational calculus, is extended to semiring-annotated databases, with a proof that division is not expressible from the five basic operations over bag databases.","lead":"Databases can carry extra numbers on every row, such as multiplicities, probabilities, or costs. This paper proves that two classic query languages, relational algebra and relational calculus, still express exactly the same questions over such annotated databases, provided new operations are added, and shows that one operation, division, cannot be hidden inside the basic algebra for bag databases.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3's proof breaks for 0-ary universal queries: Eψ ÷ Eadom is ill-formed when Eψ is unary, because division requires n1 > n2.","rationale":"The reader's weakest_assumption concerned the zero-sum-free and positive-semiring hypotheses and the non-triviality assumption. Those are genuine scope limitations, but the most load-bearing technical flaw is in the proof of Theorem 3 itself: the universal-quantifier step is not well-formed when the formula being quantified has exactly one free variable, because the proposed RA expression Eψ ÷ Eadom has equal-arity operands and division is undefined for n1 = n2. This is not a matter of an unproved edge case that can be left to the reader; it affects the central equivalence for 0-ary queries, which the theorem explicitly claims. On the bag semiring, the query ∀x R(x) returns the product of annotations, and it is unclear—and possibly impossible—for RA with division as defined to compute that product, since division can only reduce arity by a positive amount and the only 0-ary operation is summing projection. The proof gap is concrete and verifiable from the text: Definition 17 imposes n1 > n2, and the universal case in Theorem 3 assumes n−1 can be 0 without addressing the arity condition. I therefore recommend that the paper be accepted only conditionally, with a corrected or explicitly excluded treatment of 0-ary universal queries. The reader's focus on zero-sum-freeness is reasonable but does not identify this specific breakdown, so my agreement is 'disagree' rather than 'partial' or 'agree'.","tokens_in":35797,"tokens_out":23143,"duration_ms":217752,"concrete_test":"Instantiate Theorem 3 on the bag semiring N with schema (R) where R is unary, and consider the 0-ary query q(I) = ∏_{b∈adom(I)} R(b), which is definable by the RC sentence ∀x R(x). First, verify that the proof's construction Eψ ÷ Eadom is invalid because it requires 1 > 1. Then, on the database with R(a)=2 and R(b)=3, attempt to find an RA expression (built with union, difference, product, projection, selection, support, and division) that evaluates to 6. If a systematic search over small expressions or an invariant argument shows that no such expression exists, then Theorem 3 is false as stated; if one is found, the proof still needs a separate case for n = 1.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"In Theorem 3, direction (3)⇒(1), the universal-quantification case constructs Eϕ as Eψ ÷ Eadom, which has arity n−1. This is well-formed only when the arity of Eψ is strictly greater than 1, since Definition 17 requires the numerator arity n1 to be strictly larger than the denominator arity n2. When n = 1, ψ has exactly one free variable, Eψ is unary, and Eadom is unary, so n1 = n2 = 1 and the division expression is not a valid RA expression. The theorem states that queries may be 0-ary (n ≥ 0), and no separate case is given for sentences produced by universal quantification over the last remaining variable, such as ∀x R(x). On the bag semiring, this sentence evaluates to the product of all annotations in R, a genuine semiring value that is not obviously expressible by the remaining RA operations: division can never produce a 0-ary relation under the strict inequality, and the only 0-ary operation, π_[], sums instead of multiplying. Thus the proof of Theorem 3 has a concrete gap for 0-ary universal queries, and the theorem may be false as stated for such queries over non-idempotent semirings.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":36052,"tokens_out":19717,"duration_ms":178017,"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":[{"comment":"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":"Section 4.3, proof of Theorem 3, direction (3)⇒(1), universal-quantification case"},{"comment":"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.","section":"Section 4.3, proof of Theorem 3, direction (1)⇒(2), division case"}],"minor_comments":[{"comment":"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":"Section 4.1, proof of Theorem 2"},{"comment":"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":"Section 4.3, proof of Theorem 3, direction (3)⇒(1), Case 2"},{"comment":"The displayed equation uses φ_θ where the constructed formula is ∇φ_θ; the proof should consistently write ∇φ_θ, since φ_θ alone need not be Boolean-valued.","section":"Section 3.3, proof of Theorem 1, direction (1)⇒(2), selection case"},{"comment":"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":"Section 3.3, proof of Theorem 1, direction (3)⇒(1), conjunction case"},{"comment":"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":"Section 3.3, proof of Theorem 1, direction (3)⇒(1)"},{"comment":"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).","section":"Section 3.2, Proposition 4, part 3"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid contribution with a narrow but real gap in Theorem 3 for 0-ary universal queries. The natural fix is to allow division with equal arities (n1 = n2) and to check the corresponding equal-arity case in the algebra-to-calculus direction; the same fix also amply justifies the paper's inclusion of 0-ary queries. I would not reject: the main body of the proofs is sound, and Theorem 2 is convincing. The typos and minor omissions listed in the report are straightforward to correct."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Sarah, this one is worth your time, but don't take Theorem 3 at face value. The paper is the first to ask and answer Codd-type expressive-completeness questions for semiring-annotated databases, and the main body is genuinely novel: it adds a support operation and a 'but not' connective, proves two algebra/calculus equivalences, and shows that division is not definable in basic relational algebra over the bag semiring via a clean combinatorial bound. That bag inexpressibility result is the strongest part and, as far as I can tell, correct.\n\nThe soft spots are in the proofs of the two theorems. In Theorem 1, the conjunction case in direction (3)→(1) contains an internally inconsistent description of the witness tuple w; the text says Pθ(w)=1 only for one tuple, but the coordinates don't line up. This looks like a typo rather than a fatal error, but it needs rewriting. The bigger problem is in Theorem 3. The universal-quantification case constructs Eψ ÷ Eadom and says it has arity n−1. That requires arity(Eψ) > arity(Eadom), i.e., n > 1. For n=1, ψ has a single free variable and the formula ∀x ψ is a sentence; Eψ and Eadom are both unary, so the division expression is not well-formed under their Definition 17 (strict inequality). There is no separate case for this. And this isn't a cosmetic gap: on the bag semiring, ∀x R(x) evaluates to the product of the annotations of all tuples in R, which the remaining operations cannot produce — projection sums, and division requires a strict arity drop. So Theorem 3 looks false as stated for 0-ary universal queries over non-idempotent semirings. That is load-bearing.\n\nBeyond that, the paper is careful about the zero-sum-free and positive-semiring assumptions, and Remark 5 correctly explains why zero-sum-freeness is needed for the active domain. The blanket non-triviality assumption is slightly restrictive, but it's stated up front. The inductive proofs are mostly rigorous; the bag inexpressibility proof is convincing.\n\nWho is this for? Database theorists studying provenance and expressive completeness, and anyone interested in semiring semantics of first-order logic. It deserves a serious referee despite the gap — the bag result alone is worth discussing. I'd send it to review with a request to fix the 0-ary universal case and clean up the conjunction step. Whether the theorem survives in full generality is the key question; it may need a restricted statement or an additional operation.","headline":"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.","tokens_in":36573,"tokens_out":5590,"would_cite":true,"duration_ms":50956,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68P15","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["semiring databases","Codd's theorem","relational algebra","relational calculus","monus","support operation","bag semiring","expressive power"],"falsifier":"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.","tokens_in":35606,"feed_emoji":"🗄️","tokens_out":7373,"duration_ms":68875,"temperature":0.7,"pith_summary":"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.","feed_headline":"Codd's theorem now holds for bag and fuzzy databases","feed_subtitle":"Adding monus, support, and division makes algebra and calculus equally expressive over semirings.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Codd's original relational-completeness theorem, the statement this paper extends to semiring semantics.","marker":"[8]"},{"why":"The standard domain-independence formulation of Codd's theorem that serves as the template for the definitions of domain-independent BRC and RC.","marker":"[1]"},{"why":"Introduces the monus operation as the semantics for relational difference on K-relations, adopted throughout the paper.","marker":"[10]"},{"why":"Influential provenance-semiring paper that motivates studying queries over semiring-annotated databases.","marker":"[14]"},{"why":"Provides semiring semantics for first-order logic in negation normal form, the starting point for the BRC and RC semantics.","marker":"[15]"},{"why":"Surveys the alternative ways to define difference on semirings, used to justify the choice of monus.","marker":"[26]"}],"fun_headline_variants":["Codd's theorem extended to semirings with monus and support","Semiring databases: algebra and calculus match with right primitives","Bag databases defy division: inexpressibility result for semirings","Codd's equivalence for semirings hinges on monus, support, and division","For semiring databases, division is not always expressible"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Codd's theorem extended to semirings with monus and support","Semiring databases: algebra and calculus match with right primitives","Bag databases defy division: inexpressibility result for semirings","Codd's equivalence for semirings hinges on monus, support, and division","For semiring databases, division is not always expressible"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000366,"raw_usage":{"total_tokens":1922,"prompt_tokens":850,"completion_tokens":1072,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":466,"completion_tokens_details":{"reasoning_tokens":979}},"tokens_in":466,"tokens_out":1072,"duration_ms":8205,"temperature":1.0,"reasoning_tokens":979,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T12:30:49.968655+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Codd's original relational-completeness theorem, the statement this paper extends to semiring semantics."},{"cited_title":"F oundations of Databases, volume 1","cited_arxiv_id":null,"evidence_quote":"The standard domain-independence formulation of Codd's theorem that serves as the template for the definitions of domain-independent BRC and RC."},{"cited_title":"On database query la nguages for K-relations","cited_arxiv_id":null,"evidence_quote":"Introduces the monus operation as the semantics for relational difference on K-relations, adopted throughout the paper."},{"cited_title":"Green, Grigoris Karvounarakis, and V al Tannen","cited_arxiv_id":null,"evidence_quote":"Influential provenance-semiring paper that motivates studying queries over semiring-annotated databases."},{"cited_title":"Different differences in semirings","cited_arxiv_id":null,"evidence_quote":"Surveys the alternative ways to define difference on semirings, used to justify the choice of monus."}],"review_version":1}