Reference. Linear lambda terms as invariants of rooted trivalent maps
The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between α-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.
Cite
Cited by (4)
Asymptotic distribution of parameters in trivalent maps and linear lambda terms bodini-2025-asymptotic
Connected Chord Diagrams and Bridgeless Maps courtiel-2019-connected
We present a surprisingly new connection between two well-studied combinatorial classes: rooted connected chord diagrams on one hand, and rooted bridgeless combinatorial maps on the other hand. We describe a bijection between these two classes, which naturally extends to indecomposable diagrams and general rooted maps. As an application, this bijection provides a simplifying framework for some technical quantum field theory work realized by some of the authors. Most notably, an important but technical parameter naturally translates to vertices at the level of maps. We also give a combinatorial proof to a formula which previously resulted from a technical recurrence, and with similar ideas we prove a conjecture of Hihn. Independently, we revisit an equation due to Arquès and Béraud for the generating function counting rooted maps with respect to edges and vertices, giving a new bijective interpretation of this equation directly on indecomposable chord diagrams, which moreover can be specialized to connected diagrams and refined to incorporate the number of crossings. Finally, we explain how these results have a simple application to the combinatorics of lambda calculus, verifying the conjecture that a certain natural family of lambda terms is equinumerous with bridgeless maps.
A sequent calculus for a semi-associative law zeilberger-2019-a
We introduce a sequent calculus with a simple restriction of Lambek’s product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice .
A theory of linear typings as flows on 3-valent graphs zeilberger-2018-a
Cites 27 works (0 here)
External (27)
- The On-Line Encyclopedia of Integer Sequences (2016)
- A correspondence between rooted planar maps and normal planar lambda terms (2015)
- Counting isomorphism classes of $β$-normal linear lambda terms (2015)
- Balanced polymorphism and linear lambda calculus (talk at TYPES 2015) (2015)
- Classical lambda calculus in modern dress (2014)
- Asymptotics and random sampling for BCI and BCK lambda terms (2013)
- Compact Closed Bicategories (2013)
- Groupe Modulaire et Cartes Combinatoires: Génération et Comptage (PhD thesis) (2010)
- A survey of graphical languages for monoidal categories (2009)
- Graphs on Surfaces and Their Applications (2004)
- Linear lambda calculus and PTIME-completeness (2004)
- From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple (2002)
- An update on the four-color theorem (1998)
- Lie algebras and the Four Color Theorem (1997)
- Maps, Hypermaps and Triangle Groups (1994)
- Semantics of lambda-I and of other substructural lambda calculi (1993)
- The geometry of tensor calculus, I (1991)
- Map coloring and the vector cross product (1990)
- Modelling Computations: A 2-Categorical Framework (1987)
- The Lambda Calculus: Its Syntax and Semantics (1984)
- Relating theories of the λ-calculus (1980)
- Theory of Maps on Orientable Surfaces (1978)
- Combinatory Logic, vol. II (1972)
- Applications of Negative Dimensional Tensors (1971)
- Examples of formal semantics (1971)
- On the enumeration of planar maps (1968)
- A Census of Hamiltonian Polygons (1962)