Combinatorial Dyson–Schwinger equations and inductive data type

Abstract

The goal of this contribution is to explain the analogy between combinatorial Dyson–Schwinger equations and inductive data types to a readership of mathematical physicists. The connection relies on an interpretation of combinatorial Dyson–Schwinger equations as fixpoint equations for olynomial functors (established elsewhere by the author, and summarised here), combined with he now-classical fact that polynomial functors provide semantics for inductive types. The paper is xpository, and comprises also a brief introduction to type theory.

Keywords

Dyson–Schwinger equations / type theory / inductive types / bialgebras / polynomial unctors

References

[1] Programming Logic group at Chalmers and Gothenburg University, Agda, http://wiki.portal.chalmers.se/agda/pmwiki.php

[2] C. Bergbauer and D. Kreimer, Hopf algebras in renormalization theory: locality and Dyson-Schwinger equations from Hochschild cohomology, in: Physics and Number Theory, Vol. 10 of IRMA Lect. Math. Theor. Phys., Zürich: Eur. Math. Soc., 2006, pp. 133–164, arXiv: hep-th/0506190

[3] A. Connes and D. Kreimer, Hopf algebras, renormalization and noncommutative geometry, Comm. Math. Phys. 199, 203 (1998), arXiv: hep-th/9808042

[4] Coq Development Team, INRIA-Rocquencourt. Coq, https://coq.inria.fr/

[5] H. Figueroa and J. M. Gracia-Bondía. Combinatorial Hopf algebras in quantum field theory (I): Rev. Math. Phys. 17, 881 (2005), arXiv: hep-th/0408145

[6] L. Foissy, Faà di Bruno subalgebras of the Hopf algebra of planartrees from combinatorial Dyson-Schwinger equations, Adv. Math. 218, 136 (2008), arXiv: 0707.1204

[7] I. Gálvez-Carrillo, J. Kock, and A. Tonks, Groupoids and Faà di Bruno formulae for Green functions in bialgebras of trees, Adv. Math. 254, 79 (2014), arXiv: 1207.6404

[8] N. Gambino and J. Kock, Polynomial functors and polynomial monads, Math. Proc. Cambridge Phil. Soc. 154, 153 (2013), arXiv: 0906.4931

[9] J. Kock, Polynomial functors and trees, Int. Math. Res. Notices 2011, 609 (2011), aArXiv: 0807.2874

[10] J. Kock, Data types with symmetries and polynomial functors over groupoids, in: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (Bath, 2012), Vol. 286 of Electronic Notes in Theoretical Computer Science, 2012, pp. 351–365, arXiv: 1210.0828

[11] J. Kock, Categorification of Hopf algebras of rooted trees, Cent. Eur. J. Math. 11, 401 (2013), arXiv: 1109.5785

[12] J. Kock, Perturbative renormalisation for not-quite-connected bialgebras, Lett. Math. Phys. 105, 1413 (2015), arXiv: 1411.3098

[13] J. Kock, Polynomial functors and combinatorial Dyson-Schwinger equations, arXiv: 1512.03027

[14] J. Kock, Categorical formalisms for graphs and trees in quantum field theory (in preparation)

[15] D. Kreimer, On the Hopf algebra structure of perturbative quantum field theories, Adv. Theor. Math. Phys. 2, 303 (1998), arXiv: qalg/9707029

[16] D. Kreimer, Anatomy of a gauge theory, Ann. Physics 321, 2757(2006), arXiv: hep-th/0509135

[17] F. W. Lawvere and R. Rosebrugh, Sets for Mathematics, Cambridge: Cambridge University Press, 2003

[18] T. Leinster, Basic category theory, Vol. 143 of Cambridge Studies in Advanced Mathematics, Cambridge: Cambridge University Press, 2014

[19] P. L. Lumsdaine and M. Shulman, Semantics of higher inductive types, Available at http://uf-ias-2012.wikispaces.com/file/view/semantics.pdf

[20] P. Martin-Löf, Constructive mathematics and computer programming, in: Logic, Methodology and Philosophy of Science, VI (Hannover, 1979), Vol. 104 of Stud. Logic Found. Math., Amsterdam: North-Holland, 1982, pp. 153–175

[21] I. Mencattini and D. Kreimer, The structure of the ladder insertion-elimination Lie algebra, Comm. Math. Phys. 259, 413 (2005), arXiv: math-ph/0408053

[22] I. Moerdijk and E. Palmgren, Well founded trees in categories, Ann. Pure Appl. Logic 104, 189 (2000)

[23] B.Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Löf type theory: An introduction, Vol. 7 of International Series of Monographs on Computer Science, New York: The Clarendon Press, Oxford University Press, 1990

[24] C. D. Roberts, Strong QCD and Dyson-Schwinger equations, in: Faà di Bruno Hopf algebras, Dyson-Schwinger equations, and Lie-Butcher series, Vol. 21 of IRMA Lect. Math. Theor. Phys., Zürich: Eur. Math. Soc., 2015, pp. 355–458, arXiv: 1203.5341

[25] D. I. Spivak, Category Theory for the Sciences, MA, Cambridge: MIT Press, 2014

[26] The Univalent Foundations Program, Homotopy type theory — Univalent foundations of mathematics, The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ, 2013. Available from http://homotopytypetheory.org/book

[27] W. D. van Suijlekom, The structure of renormalization Hopf algebras for gauge theories. I. Representing Feynman graphs on BV algebras, Comm. Math. Phys. 290, 291 (2009), arXiv: 0807.0999

[28] S. Weinzierl, Hopf algebras and Dyson-Schwinger equations, in: This volume, 2015, arXiv: 1506.09119

RIGHTS & PERMISSIONS

2015 The Author(s). This article is published with open access at www.springer.com/11467 and journal.hep.com.cn/fop