{"id":"fc7e2bdc-5ccf-417e-b7b9-33df0346906f","arxiv_id":"2505.08633","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"D-Hammer automates equational reasoning in labelled Dirac notation using a dependently typed language and a normalization algorithm, and it runs faster than DiracDec on plain Dirac examples.","lead":"The paper introduces D-Hammer, a C++ tool that automatically proves equalities in labelled Dirac notation, the standard notation for describing quantum states on multiple subsystems and for assertions in quantum program logics. It aims to replace long, error-prone pen-and-paper calculations, and it reports large speedups over the earlier DiracDec tool on plain Dirac notation benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Normalizer's sort-then-swap can map AC/SUM-SWAP-equivalent terms to different normal forms when =B-equal summands tie; a concrete two-term example shows false negatives are possible.","rationale":"The reader's weakest assumption identified the normalization algorithm's confluence/uniqueness as the main risk; my concrete two-term example supports that concern and shows it is not merely a missing proof but a likely failure of the algorithm as written. The example does not attack Theorem 1's soundness or Theorem 2's semantic iff, and the paper explicitly disclaims completeness in Section 7, so the correct verdict remains CONDITIONAL rather than REJECT. The condition should be: supply a precise tie-breaking rule for =B-equal terms, prove confluence of the sort/swap/de Bruijn pipeline, or generate certificates. The evaluation still demonstrates meaningful performance on the selected benchmarks, and the label-elimination theorem is a genuine contribution; those parts deserve credit. Since the reader already assigned CONDITIONAL on essentially this basis, my read does not change the verdict, but it sharpens the required condition with a concrete falsifiable test.","tokens_in":37015,"tokens_out":16526,"duration_ms":169780,"concrete_test":"Run D-Hammer's CheckEq on X and Y from the attack, with context T:Index, A,B:O(T,T), and s1=s2=U(T). If the tool reports 'not equal', or prints different normal forms, the normalization is not confluent modulo AC plus SUM-SWAP. If it reports equal, inspect the implementation to see whether an undocumented tie-breaking rule (e.g., comparing de Bruijn forms) is used; such a rule is absent from the paper's Definition 13 and must be stated and proven.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The weakest load-bearing point is the confluence/uniqueness of the normalization described in Section 3.4 and Appendix E. Definition 13 sorts arguments by <B, but terms that are =B-equal are tied; the paper gives no tie-breaking rule, and a stable sort preserves the original order of such summands. This matters because =B-equal summands can become syntactically different after de Bruijn conversion, since bound variables occupy different argument positions. Concretely, let s1,s2 be sets and A,B operator variables, and define X = Σ_{i∈s1} Σ_{j∈s2} ( (⟨i|A|j⟩×⟨j|B|i⟩) + (⟨j|A|i⟩×⟨i|B|j⟩) ) and Y = Σ_{j∈s2} Σ_{i∈s1} ( (⟨j|A|i⟩×⟨i|B|j⟩) + (⟨i|A|j⟩×⟨j|B|i⟩) ). X and Y are semantically equal: swap the two summations in Y and use commutativity of +. After Step 4 sorting without bound variables, both bodies consist of two =B-equal summands. With a stable sort, X keeps i before j in the first summand, while Y keeps j before i; Step 5 then orders the summations as Σ_{s1}Σ_{s2} for X but Σ_{s2}Σ_{s1} for Y. After de Bruijn conversion the bodies coincide, but the nesting order of the sums differs. Thus the two normal forms are syntactically different even though the original terms are semantically equal. The paper's assertion that the transformations yield a unique normal form for AC plus SUM-SWAP is therefore unsupported and, as described, false. This directly weakens the central capability claim: CheckEq can return 'not equal' on valid equations.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents D-Hammer, a C++ implementation of an equational prover for plain and labelled Dirac notation. The formal language is a higher-order, dependently typed calculus with AC symbols of indefinite arity, and expressions are interpreted as linear maps between Hilbert spaces over finite index sets. The paper states a soundness theorem (Theorem 1) for the equational axioms and a label-elimination theorem (Theorem 2) that reduces equality of labelled expressions to equality of plain expressions. Normalization consists of rewriting rules and three specialized steps: sorting modulo AC while ignoring bound variables, reordering nested summations, and de Bruijn conversion. The implementation is evaluated on 18 textbook examples, 158 CoqQ examples, six labelled-Dirac examples, and six small quantum-circuit equivalences, with a claimed speedup over DiracDec on the CoqQ subset.","tokens_in":37381,"tokens_out":10943,"duration_ms":109571,"significance":"If the completeness claims were established, this would be a useful contribution: labelled Dirac notation is central to several quantum Hoare logics, and automated equality checking would relieve a real bottleneck. The paper's strengths include a typed formalization with a denotational semantics, a proof sketch of Theorem 1, a detailed soundness argument for the label-elimination rules in Appendix D.1, external benchmarks with no fitted parameters, and an open-source implementation. The weakness is that the normalizer's confluence and uniqueness, which would make CheckEq complete, are asserted rather than proven, and the tie-breaking issue in Section E can produce false negatives.","major_comments":[{"comment":"The claimed uniqueness of the normal form modulo AC plus SUM-SWAP is unsupported and, as stated, false. Definition 12 treats all bound variables as equal under =B, and Algorithm 1 in Definition 13 sorts arguments by <B without specifying how ties between =B-equal arguments are broken; a stable sort preserves their original order. Let X = sum_{i in s1} sum_{j in s2} ((<i|A|j> * <j|B|i>) + (<j|A|i> * <i|B|j>)) and Y = sum_{j in s2} sum_{i in s1} ((<j|A|i> * <i|B|j>) + (<i|A|j> * <j|B|i>)). These are semantically equal by one application of SUM-SWAP and commutativity of +. After Step 4, both sum bodies contain two =B-equal summands; a stable sort leaves X with the i-first summand first and Y with the j-first summand first. Step 5 then orders the two summations by first occurrence of bound variables, producing different nestings (sum_{s1} sum_{s2} versus sum_{s2} sum_{s1}), and after de Bruijn conversion the additive terms remain in opposite order. The two normal forms are syntactically different, so CheckEq can report 'not equal' for a valid equation. This directly undermines the paper's assertion in Section 3.4 that the normalization is full rather than partial.","section":"Section 3.4 / Appendix E (Definitions 12–14)"},{"comment":"The correctness of the normalization algorithm is load-bearing but is never proved. The text asserts that Steps 4–6 'fully normalize' terms on R union E and that the transformations yield a unique normal form, but Section E contains only definitions and worked examples: there is no termination proof for the sort/swap transformations, no confluence proof for their interaction, and no argument that the final de Bruijn form is independent of the order in which Steps 4 and 5 are applied. Because CheckEq decides equality by comparing normal forms, this missing proof is exactly what would justify the tool's completeness. The soundness of 'equal' answers is not affected, since same normal form plus sound rewrites implies semantic equality, but the capability claim of providing automated equational proof requires completeness. The authors should either supply a rigorous proof for the exact algorithm, including a deterministic tie-breaking rule, or explicitly present D-Hammer as a sound but possibly incomplete normalizer.","section":"Section 3.4 and Section E"}],"minor_comments":[{"comment":"Typo: 'cannot alwasy' should be 'cannot always'.","section":"Section 3.4, Step 4"},{"comment":"The column header 'expressable' should be 'expressible', and the CoqQ paragraph should explicitly state that the comparison is on the 158 examples expressible in D-Hammer; the remaining four DiracDec-expressible examples are not ported, so the headline speedup is on a restricted set.","section":"Table in Section 6"},{"comment":"The proof repeatedly refers to 'the form of Eqn. (1)' when the displayed normal form it establishes is Eqn. (2) of Section 4.2; the cross-reference should be corrected.","section":"Appendix D.1"},{"comment":"The footnote pointing out a naming typo in Table 21 should be resolved by renaming the rule in the table, not by annotating the proof.","section":"Appendix D.1, footnote 5"},{"comment":"The pseudocode line 'ls := ls sorted by <B' should specify the sorting algorithm's tie-breaking behavior (e.g., stable sort or a total order on de Bruijn forms); the implementation's behavior is currently under-specified.","section":"Definition 13"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid tool paper with an honest evaluation and a real application, but the normalizer completeness gap is central. My recommended action is major revision: add a correct confluence/uniqueness proof for the exact algorithm, or weaken the claims and add a proof-of-correctness mechanism for reported equalities (e.g., certificates). The counterexample in Major Comment 1 is small and I believe fixable within the paper's scope, so I do not recommend rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"D-Hammer is the first automated prover for labelled Dirac notation, and that is not a small thing. The language design is thoughtful: dependent types, higher-order functions, AC symbols with indefinite arity, and a generic composition that unifies kets, bras, and operators. Theorem 1 (soundness of the equational theory) is standard but solid. Theorem 2 (label elimination) is a genuinely new reduction from labelled to plain Dirac notation, and the proof idea via rewriting to a normal form is credible. The implementation is open source and the evaluation is honest: they benchmark against their own DiracDec on CoqQ, show 2-40x speedups, and also report that D-Hammer is much slower than specialized circuit-checking tools on the circuit benchmark. That kind of candor is welcome.\n\nThe weak point is the normalization algorithm. Appendix E asserts that the sort-then-swap transformations yield a unique normal form for terms under AC plus SUM-SWAP, but no termination or confluence proof is given. More seriously, the claim looks false as stated. Definition 13 sorts arguments by <B, treating bound-variable-only differences as ties. If two summands are =B-equal (which happens whenever they differ only in the positions of bound variables), the paper gives no tie-break. With a stable sort—or any arbitrary order—the relative order of those summands is inherited from the input. The swap transformation then orders the outer sums by the first appearance of the bound variables in the body, so different input orders can produce different nesting orders for the same semantic term. A concrete example: X = \\Sigma_{i\\in s1}\\Sigma_{j\\in s2} (\\langle i|A|j\\rangle\\langle j|B|i\\rangle + \\langle j|A|i\\rangle\\langle i|B|j\\rangle) and Y = \\Sigma_{j\\in s2}\\Sigma_{i\\in s1} (\\langle j|A|i\\rangle\\langle i|B|j\\rangle + \\langle i|A|j\\rangle\\langle j|B|i\\rangle). These are equal by SUM-SWAP plus commutativity, but the first summand of X has i before j, the first of Y has j before i, so after Step 5 the sums are nested s1/s2 versus s2/s1, and the de Bruijn forms differ. So CheckEq would report \"not equal\" on a valid equation. The paper itself disclaims completeness in Section 7, which softens the blow—this is not a refuted soundness result, just a weaker capability than the abstract suggests.\n\nWho should read this? Anyone building quantum-program verification tools, especially on top of CoqQ or separation logic. The label-elimination theorem and the evaluation data are worth having. But a referee should push for a proof or a correction of the uniqueness claim, or an explicit statement that CheckEq is only complete for the tested fragment, plus a warning when the normalizer hits =B ties. As is, I would not treat \"not equal\" as a reliable answer.\n\nRecommendation: send to a serious referee. The paper deserves reviewer time, but it needs a fix or a disclaimer before acceptance.","headline":"D-Hammer is a real step forward for automated reasoning in labelled Dirac notation, but the normalization's confluence claim in Appendix E is unproven and my quick example suggests CheckEq can return false negatives.","tokens_in":37898,"tokens_out":7349,"would_cite":true,"duration_ms":70517,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q42","03B35","68N30","81P68"],"pacs":[],"model":"deepseek-v4-flash","headline":"D-Hammer proves labelled Dirac equalities by sound normalization and a label-elimination theorem.","keywords":["labelled Dirac notation","bra-ket notation","equational reasoning","term normalization","quantum program verification","dependently typed language","soundness","SUM-SWAP"],"falsifier":"Find two well-typed, semantically equal labelled expressions, such as the same summation body written under different nested orders of the same bound variables, and check whether D-Hammer normalizes them to different normal forms; a counterexample would refute the normalizer's completeness and make 'not equal' answers unreliable.","tokens_in":36798,"feed_emoji":"⚛️","tokens_out":5754,"duration_ms":60510,"temperature":0.7,"pith_summary":"This paper presents D-Hammer, a tool that automates equational reasoning in labelled Dirac notation, the bra-ket formalism used for many-body quantum states and quantum program assertions. It defines a dependently typed, higher-order language for such expressions, gives it a Hilbert-space denotational semantics, and proves that the equational proof system is sound with respect to that semantics. The central technical result is a label-elimination theorem showing that equality between labelled expressions reduces, soundly and completely, to equality between plain Dirac expressions. The tool then checks plain equality with a normalizing rewrite engine that handles associative-commutative symbols, summation swapping, and alpha-equivalence. The paper evaluates the implementation on textbook examples, a large Coq formalization benchmark, and labelled examples including a hard quantum separation logic identity.","feed_headline":"Labelled Dirac equations get a fast automated prover","feed_subtitle":"Soundness plus a label-elimination theorem turns pen-and-paper bra-ket proofs into seconds.","key_machinery":"The engine is a normalization algorithm that reduces equivalence modulo the axiom sets R and E to syntactic identity. It uses term rewriting for the R rules, including definition expansion, scalar and linear algebra, delta elimination, and sum pushing, then handles the E axioms with three specialized passes: sorting terms by an order that treats all bound variables as equal, reordering successive summations by the first appearance of their bound variables, and converting to de Bruijn indices to eliminate alpha-equivalence. The key design point is that sorting is done before summation order is fixed, because bound-variable names can be permuted freely in a successive sum. For labelled expressions, register-indexed kets, bras, and operators are expanded into big sums of labelled basis tensors, and sorting rules eliminate matching bra-ket pairs, eventually producing a plain Dirac expression.","core_discovery":"The paper's central claim is that equational proofs in labelled Dirac notation can be automated without losing semantic fidelity. D-Hammer's language separates indices, types, and terms, and interprets expressions in Hilbert spaces with the tensor product as an associative-commutative symbol. Theorem 1 states soundness: any equation provable from the axioms is valid in the denotational semantics. Theorem 2 states that for labelled expressions without free variables of the labelled type, eliminating labels—expanding registers to basis sums, rewriting to a normal form, then ordering and stripping labels—preserves semantic equality in both directions: Γ⊨D₁=D₂ iff Γ⊨e₁=e₂ for the translated plain equations. So the proof burden for labelled notation is reduced to proving plain Dirac equalities, and those are handled by a normalization algorithm that fully rewrites modulo the axiom set.","pith_inferences":["If the normalization algorithm were proved confluent and terminating, D-Hammer would become a decision procedure for its equational theory; the paper currently proves soundness and semantic label elimination but not completeness of the normalizer.","The two-phase sort-then-swap strategy for handling AC symbols and permutable summations may transfer to other formalisms where associative-commutative operators coexist with reorderable binders.","D-Hammer's rewriting traces are a natural starting point for machine-checkable certificates, which would let a proof assistant independently confirm each reported equality.","The label-elimination reduction suggests that labelled formalisms can often be implemented as a thin layer over an efficient plain normalizer, rather than requiring a purpose-built labelled rewriting engine."],"forward_implications":["Every equation D-Hammer reports as equal is genuinely valid in the Hilbert-space semantics, by Theorem 1.","Labelled equalities can be checked by eliminating labels and running the plain normalizer, by the iff reduction of Theorem 2.","On the plain Dirac benchmark, D-Hammer verifies 158 ported examples from a Coq formalization in under ten seconds, whereas the prior tool takes more than 45 seconds for 156 examples.","The labelled examples include LDN-10, a seven-register quantum separation logic identity that is difficult to write or prove without labels, solved in about five seconds.","The tool is not competitive with specialized quantum circuit equivalence checkers, and the authors state that D-Hammer makes no completeness claim for its rewriting theory."],"supporting_citations":[{"why":"Defines the previous plain Dirac notation prover and the rewriting basis that D-Hammer extends and benchmarks against.","marker":"[34]"},{"why":"Supplies the Coq formalization whose 162 statements are the main benchmark, and the function view of kets and bras used in the labelled semantics.","marker":"[38]"},{"why":"Source of LDN-10, the hard quantum separation logic example that motivates and demonstrates the labelled reasoning capability.","marker":"[37]"},{"why":"Provides de Bruijn indices, used by the normalization step that resolves alpha-equivalence.","marker":"[16]"}],"fun_headline_variants":["First automated prover for labelled Dirac equations","D-Hammer: fast, sound automated Dirac proofs","Label elimination speeds up Dirac equational proofs","From pen-and-paper to automated bra-ket proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the normalization algorithm is a full normalizer: any two expressions equivalent under the axioms reduce to the same syntactic normal form, and the paper asserts this for the AC and summation-swap passes without giving a confluence proof.","fun_headline_variants_meta":{"raw":{"variants":["First automated prover for labelled Dirac equations","D-Hammer: fast, sound automated Dirac proofs","Label elimination speeds up Dirac equational proofs","From pen-and-paper to automated bra-ket proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000237,"raw_usage":{"total_tokens":1456,"prompt_tokens":842,"completion_tokens":614,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":458,"completion_tokens_details":{"reasoning_tokens":554}},"tokens_in":458,"tokens_out":614,"duration_ms":6114,"temperature":1.0,"reasoning_tokens":554,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:49:12.018184+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find two well-typed, semantically equal labelled expressions, such as the same summation body written under different nested orders of the same bound variables, and check whether D-Hammer normalizes them to different normal forms; a counterexample would refute the normalizer's completeness and make 'not equal' answers unreliable.","supporting_citations":[{"cited_title":"In: 36th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2,","cited_arxiv_id":null,"evidence_quote":"Source of LDN-10, the hard quantum separation logic example that motivates and demonstrates the labelled reasoning capability."}],"review_version":1}