Computational category-theoretic rewriting

DOI10.1016/J.JLAMP.2023.100888MaRDI QIDQ6113023zbMATH OpenFDO

Authors Kristopher Brown, Evan Patterson, Tyler Hanks, James P. Fairbanks

Publication date 8 August 2023

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2111.03784

Mathematics Subject Classification ID

Computer science (68-XX)

Abstract: We demonstrate how category theory provides specifications that can efficiently be implemented via imperative algorithms and apply this to the field of graph rewriting. By examples, we show how this paradigm of software development makes it easy to quickly write correct and performant code. We provide a modern implementation of graph rewriting techniques at the level of abstraction of finitely-presented C-sets and clarify the connections between C-sets and the typed graphs supported in existing rewriting software. We emphasize that our open-source library is extensible: by taking new categorical constructions (such as slice categories, structured cospans, and distributed graphs) and relating their limits and colimits to those of their underlying categories, users inherit efficient algorithms for pushout complements and (final) pullback complements. This allows one to perform double-, single-, and sesqui-pushout rewriting over a broad class of data structures.

Cites work

• Adhesive and quasiadhesive categories
• AGREE -- algebraic graph rewriting with controlled embedding
• Algebraic approach to single-pushout graph transformation
• Analysis of graph transformation systems: native vs translation-based techniques
• Categories and Sheaves
• Category theory in context
• Concurrency theorems for non-linear rewriting theories
• Foundations of Software Science and Computation Structures
• Functorial data migration
• Graph rewriting and relabeling with PBPO^+: a unifying theory for quasitoposes
• Graph Transformation by Computational Category Theory
• How to delete categorically -- two pushout complement constructions
• scientific article; zbMATH DE number 919845 (Why is no real title available?)
• scientific article; zbMATH DE number 7456055 (Why is no real title available?)
• Kan extensions are partial colimits
• Pattern graphs and rule-based models: the semantics of Kappa
• Sesqui-Pushout Rewriting
• The Verigraph system for graph transformation

Cited in

(7)

• Using rewriting systems to compute left Kan extensions and induced actions of categories
• A categorical foundation for structured reversible flowchart languages
• Rewriting in Operads and PROPs
• Relating two categorical models of term rewriting
• Presenting a Category Modulo a Rewriting System
• Rewriting in Gray categories with applications to coherence
• Termination of graph transformation systems using weighted subgraph counting

This page was built for publication: Computational category-theoretic rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6113023)