Document Open Access Logo

Functorial String Diagrams for Reverse-Mode Automatic Differentiation

Authors Mario Alvarez-Picallo , Dan Ghica , David Sprunger , Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.6.pdf
  • Filesize: 0.95 MB
  • 20 pages

Document Identifiers

Author Details

Mario Alvarez-Picallo
  • Programming Languages Laboratory, Huawei Research Centre, Cambridge, UK
Dan Ghica
  • Department of Computer Science, University of Birmingham, UK
  • Programming Languages Laboratory, Huawei Research Centre, Cambridge, UK
David Sprunger
  • Department of Computer Science, University of Birmingham, UK
Fabio Zanasi
  • Department of Computer Science, University College London, UK

Funding

The last three authors acknowledge support from epsrc grant EP/V002376/1.

Cite As Get BibTex

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.6

Abstract

We formulate a reverse-mode automatic differentiation (RAD) algorithm for (applied) simply typed lambda calculus in the style of Pearlmutter and Siskind [Barak A. Pearlmutter and Jeffrey Mark Siskind, 2008], using the graphical formalism of string diagrams. Thanks to string diagram rewriting, we are able to formally prove for the first time the soundness of such an algorithm. Our approach requires developing a calculus of string diagrams with hierarchical features in the spirit of functorial boxes, in order to model closed monoidal (and cartesian closed) structure. To give an efficient yet principled implementation of the RAD algorithm, we use foliations of our hierarchical string diagrams.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Automatic differentiation
  • Theory of computation → Categorical semantics
Keywords
  • string diagrams
  • automatic differentiation
  • hierarchical hypergraphs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Martín Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, et al. TensorFlow: a system for large-scale machine learning. In 12th USENIX symposium on operating systems design and implementation (OSDI 16), pages 265-283, 2016. Google Scholar
  2. Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Rewriting for monoidal closed categories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022. Google Scholar
  3. John Baez and Mike Stay. Physics, topology, logic and computation: a rosetta stone. In New structures for physics, pages 95-172. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_2.
  4. Atilim Gunes Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind. Automatic differentiation in machine learning: a survey. J. Mach. Learn. Res., 18:153:1-153:43, 2017. URL: http://jmlr.org/papers/v18/17-468.html.
  5. Atilim Günes Baydin, Barak A. Pearlmutter, and Jeffrey Mark Siskind. Diffsharp: An AD library for .net languages. CoRR, abs/1611.03423, 2016. URL: http://arxiv.org/abs/1611.03423.
  6. Nick Benton, Gavin Bierman, Valeria De Paiva, and Martin Hyland. Linear λ-calculus and categorical models revisited. In International Workshop on Computer Science Logic, pages 61-84. Springer, 1992. Google Scholar
  7. Richard F Blute, J Robin B Cockett, and Robert AG Seely. Cartesian differential categories. Theory and Applications of Categories, 22(23):622-672, 2009. Google Scholar
  8. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 710-719. ACM, 2016. URL: https://doi.org/10.1145/2933575.2935316.
  9. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Deconstructing lawvere with distributive laws. J. Log. Algebraic Methods Program., 95:128-146, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.12.002.
  10. Aloïs Brunel, Damiano Mazza, and Michele Pagani. Backpropagation in the simply typed lambda-calculus with linear negation. Proc. ACM Program. Lang., 4(POPL):64:1-64:27, 2020. URL: https://doi.org/10.1145/3371132.
  11. Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical computer science, 115(1):43-62, 1993. Google Scholar
  12. Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk. Reverse derivative categories. arXiv preprint, 2019. URL: http://arxiv.org/abs/1910.07065.
  13. Conal Elliott. The simple essence of automatic differentiation. Proceedings of the ACM on Programming Languages, 2(ICFP):1-29, 2018. Google Scholar
  14. Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363-375. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190269.
  15. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  16. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types, volume 7. Cambridge university press Cambridge, 1989. Google Scholar
  17. Stefano Guerrini. A general theory of sharing graphs. Theor. Comput. Sci., 227(1-2):99-151, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00050-X.
  18. Yves Guiraud. Rewriting methods in higher algebra. PhD thesis, Université Paris 7, 2019. Google Scholar
  19. Chris Heunen and Jamie Vicary. Lectures on categorical quantum mechanics. Computer Science Department. Oxford University, 2012. URL: http://www.cs.ox.ac.uk/files/4551/cqm-notes.pdf.
  20. Dominic Hughes. Simple free star-autonomous categories and full coherence. CoRR, 2005. URL: http://arxiv.org/abs/0506521.
  21. Mathieu Huot, Sam Staton, and Matthijs Vákár. Correctness of automatic differentiation via diffeologies and categorical gluing. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 319-338. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_17.
  22. Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A Eisenberg, and Andrew W Fitzgibbon. Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. Google Scholar
  23. John Lamping. An algorithm for optimal lambda calculus reduction. In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 16-30. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96711.
  24. Ian Mackie. Interaction nets for linear logic. Theor. Comput. Sci., 247(1-2):83-140, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00198-5.
  25. Paul-André Melliès. Functorial boxes in string diagrams. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 1-30. Springer, 2006. URL: https://doi.org/10.1007/11874683_1.
  26. Koko Muroya and Dan R. Ghica. The dynamic geometry of interaction machine: A token-guided graph rewriter. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:7)2019.
  27. Barak A. Pearlmutter and Jeffrey Mark Siskind. Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator. ACM Trans. Program. Lang. Syst., 30(2):7:1-7:36, 2008. URL: https://doi.org/10.1145/1330017.1330018.
  28. Ralf Schweimeier and Alan Jeffrey. A categorical and graphical treatment of closure conversion. In Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov, editors, Fifteenth Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999, volume 20 of Electronic Notes in Theoretical Computer Science, pages 481-511. Elsevier, 1999. URL: https://doi.org/10.1016/S1571-0661(04)80090-2.
  29. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. URL: http://arxiv.org/abs/0908.3347.
  30. Michael Shulman. *-autonomous envelopes and 2-conservativity of duals. CoRR, 2020. URL: http://arxiv.org/abs/2004.08487.
  31. Jeffrey Mark Siskind and Barak A. Pearlmutter. Efficient implementation of a higher-order language with built-in AD. CoRR, abs/1611.03416, 2016. URL: http://arxiv.org/abs/1611.03416.
  32. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006. Google Scholar
  33. Matthijs Vákár. Reverse AD at higher types: Pure, principled and denotationally correct. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 607-634. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_22.
  34. Jamie Vicary and Antonin Delpeuch. Normalization for planar string diagrams and a quadratic equivalence algorithm. Logical Methods in Computer Science, 18, 2022. Google Scholar
  35. Jamie Vicary, Aleks Kissinger, and Krzysztof Bar. Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14, 2018. Google Scholar
  36. Fei Wang, Daniel Zheng, James M. Decker, Xilun Wu, Grégory M. Essertel, and Tiark Rompf. Demystifying differentiable programming: shift/reset the penultimate backpropagator. Proc. ACM Program. Lang., 3(ICFP):96:1-96:31, 2019. URL: https://doi.org/10.1145/3341700.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact