Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalising the Double-Pushout Approach to Graph Transformation

Robert Söldner, Detlef Plump

TL;DR

This paper utilizes Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation, establishing the uniqueness of derivations, and verifying the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof.

Abstract

In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts.

Formalising the Double-Pushout Approach to Graph Transformation

TL;DR

This paper utilizes Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation, establishing the uniqueness of derivations, and verifying the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof.

Abstract

In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts.
Paper Structure (14 sections, 18 theorems, 1 equation, 17 figures)

This paper contains 14 sections, 18 theorems, 1 equation, 17 figures.

Table of Contents

  1. Isabelle/HOL
  2. DPO Graph Transformation in Isabelle
  3. Graphs
  4. Morphisms
  5. Rules
  6. Gluings
  7. Pushouts
  8. Direct Derivations
  9. Pullbacks
  10. Composition and Decomposition of Pullbacks and Pushouts
  11. Uniqueness of Direct Derivations
  12. Church-Rosser Theorem
  13. Related Work
  14. Conclusion

Key Result

Lemma 2.6

Given two morphisms $f \colon G \to H$ and $g \colon H \to K$, the composition $g \circ f \colon G \to K$ is also a morphism.

Figures (17)

  • Figure 1: locale hierarchy reflecting our formalisation
  • Figure 2: Gluing diagram
  • Figure 3: Pushout $A \rightarrow B \rightarrow D \leftarrow C \leftarrow A$
  • Figure 4: Double-pushout diagram
  • Figure 5: Pullback $D \leftarrow C \leftarrow A \rightarrow B \rightarrow D$
  • ...and 12 more figures

Theorems & Definitions (35)

  • Definition 2.1: Graph
  • Definition 2.2: Graphs over naturals
  • Definition 2.3: Graph morphism
  • Definition 2.4: Special morphisms and isomorphic graphs
  • Definition 2.5: Morphism composition
  • Lemma 2.6: Well-definedness of morphism composition
  • Definition 2.7: Rule
  • Lemma 2.8: Gluing Ehrig79a
  • Definition 2.9: Pushout
  • Lemma 2.10: Correctness of to_ngraph
  • ...and 25 more