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

Formale Metadaten

Titel
Untyped Linear Lambda Calculus and the Combinatorics of 3-valent Graphs
Serientitel
Anzahl der Teile
15
Autor
Mitwirkende
Lizenz
CC-Namensnennung 3.0 Unported:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
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.