Orateur
Description
The lambda calculus was invented by Church in the late 1920s, as part of an ambitious project to build a foundation for mathematics around the concept of function. Although his original system turned out to be logically inconsistent, Church was able to extract from it two separate usable systems, with a typed calculus for logic and an untyped calculus for pure computation. Through the work of Lawvere and Lambek in the 1970s, a close connection was established between typed lambda calculus and the theory of cartesian closed categories (cccs). Around the same time, Dana Scott discovered the first non-trivial mathematical models of untyped lambda calculus, which he later axiomatized using the notion of reflexive object in a ccc. After Jean-Yves Girard’s formulation of Linear Logic in the 1980s, some renewed attention was paid to the linear subsystem of lambda calculus, which has similar relationships with the theory of symmetric monoidal closed categories, in
particular untyped linear lambda calculus may be modelled as the endomorphism operad of a reflexive object in a symmetric closed multicategory. In the talk, I will analyze a surprising bijection originally presented by Bodini, Gardy, and Jacquot (2013) between untyped linear lambda terms and rooted 3-valent maps (= 3-valent graphs embedded on oriented surfaces). Rather than being a mere coincidence, this bijection appears to be part of a deeper connection between the combinatorics of lambda calculus and the theory of map enumeration initiated by Tutte in the 1960s, as witnessed by a host of correspondences between different natural subsystems of linear lambda calculus and different natural families of maps.
