Theory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5
summary
Part 3 lays out concrete constructions and results: lambda abstraction is realized as the largest lookup table that reproduces a continuous operator; pure lambda terms denote computable enumeration operators (recursively enumerable lookup tables); a universal enumeration V and finite resource approximations get built; least fixed points are shown to exist and be computable, via self-application and well‑founded griddle numbering; connections to enumeration degrees, closure operators and classical recursion proofs are given.
AI-written summary · about
chapters (13)
- 0:00Start
- 2:31Open Sets Are Unions of Neighborhoods
- 3:56Continuity
- 4:32Example of a Discontinuous Function
- 5:28Example of a Non Monotone Function
- 12:11Candice Theorem
- 12:35Enumeration Operators
- 20:26Computable Enumeration Operators
- 25:56Primitive Recursion
- 45:46Limiting Girdle Numbers
- 51:18Logical Deduction
- 51:59Closure Operator
- 54:48Lattice Theory
related talks
41mInfinite Lambda Calculus
44mSome History of Functional Programming Languages
06mLightning Talk: The Lambda Calculus in C++ Lambdas
01h 04mThe Leibniz Library and Applied Propositions as Types
41mWar Time Proofs and Futuristic Programs
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
39mA Little Taste of Dependent Types
01h 00mProspects for Computer Formalization of Infinite-Dimensional Category Theory