LambdaComb days, 22-24 January 2024

Information

The third meeting of the LambdaComb project will be was held on the Jussieu campus of Sorbonne Université, located at:

4 place jussieu 75005 paris

External participants are welcome, but it would be appreciated if you send us an email to let us know you would like to join in-person / online.

Schedule

The talks and open sessions take place in different buildings on the Jussieu campus — please note the first component of the room numbers below. All times below are in CET. (Lunch is unorganized but there are many places to eat in the area.)

Talk titles and abstracts

---

Lionel Vaux Auclair. The resource calculus and Taylor expansion of lambda-terms. [whiteboard talk]

I will present the resource λ-calculus, which is a multilinear variant of the λ-calculus, and the target language of the Taylor expansion of λ-terms. The combinatorics of resource terms (and especially the combinatorics of permutations of bags of arguments inside resource terms) plays a crucial rôle in the dynamics of the calculus. I will survey results including Ehrhard and Regnier's original study of resource substitution, leveraging not only their version of the resource calculus but also several rigid variants.

---

Peter Hines. Some Open Questions on Coherence for Unbiased Untyped Conjunction. [slides]

This talk is based around the classic theory of coherence for associativity, as described by MacLane / Kelly, and significantly prefigured by Benabou. This is the notion that although operations of interest (such as models of conjunction) may not be precisely associative, they nevertheless are associative up to some ‘well-behaved’ family of natural isomorphisms.

Dealing with such ‘canonical isomorphisms’ may be appear to be a significant complication. In practice, categorical logicians and category theorists simply appeal to MacLane’s ‘strictification procedure’, which demonstrates a categorical equivalence with the ‘strict’ case, where associativity is exact, and all canonical isomorphisms are simply identity arrows.

Doing so is of course entirely valid, but nevertheless raises an interesting point : many structures of interest to both mathematicians and computer scientists may be identified as canonical isomorphisms. We wish to know how their structure arises from the categorical notion of ‘coherence’, and – when appropriate -- how they interact with ‘strictification’.

We concentrate on the untyped, or single-object, case. Here, it has long been folklore that the canonical isomorphisms for associativity form a group – Richard Thompson’s iconic group F. This is equally of interest to pure mathematicians (from its origins as a potential counterexample to a conjecture of J. Von Neumann), theoretical computer scientists (due to its close connection with the minimum rotation distance problem, Ladner’s theorem, and the NPI compexity class, as studied by P. Dehornoy), and practical computer scientists (based on its proposed use as a platform for non-commutative cryptography by V. Shpilrain and A. Ushakov). More recently, it has been shown to have close connections to the ‘special Frobenius algebras’ of categorical quantum mechanics.

The structure of the canonical isomorphisms for coherence becomes yet more interesting when we consider the `unbiased’ setting. The definition of a monoidal tensor has a significant bias towards the binary case – trivially, a tensor is a binary operation. The ‘unbiased’ setting instead requires a family of operations, one of each arity. We thus have a family of functors, indexed by the natural numbers, and related by families of canonical isomorphisms. However, the strict case is identical to MacLane’s definition of a strict monoidal tensor.

Non-strict unbiased tensors are even less well-studied than non-strict associativity, and seemingly for good reasons! T. Leinster demonstrated an equivalence with the usual binary case of MacLane – Kelly, and thus with the strict setting, via MacLane’s strictification procedure.

From a purely categorical point of view, strictification reduces an excessively complicated setting to a significantly simpler one!

Despite this, when we consider the untyped, or monoid-theoretic, case we again see a wide range of structures from pure mathematics, and theoretical & practical computer science. We give a selection of these, with particular emphasis on those relating to number theory & combinatorics, combined with a series of conjectures & open questions on how they relate to the pure category theory.

---

Cameron Calk. Lattices of Paths and Flat Dihomotopy Types. [slides]

---

Gilles Schaeffer. Context-free specifications for solutions of order one catalytic equations. [slides]

---

Luigi Santocanale. Lifting star-autonomous structures. [slides]

---

Noam Zeilberger. The combinatorics of free bifibrations. [slides]

I will motivate the abstract problem of building the free bifibration over a functor of categories, describe a few different-but-related explicit constructions, and discuss some of the rich combinatorics that emerges, including an unexpected equivalence with a category of rooted plane trees introduced by Batanin and Joyal. Joint work with Bryce Clarke and Gabriel Scherer.

---

Alexandros Singh. A novel interpretation of the planar Goulden-Jackson recurrence using the planar λ-calculus. [slides]

---

Mehdi Naima. A lattice on Dyck paths close to the Tamari lattice. [slides]

We introduce a new poset structure on Dyck paths where the covering relation is a particular case of the relation inducing the Tamari lattice. We prove that the transitive closure of this relation endows Dyck paths with a lattice structure. We provide a trivariate generating function counting the number of Dyck paths with respect to the semilength, the numbers of outgoing and incoming edges in the Hasse diagram. We deduce the numbers of coverings, meet and join irreducible elements. We give a generating function for the number of intervals, and we compare this number with the number of intervals in the Tamari lattice. Finally, we present a sequent calculus capturing this new Lattice.

---

Lê Thành Dũng Nguyễn. Complexity of normalization in planar lambda calculus. [talk cancelled, but see the TLLA 2023 abstract for more details]

This talk sketches a proof that whether two untyped planar λ-terms have the same normal form (i.e. are convertible) is P-complete. The proof proceeds by reduction from a variant of the Circuit Value Problem (CVP) that uses straight-line programs. Mairson had already established that convertibility for the linear λ-calculus is P-complete using a reduction from CVP, but his strategy seems to break down in the planar case, and we had to come up with a different idea. Joint work with Anupam Das, Damiano Mazza and Noam Zeilberger.

---