Linear lambda terms as invariants of rooted trivalent maps

DOI10.1017/S095679681600023XzbMATH Open1420.68050arXiv1512.06751OpenAlexW2278483746MaRDI QIDQ5371978FDOQ5371978

Noam Zeilberger

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Abstract: The main aim of the article is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) 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.

Full work available at URL: https://arxiv.org/abs/1512.06751

Recommendations

• A correspondence between rooted planar maps and normal planar lambda terms
• A theory of linear typings as flows on 3-valent graphs
• Connected chord diagrams and bridgeless maps
• Quantitative Aspects of Linear and Affine Closed Lambda Terms
• Viewing \({\lambda}\)-terms through maps

Mathematics Subject Classification ID

Asymptotic enumeration (05A16) Coloring of graphs and hypergraphs (05C15) Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Functional programming and lambda calculus (68N18)

Cites Work

• Compact closed bicategories
• A Survey of Graphical Languages for Monoidal Categories
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Graphs on surfaces and their applications. Appendix by Don B. Zagier
• Title not available (Why is that?)
• Theory of Maps on Orientable Surfaces
• Map coloring and the vector cross product
• Title not available (Why is that?)
• Lie algebras and the four color theorem
• On the enumeration of planar maps
• Combinatory logic. Vol. II
• Title not available (Why is that?)
• Asymptotics and random sampling for BCI and BCK lambda terms
• Title not available (Why is that?)
• A Census of Hamiltonian Polygons
• Title not available (Why is that?)
• Title not available (Why is that?)
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
• A correspondence between rooted planar maps and normal planar lambda terms

Cited In (7)

• Quantitative Aspects of Linear and Affine Closed Lambda Terms
• Connected chord diagrams and bridgeless maps
• On some enumerative problems in lambda calculus
• Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels
• Bijections between planar maps and planar linear normal \(\lambda\)-terms with connectivity condition
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• OEIS

This page was built for publication: Linear lambda terms as invariants of rooted trivalent maps

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371978)