LambdaComb kickoff meeting, April 11th, 2022

Information

The kickoff meeting of the LambdaComb project was held as a hybrid event at LIX, located in the Alan Turing building of Ecole Polytechnique.

Participants included (in person) Adrien Ragot, Alexandros Singh, Bryce Clarke, Farzad Jafarrahmani, Flavien Breuvart, Gilles Schaeffer, Luigi Santocanale, Marie Albenque, Noam Zeilberger, Olivier Bodini, Samuel Mimram, Samuele Giraudo, Stefano Guerrini, and Wenjie Fang, together with (online) Cedric DeLacroix, Erkan Narmanli, Giulio Manzonetto, Katarzyna Grygiel, Lê Thành Dũng Nguyễn, Maciej Bendkowski, Marek Zaionc, and Sam Speight.

Schedule

All talks took place in Salle Henri Poincaré located on the ground floor of LIX. All times are CEST.

Talk titles and abstracts

---

Noam Zeilberger. A quick introduction to species, operads, and closed multicategories [slides]

Species and operads are mathematical structures that may be defined concisely in categorical language, and which arise naturally in many different settings including combinatorics, proof theory, and lambda calculus. In this introductory talk I will give a basic overview of species and operads (in symmetric, non-symmetric, and colored form), emphasizing free constructions of species and operads, and their relation to functional-differential equations in combinatorics. I will also briefly discuss closed multicategories. The aim will be to motivate the study of lambda calculus from this categorical perspective, and point out some natural questions about enumeration of typed lambda terms.

---

Olivier Bodini. A quick introduction to analytic combinatorics [whiteboard]

We recall here the basics of the symbolic method and of the analytic combinatorics. In particular, we show how linear lambda terms can be described with differential operators (called pointing operators).

---

Alexandros Singh. A lower bound on the average length of reduction in linear λ-terms [slides]

Extending our recent work on the distribution of parameters in trivalent maps and linear lambda-terms, we explore the behaviour of beta-reduction in random closed linear lambda-terms. The first part of this talk focuses on the enumeration of redices in such terms. We then shift our attention to the analysis of three specific families of redices: those whose reduction results in a term having the same number of redices as the original. Combining the results of these two parts, we obtain a lower bound on the number of steps required to reduce a random closed linear lambda-term to its beta-normal form. This talk is based on a combination of results drawn from joint work(s) by (subsets of) Bodini, Gittenberger, Singh, Wallner, Zeilberger.

---

Wenjie Fang. Bijections between planar maps and planar linear normal λ-terms with connectivity condition [slides]

The enumeration of linear λ-terms has attracted quite some attention recently, partly due to their link to combinatorial maps. Zeilberger and Giorgetti (2015) gave a recursive bijection between planar linear normal λ-terms and planar maps, which, when restricted to 2-connected λ-terms (i.e., without closed sub-terms), leads to bridgeless planar maps. Inspired by this restriction, Zeilberger and Reed (2019) conjectured that 3-connected planar linear normal λ-terms have the same counting formula as bipartite planar maps. In this talk, we present a proof of this conjecture by giving a direct bijection between these two families. Furthermore, using a similar approach, we give a direct bijection between planar linear normal λ-terms and planar maps, whose restriction to 2-connected λ-terms leads to loopless planar maps. We also explore enumerative consequences of the two bijections.

---

Samuel Mimram. A cartesian bicategory of polynomial functors in homotopy type theory [slides]

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting of a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.

---

Lê Thành Dũng Nguyễn. Proof nets and mainstream graph theory [slides]

A connection between the "homemade" combinatorics of proof nets — a graphical representation of linear logic proofs — and the classical topic of perfect matchings was discovered in the 1990s by Retoré. After introducing proof nets, I will explain how this connection can be leveraged to:

• rebuild the theory of proof nets by reducing the difficult "sequentialization theorem" to Kotzig's theorem (1959) on matchings;
• rephrase an obscure theorem on proof nets into a nice elementary statement on perfect matchings;
• apply the vast literature on graph algorithms to get new complexity results on proof nets.

As an unexpected side effect of this last item, Lutz Straßburger and I refuted a 20-year-old conjecture in the proof theory of linear logic, namely the equivalence between pomset logic (based on proof nets) and system BV (based on deep inference).

---