zbMATH — the first resource for mathematics

Linear lambda terms as invariants of rooted trivalent maps. (English) Zbl 1420.68050
Summary: The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by O. Bodini et al. [Theor. Comput. Sci. 502, 227–238 (2013; Zbl 1297.68184)]) between \(\alpha\)-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact-oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. We begin by recalling a familiar diagrammatic representation for linear lambda terms, while at the same time explaining how such diagrams may be read formally as a notation for endomorphisms of a reflexive object in a symmetric monoidal closed (bi)category. From there, the “easy” direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other direction views linear lambda terms as complete invariants of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style topological recurrence on maps with free edges. As an application in combinatorics, we use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed proper subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus.

68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
03G30 Categorical logic, topoi
05A16 Asymptotic enumeration
05C15 Coloring of graphs and hypergraphs
Full Text: DOI arXiv
[1] Barendregt, H. P. (1984) The Lambda Calculus: Its Syntax and Semantics, Studies in Logic, vol. 103, 2nd revised ed., Amsterdam, North-Holland.0774952 · Zbl 0551.03007
[2] Bar-Natan, D., Lie algebras and the four color theorem., Combinatorica, 17, 43-52, (1997) · Zbl 0880.17005
[3] Bodini, O.; Gardy, D.; Jacquot, A., Asymptotics and random sampling for BCI and BCK lambda terms., Theor. Comput. Sci., 502, 227-238, (2013) · Zbl 1297.68184
[4] Curry, H. B., Hindley, J. R. & Seldin, J. P. (1972) Combinatory Logic, vol. II, North-Holland. · Zbl 0242.02029
[5] Hyland, M. (2013) Classical lambda calculus in modern dress. Mathematical Structures in Computer Science. In special issue dedicated to Corrado Böhm for his 90th birthday, pp. 1-20.
[6] Jacobs, B. (1993) Semantics of lambda-I and of other substructural lambda calculi. In Typed Lambda Calculus and Applications, LNCS, vol. 664. Springer, pp. 195-208. · Zbl 0795.68126
[7] Jones, G. A.; Singerman, D., Theory of maps on orientable surfaces., Proc. Lond. Math. Soc., 37, 273-307, (1978) · Zbl 0391.05024
[8] Jones, G. A. & Singerman, D. (1994) Maps, hypermaps, and triangle groups. In The Grothendieck Theory of Dessins d’Enfants, Schneps, L. (ed), London Mathematical Society Lecture Note Series, vol. 200. Cambridge University Press, pp. 115-145. · Zbl 0833.20045
[9] Joyal, A.; Street, R., The geometry of tensor calculus I., Adv. Math., 102, 20-78, (1991)
[10] Kauffman, L. H., Map coloring and the vector cross product., J. Comb. Theory B, 48, 145-154, (1990) · Zbl 0638.05025
[11] Knuth, D. E. (1970) Examples of formal semantics. In Symposium on Semantics of Algorithmic Languages, Engeler, E. (ed), Lecture Notes in Mathematics, vol. 188. Springer, pp. 212-235.
[12] Lando, S. K. & Zvonkin, A. K. (2004) Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences, vol. 141. Springer-Verlag. · Zbl 1040.05001
[13] Mairson, H. G. (2002) From Hilbert spaces to Dilbert spaces: Context semantics made simple. In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science. Kanpur, India, Springer, pp. 2-17. · Zbl 1027.68080
[14] Mairson, H. G., Linear lambda calculus and PTIME-completeness., J. Funct. Program., 14, 6, (2004) · Zbl 1063.68036
[15] (2016) The On-Line Encyclopedia of Integer Sequences.
[16] Penrose, R. (1971) Applications of negative dimensional tensors. In Combinatorial Mathematics and its Application, Welsh, D. (ed). Academic Press, pp. 221-243. · Zbl 0216.43502
[17] Scott, D. S. (1980) Relating theories of the λ-calculus. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Hindley & Seldin (eds). Academic Press, pp. 403-450.
[18] Seely, R. A. G. (1987) Modelling computations: A 2-categorical framework. In Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, Ithaca, NY, USA, IEEE Computer Society, pp. 65-71.
[19] Selinger, P. (2011) A survey of graphical languages for monoidal categories. In New Structures for Physics, Coecke, B. (ed), Springer Lecture Notes in Physics, vol. 813. Springer, pp. 289-355. · Zbl 1217.18002
[20] Stay, M. (2013) Compact closed bicategories. Theory and Applications of Categories 31 (2016), pp. 755-798. · Zbl 1356.18003
[21] Thomas, R., An update on the four-color theorem, Not. Am. Math. Soc., 45, 848-859, (1998) · Zbl 0908.05040
[22] Tutte, W. T., A census of Hamiltonian polygons., Can. J. Math., 14, 402-417, (1962) · Zbl 0105.17601
[23] Tutte, W. T., On the enumeration of planar maps., Bull. Am. Math. Soc., 74, 64-74, (1968) · Zbl 0157.31101
[24] Vidal, S. (2010) Groupe Modulaire et Cartes Combinatoires: Génération et Comptage. PhD Thesis, Université Lille I, France (July).
[25] Zeilberger, N. (2015a) Balanced polymorphism and linear lambda calculus. Talk at TYPES 2015, Tallinn, Estonia (18 May).
[26] Zeilberger, N. (2015b) Counting isomorphism classes of β-normal linear lambda terms. arXiv:1509.07596 (25 September)
[27] Zeilberger, N.; Giorgetti, A., A correspondence between rooted planar maps and normal planar lambda terms, Log. Methods Comput. Sci., 11, 1-39, (2015) · Zbl 1448.03010
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.