Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Introduction to the Finite Developments Theorem
•
Aaron Stump
•
Season 6
•
Episode 6
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.