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.

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 ${𝑌}_{𝑛}$.

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.

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.