[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Mechanised DPO Theory: Uniqueness of Derivations and Church-Rosser Theorem

  • Conference paper
  • First Online:
Graph Transformation (ICGT 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13961))

Included in the following conference series:

  • 383 Accesses

Abstract

We demonstrate how to use the proof assistant Isabelle/HOL to obtain machine-checked proofs of two fundamental theorems in the double-pushout approach to graph transformation: the uniqueness of derivations up to isomorphism and the so-called Church-Rosser theorem. The first result involves proving the uniqueness of pushout complements, first established by Rosen in 1975. The second result formalises Ehrig’s and Kreowski’s proof of 1976 that parallelly independent direct derivations can be interchanged to obtain derivations ending in a common graph. We also show how to overcome Isabelle’s limitation that graphs in locales must have nodes and edges of pre-defined types.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 43.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 54.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Log. 9(1), 2 (2007). https://doi.org/10.1145/1297658.1297660

    Article  MathSciNet  MATH  Google Scholar 

  2. Ballarin, C.: Tutorial to locales and locale interpretation (2021). https://isabelle.in.tum.de/doc/locales.pdf

  3. Brucker, A.D., Herzberg, M.: A formal semantics of the core DOM in Isabelle/HOL. In: Companion Proceedings of the The Web Conference 2018, WWW 2018, pp. 741–749. International World Wide Web Conferences Steering Committee (2018). https://doi.org/10.1145/3184558.3185980

  4. Campbell, G., Courtehoute, B., Plump, D.: Fast rule-based graph programs. Sci. Comput. Program. 214 (2022). https://doi.org/10.1016/j.scico.2021.102727

  5. da Costa Cavalheiro, S.A., Foss, L., Ribeiro, L.: Theorem proving graph grammars with attributes and negative application conditions. Theoret. Comput. Sci. 686, 25–77 (2017). https://doi.org/10.1016/j.tcs.2017.04.010

    Article  MathSciNet  MATH  Google Scholar 

  6. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. MTCSAES, Springer, Heidelberg (2006). https://doi.org/10.1007/3-540-31188-2

    Book  MATH  Google Scholar 

  7. Ehrig, H., Kreowski, H.-J.: Parallelism of manipulations in multidimensional information structures. In: Mazurkiewicz, A. (ed.) MFCS 1976. LNCS, vol. 45, pp. 284–293. Springer, Heidelberg (1976). https://doi.org/10.1007/3-540-07854-1_188

    Chapter  Google Scholar 

  8. Ehrig, H., Kreowski, H.J.: Pushout-properties: an analysis of gluing constructions for graphs. Math. Nachr. 91, 135–149 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87827-8_28

    Chapter  Google Scholar 

  10. Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comput. Sci. 11(5), 637–688 (2001). https://doi.org/10.17/S0960129501003425

  11. Hales, T., et al.: A formal proof of the Kepler conjecture. In: Forum of Mathematics, Pi, vol 5 (2015). https://doi.org/10.1017/fmp.2017.1

  12. Hristakiev, I., Plump, D.: Attributed graph transformation via rule schemata: Church-Rosser theorem. In: Milazzo, P., Varró, D., Wimmer, M. (eds.) STAF 2016. LNCS, vol. 9946, pp. 145–160. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50230-4_11

    Chapter  Google Scholar 

  13. Huth, M., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  14. Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings Symposium on Operating Systems Principles (SOSP 2009), pp. 207–220. Association for Computing Machinery (2009). https://doi.org/10.1145/1629575.1629596

  15. Lack, S., Sobociński, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FoSSaCS 2004. LNCS, vol. 2987, pp. 273–288. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24727-2_20

    Chapter  Google Scholar 

  16. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814

    Article  Google Scholar 

  17. Libkin, L.: Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Cham (2004). https://doi.org/10.1007/978-3-662-07003-1

  18. Nipkow, T., Klein, G.: Concrete Semantics: with Isabelle/HOL. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10542-0. http://concrete-semantics.org/

  19. Noschinski, L.: A graph library for Isabelle. Math. Comput. Sci. 9(1), 23–39 (2014). https://doi.org/10.1007/s11786-014-0183-z

    Article  MathSciNet  MATH  Google Scholar 

  20. Paulson, L.C., Nipkow, T., Wenzel, M.: From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6), 675–698 (2019). https://doi.org/10.1007/s00165-019-00492-1

  21. Plump, D.: Reasoning about graph programs. In: Proceedings with Terms and Graphs (TERMGRAPH 2016). Electronic Proceedings in Theoretical Computer Science, vol. 225, pp. 35–44 (2016). https://doi.org/10.4204/EPTCS.225.6

  22. Rosen, B.K.: Deriving graphs from graphs by applying a production. Acta Informatica 4, 337–357 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  23. Schirmer, N., Wenzel, M.: State spaces - the locale way. In: Proceedings International Workshop on Systems Software Verification (SSV 2009). Electronic Notes in Theoretical Computer Science, vol. 254, pp. 161–179 (2009). https://doi.org/10.1016/j.entcs.2009.09.065

  24. Söldner, R., Plump, D.: Towards Mechanised proofs in Double-Pushout graph transformation. In: Proceedings International Workshop on Graph Computation Models (GCM 2022). Electronic Proceedings in Theoretical Computer Science, vol. 374, pp. 59–75 (2022). https://doi.org/10.4204/EPTCS.374.6

  25. Strecker, M.: Interactive and automated proofs for graph transformations. Math. Struct. Comput. Sci. 28(8), 1333–1362 (2018). https://doi.org/10.1017/S096012951800021X

    Article  MathSciNet  MATH  Google Scholar 

  26. Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_12

    Chapter  Google Scholar 

  27. Wulandari, G.S., Plump, D.: Verifying graph programs with monadic second-order logic. In: Gadducci, F., Kehrer, T. (eds.) ICGT 2021. LNCS, vol. 12741, pp. 240–261. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78946-6_13

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

We are grateful to Brian Courthoute and Annegret Habel for discussions on the topics of this paper.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, UK

    Robert Söldner & Detlef Plump

Authors
  1. Robert Söldner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Detlef Plump
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robert Söldner .

Editor information

Editors and Affiliations

  1. King's College London, London, UK

    Maribel Fernández

  2. Singapore Management University, Singapore, Singapore

    Christopher M. Poskitt

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Söldner, R., Plump, D. (2023). Mechanised DPO Theory: Uniqueness of Derivations and Church-Rosser Theorem. In: Fernández, M., Poskitt, C.M. (eds) Graph Transformation. ICGT 2023. Lecture Notes in Computer Science, vol 13961. Springer, Cham. https://doi.org/10.1007/978-3-031-36709-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-36709-0_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-36708-3

  • Online ISBN: 978-3-031-36709-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation