We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Untyped Linear Lambda Calculus and the Combinatorics of 3-valent Graphs

Formal Metadata

Title
Untyped Linear Lambda Calculus and the Combinatorics of 3-valent Graphs
Title of Series
Number of Parts
15
Author
Contributors
License
CC Attribution 3.0 Unported:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
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.