pith. sign in

arxiv: 2604.17592 · v1 · submitted 2026-04-19 · 💻 cs.LO · cs.PL

TensorRocq: Enabling diagrammatic reasoning in Rocq

Benjamin Caldwell , William Spencer , Robert Rand This is my paper

Pith reviewed 2026-05-10 04:55 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords symmetric monoidal categoriesstring diagramsdiagrammatic reasoningRocqproof assistantstensor semanticshypergraphs with interfaces
0
0 comments X

The pith

Tools in Rocq convert symmetric monoidal category terms to hypergraphs with interfaces to support verified reasoning about string diagram deformations.

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

Symmetric monoidal categories provide a framework for parallel and sequential composition in computation. String diagrams offer a visual way to reason about equations by emphasizing connectivity over syntactic details. Formal proofs in Rocq, however, force users to manipulate rigid composition structures, producing long sequences of uninformative steps. The paper supplies verified tools that translate syntactic SMC terms into hypergraphs with interfaces while maintaining a common tensor semantics. These tools enable inference of term equivalence and rewriting that respects the deformations allowed by string diagrams, and they integrate with theories built from generators and relations as well as with existing tensor-based verification projects.

Core claim

By converting syntactic representations of SMC terms into hypergraphs with interfaces while preserving tensor semantics, verified tools in Rocq support inferring term equivalence and rewriting modulo the allowed deformations of string diagrams.

What carries the argument

The conversion between syntactic SMC terms and hypergraphs with interfaces that preserves tensor semantics and captures diagram deformations.

If this is right

  • Users can build simple SMC theories from generators and relations and carry out equational reasoning inside them.
  • Tactics become usable inside existing verification projects that assign tensor semantics to SMCs.
  • Equivalence proofs can ignore fine syntactic composition details and focus on connectivity.
  • Rewriting steps are valid precisely when they correspond to allowed string diagram deformations.

Where Pith is reading between the lines

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

  • The translation reduces the distance between informal diagrammatic arguments used on paper and fully formal proofs inside a proof assistant.
  • The same hypergraph representation could serve as an intermediate form for diagrammatic reasoning in other categorical structures.
  • Once equivalence checking is available, automated search for diagram simplifications or normal forms becomes feasible within Rocq.

Load-bearing premise

The conversion between syntactic SMC terms and hypergraphs with interfaces correctly preserves tensor semantics and fully captures all allowed deformations of string diagrams.

What would settle it

An SMC term pair where two diagrams are related by a permitted deformation yet their corresponding hypergraphs are not equivalent, or where the tensor interpretations of the term and hypergraph diverge.

Figures

Figures reproduced from arXiv: 2604.17592 by Benjamin Caldwell, Robert Rand, William Spencer.

