Lambda Calculus Then and Now

The speaker expresses sadness over not having the opportunity to collaborate more with Michael Rabin, a Turing Award recipient, who is not present at the event. They invite the audience to extend their warm greetings to Rabin at an upcoming Turing conference. The speaker also reflects on their academic career and their regret over not collaborating with Rabin for a longer period. The main topic of the talk is introduced: a historical overview of the development of the lambda calculus, which the speaker describes as having been effectively 'recycled' every decade due to its foundational nature. The speaker invites feedback on a timeline and bibliography they have prepared, which are available on the ACM site, to ensure a fair representation of the developments over a long period.

The speaker delves into the history of lambda calculus, highlighting the contributions of Alonzo Church and Alan Turing. They discuss how Church and Turing independently applied ideas about logic and computability to demonstrate the undecidability of first-order logic. The speaker also mentions the influence of Kurt Gödel's work and the role of Max Newman in Turing's career. The lambda calculus is described as a method for explicit definitions of functions, initially developed by Church to avoid the Russell paradox. The speaker notes the simplicity of the lambda calculus and its ability to represent functions, arguments, and values in an untyped system. The talk also touches on the lambda calculus's connection to the Church-Turing thesis, which equates the lambda calculus with Turing machines in terms of their computational capabilities.

The speaker continues to explore the lambda calculus, focusing on its role as a model for computability. They discuss the early work of Church and Turing, and how the lambda calculus was initially part of a larger logical system. The speaker explains how Church's students found inconsistencies in this system, leading to the lambda calculus being separated from the rest. The speaker then describes a model for the lambda calculus using sets of integers, explaining how this model can represent functions and data structures. They also touch on the lambda calculus's ability to simulate data structures and its connection to the Church-Turing thesis, emphasizing the importance of understanding the lambda calculus in the context of computability.

The speaker discusses the lambda calculus's ability to represent data structures and its implications for computability. They explain how lambda expressions can act as stored computer programs, capable of being both data structures and operators. The speaker highlights Church's approach to interpreting integers using iterators and how this can be represented in lambda calculus. They also mention Turing's realization of the lambda calculus's potential for self-replication through the fixed-point theorem. The speaker emphasizes the importance of understanding the lambda calculus in the context of data structures and its role in the Church-Turing thesis, which posits that the lambda calculus can simulate any form of computation.

The speaker addresses the Church-Turing thesis and the decision problem, focusing on the question of whether first-order logic is recursively enumerable or decidable. They discuss Church's approach, which was based on Gödel's work, and Turing's solution, which involved the universal Turing machine. The speaker explains how the Church-Turing thesis was ultimately accepted when it was shown that all these models could be made equivalent. They also touch on the work of Emily Post, who independently thought of the idea of a Turing machine but did not put it in the same context. The speaker concludes by highlighting the importance of the Church-Turing thesis in understanding the limits of computability and the role of the lambda calculus in this discussion.

The speaker provides a timeline of the evolution of lambda calculus and its influence on computing. They mention the introduction of simple type theory by Church and its impact on the work of Leon Henkin, who developed new completeness proofs. The speaker also discusses the development of recursive function theory by Kleene and the influence of category theory on the lambda calculus. They highlight the importance of the 1950s, when computers and computer languages began to emerge, and the 1960s, which saw significant developments in category theory. The speaker concludes by noting the ongoing influence of lambda calculus in the development of new computing languages and its potential future applications in areas such as automated theorem proving and proof assistance.

The speaker concludes the talk by discussing the future of lambda calculus, highlighting its potential connections with other models, particularly topology and homotopy theory. They mention the work of Auskey at the Institute for Advanced Study, who has explored the idea of connecting lambda calculus with these mathematical fields. The speaker explains how the rules for homotopy theory align with the concept of intentional identity, which is concerned with the way things are defined rather than their extensional properties. They conclude by emphasizing the ongoing development and potential future applications of lambda calculus, inviting the audience to consider its role in the broader context of mathematical and computational theory.