Metraipolis › archive › dc_14fecc245f4e

How to prove equations using diagrams: A categorical and operational semantics for e-graphs — arXiv:2611.05924

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.05924
License (as archived): CC0-1.0
Archived: 2026-11-05T18:31:54.292Z
SHA-256 of the archived text: ef103f72d93edc73b512e8314104c9709dc6ad983476b1c5bd5ec383db936588
Stable URL of this page: https://metraipolis.com/documento/dc_14fecc245f4e

How to cite

How to prove equations using diagrams: A categorical and operational semantics for e-graphs — arXiv:2611.05924 — arXiv (en), https://arxiv.org/abs/2611.05924 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_14fecc245f4e (Metraipolis archive dc_14fecc245f4e, sha256 ef103f72d93edc73b512e8314104c9709dc6ad983476b1c5bd5ec383db936588)

BibTeX

@misc{dc14fecc245f4e,
  title = {How to prove equations using diagrams: A categorical and operational semantics for e-graphs — arXiv:2611.05924},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.05924},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_14fecc245f4e; sha256 ef103f72d93edc73b512e8314104c9709dc6ad983476b1c5bd5ec383db936588},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.05924. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

E-graphs are a powerful algorithmic technique for automated equational reasoning but have resisted a conceptual understanding independent of issues of presentation and implementation. We propose an operational semantics for e-graphs based on the fundamental category-theoretic concepts of diagrams, limits, and initial functors. We illustrate the formalism through numerous example calculations and establish its soundness and completeness. Technical prerequisites are kept to a minimum in the main text; less standard elements of the mathematical theory are developed in two appendices.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv cs.LO, nuovi lavori del giorno).
Categorie arXiv: Category Theory (math.CT) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2611.05924 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-05T18:21:19.042Z dalla pagina https://arxiv.org/list/cs.LO/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).