Figure 1
Figure 1. Figure 1: A visualization of tensor terms, including contraction, product, and tensors with multiple inputs. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A labeled directed hypergraph with interfaces on the left and right. The interfaces fix the order on the [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The decomposition given by Lemma 3. Lemma 4 (Double Pushout Rewrite). For a hypergraph 𝐻 with interfaces 𝑉𝐿 and 𝑉𝑅 and a rewrite rule 𝑇 = 𝑇 ′ where 𝑇 is a subgraph of 𝐻, we can perform the decomposition procedure as in Lemma 3, replacing the term 𝑇 with 𝑇 ′ . Both Lemma 3 and Lemma 4 have been well explored and proved through the language of cospans of hypergraphs [2]. Their inclusion here serves to illust… view at source ↗
Figure 4
Figure 4. Figure 4: The core rewrite engine of TensorRocq, showing how APROPs and hypergraphs are equivalent and [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
read the original abstract

Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, leveraging eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition occludes the essential connective information, longer proofs filled with uninformative syntactic manipulation. To address the gap between proof assistants and paper proof, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning these systems. We also enable our tactics to be used in existing verification projects about SMCs which can be given semantics as tensor expressions.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 1 minor

Summary. The manuscript presents TensorRocq, a Rocq development providing verified tools for diagrammatic reasoning over symmetric monoidal categories. It converts syntactic SMC terms to hypergraphs with interfaces while preserving a common tensor semantics, thereby supporting inference of term equivalence and equational rewriting modulo string-diagram deformations. The library also supplies infrastructure for defining SMC theories from generators and relations and for integrating the tactics into existing verification projects that interpret terms as tensor expressions.

Significance. If the conversion is shown to be both sound and complete with respect to the tensor semantics for the full class of SMC-licensed deformations, the work would meaningfully reduce the syntactic overhead of equational proofs in proof assistants and make diagrammatic intuition directly usable inside Rocq. This could accelerate formal developments in areas that already employ SMCs (e.g., quantum protocols, concurrency, or categorical semantics) and encourage wider adoption of string-diagram techniques in machine-checked reasoning.

major comments (1)
  1. [Abstract] Abstract and the description of the conversion: the central claim that the tools correctly infer equivalence and support rewriting modulo all allowed deformations requires that hypergraph equivalence is both sound and complete with respect to SMC term equivalence under the tensor semantics. The manuscript asserts preservation of a common semantics but does not appear to contain an explicit machine-checked theorem establishing the if-and-only-if correspondence for the full set of topological rewrites licensed by the SMC axioms. Without such a completeness result, rewriting may miss valid equivalences or accept invalid ones.
minor comments (1)
  1. The abstract would benefit from a brief concrete example illustrating a non-trivial deformation that the hypergraph representation captures but that is cumbersome in pure syntactic rewriting.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thorough review and constructive feedback. The positive assessment of TensorRocq's potential impact is appreciated. Below we address the major comment point by point, providing the strongest honest defense of the manuscript while acknowledging where clarification is warranted.

read point-by-point responses

  1. Referee: [Abstract] Abstract and the description of the conversion: the central claim that the tools correctly infer equivalence and support rewriting modulo all allowed deformations requires that hypergraph equivalence is both sound and complete with respect to SMC term equivalence under the tensor semantics. The manuscript asserts preservation of a common semantics but does not appear to contain an explicit machine-checked theorem establishing the if-and-only-if correspondence for the full set of topological rewrites licensed by the SMC axioms. Without such a completeness result, rewriting may miss valid equivalences or accept invalid ones.

    Authors: We agree that soundness and completeness are central to the claims. The manuscript establishes that the term-to-hypergraph conversion preserves tensor semantics, which directly yields soundness: any equivalence inferred or used for rewriting via hypergraph deformation is valid under the common semantics, so invalid equivalences cannot be accepted. The hypergraph construction (with interfaces and hyperedges) is defined to encode precisely the connectivity and topological deformations licensed by the SMC axioms, ensuring that the supported rewrites align with string-diagram deformations. We acknowledge that the current text does not isolate a single machine-checked if-and-only-if theorem covering the full set of deformations. We will revise the manuscript to add an explicit soundness theorem statement (already implicit in the semantics preservation lemmas) together with a discussion of completeness grounded in the construction and the known correspondence between SMC axioms and string-diagram isotopy. This will be a partial revision that clarifies the claims without changing the core development. revision: partial

Circularity Check

0 steps flagged

No circularity: verified implementation defines and proves its own conversions

full rationale

The paper presents a Rocq development that defines syntactic-to-hypergraph conversions for SMC terms and claims semantic preservation. This is self-contained formal work: the representations are introduced, the conversion functions are implemented, and preservation is established inside the proof assistant rather than by reducing to prior fitted values, self-citations, or tautological redefinitions. No equations or steps in the abstract reduce a claimed result to its own inputs by construction, and the central contribution (tactics for diagrammatic reasoning) consists of new verified code rather than a renaming or imported uniqueness theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard properties of symmetric monoidal categories and the assumption that hypergraphs faithfully model string-diagram deformations; no free parameters or new invented entities are introduced in the abstract.

axioms (2)
  • standard math Symmetric monoidal categories satisfy the standard associativity, commutativity, and unit laws for the tensor product.
    Invoked as the semantic foundation for both the syntactic terms and the hypergraph representation.
  • domain assumption String diagrams represent equations in SMCs via connectivity and continuous deformations.
    Core modeling assumption that justifies rewriting modulo deformation.

pith-pipeline@v0.9.0 · 5472 in / 1365 out tokens · 49781 ms · 2026-05-10T04:55:05.984559+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    Journal of the ACM (JACM)69(2), 1–58 (2022)

    Bonchi, F., Gadducci, F., Kissinger, A., Sobocinski, P., Zanasi, F.: String diagram rewrite theory i: Rewriting with frobenius structure. Journal of the ACM (JACM)69(2), 1–58 (2022)

    work page 2022

  2. [2]

    Mathematical Structures in Computer Science32(4), 511–541 (2022)

    Bonchi, F., Gadducci, F., Kissinger, A., Sobocinski, P., Zanasi, F.: String diagram rewrite theory ii: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science32(4), 511–541 (2022)

    work page 2022

  3. [3]

    Mathematical Structures in Computer Science32(7), 829–869 (2022)

    Bonchi, F., Gadducci, F., Kissinger, A., Sobociński, P., Zanasi, F.: String diagram rewrite theory iii: Confluence with and without frobenius. Mathematical Structures in Computer Science32(7), 829–869 (2022)

    work page 2022

  4. [4]

    An automated deductive verification framework for circuit-building quantum programs

    Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) Programming Languages and Systems, ESOP 2021. Lec- ture Notes in Computer Science, vol. 12648, pp. 148–177. Springer International Publishing, Cham (March 2021). https://doi.org/10.1007/...

    work page doi:10.1007/978-3-030-72019-3_6 2021

  5. [5]

    New Journal of Physics 13(4), p

    Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics13(4), 043016 (apr 2011). https://doi.org/10.1088/1367-2630/13/4/043016

    work page doi:10.1088/1367-2630/13/4/043016 2011

  6. [6]

    Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning

    Coecke, B., Kissinger, A.: Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press (2017). https://doi.org/10.1017/9781316219317

    work page doi:10.1017/9781316219317 2017

  7. [7]

    In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming

    Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming. p. 235–246. ICFP ’02, Association for Computing Machinery, New York, NY, USA (2002). https://doi.org/10.1145/581478.581501, https://doi.org/10.1145/581478.581501

    work page doi:10.1145/581478.581501 2002

  8. [8]

    In: Hurd, J., Melham, T

    Gregoire, B., Mahboubi, A.: Proving Equalities in a Commutative Ring Done Right in Coq. In: Hurd, J., Melham, T. (eds.) Lecture Notes in Computer Science. Lecture Notes in Computer Science, vol. 3603, pp. 98–113. Springer, Oxford, United Kingdom (Aug 2005). https://doi.org/10.1007/11541868_7, https://inria.hal.science/hal-00819484

    work page doi:10.1007/11541868_7 2005

  9. [9]

    In: Cohen, L., Kaliszyk, C

    Hietala, K., Rand, R., Hung, S.H., Li, L., Hicks, M.: Proving Quantum Programs Correct. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 21:1–21:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021)....

    work page doi:10.4230/lipics.itp.2021.21 2021

  10. [10]

    INQWIRE Developers: INQWIRE QuantumLib (1 2022), https://github.com/inQWIRE/QuantumLib

    work page 2022

  11. [11]

    Kissinger, A.: Abstract Tensor Systems as Monoidal Categories, pp. 235–252. Springer Berlin Heidelberg, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54789-8_13, https://doi.org/10.1007/978-3-642-54789-8_13

    work page doi:10.1007/978-3-642-54789-8_13 2014

  12. [12]

    https: //github.com/akissinger/chyp (2023)

    Kissinger, A.: GitHub - akissinger/chyp: An interactive theorem prover for string diagrams — github.com. https: //github.com/akissinger/chyp (2023)

    work page 2023

  13. [13]

    Krebbers, R., Jung, R.: Rocq-std++, https://gitlab.mpi-sws.org/iris/stdpp

    work page

  14. [14]

    Lehmann, A., Caldwell, B., Shah, B., Spencer, W., Rand, R.: Vyzx: Formal verification of a graphical quantum language (2026), https://arxiv.org/abs/2311.11571

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  15. [15]

    Online book (2021)

    Mahboubi, A., Tassi, E.: Mathematical components. Online book (2021)

    work page 2021

  16. [16]

    Nielsen and Isaac L

    Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, Cambridge (December 2010). https://doi.org/10.1017/CBO9780511976667

    work page doi:10.1017/cbo9780511976667 2010

  17. [17]

    arXiv preprint arXiv:2602.19806 (2026)

    Pous, D.: String diagrams for monoidal categories, in rocq. arXiv preprint arXiv:2602.19806 (2026)

    work page arXiv 2026

  18. [18]

    Selinger

    Selinger, P.: A survey of graphical languages for monoidal categories. In: New Structures for Physics, pp. 289–355. Springer Berlin Heidelberg (2010). https://doi.org/10.1007/978-3-642-12821-9_4

    work page doi:10.1007/978-3-642-12821-9_4 2010

  19. [19]

    In: Johnson, M., Myers, D.J

    Shah, B., Spencer, W., Zielinski, L., Caldwell, B., Lehmann, A., Rand, R.: ViCAR: Visualizing Categories with Automated Rewriting in Coq. In: Johnson, M., Myers, D.J. (eds.) Proceedings Seventh International Conference on Applied Category Theory 2024, Oxford, United Kingdom, 17 - 21 June 2024. Electronic Proceedings in Theoretical Computer Science, vol. 4...

    work page doi:10.4204/eptcs.429.13 2024