Theory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5

on YouTube ↗01h 02m

" summary

Constructs models inside P(N) using enumeration operators and least fixed points to show that closure operators form a cartesian closed category and that computable continuous maps arise from those operators. Encodes products by evens/odds pairing, embeds countably based T0 spaces and quotients (reals via Cauchy sequences), and builds a nontrivial closure operator D with the property D ≅ D→D (homeomorphic to its own function space), giving a concrete consistency/model result for untyped lambda calculus.

AI-written summary · about

" chapters (7)

1. 0:00Start
2. 33:26Enumeration Operators
3. 37:21Quotients of Subspaces
4. 43:07A Partial Equivalence Relation
5. 48:25Closure Operators
6. 54:34Quantifier Manipulation
7. 1:00:12Products and Sums

" related talks

• 41mWar Time Proofs and Futuristic ProgramsValeria de Paiva · Strange Loop 2023
• 41mInfinite Lambda CalculusEinar W. Høst, Jonas Winje · Code Mesh 2017
• 01h 00mProspects for Computer Formalization of Infinite-Dimensional Category TheoryEmily Riehl · CPP 2025
• 04mSeparated and Shared Effects in Higher-Order LanguagesJustin Hsu · LAFI 2023
• 52mA Categorical View of Adjunctions, Free Constructions, and Profunctor OpticsEmily Pillmore · LambdaConf 2019
• 44mSome History of Functional Programming LanguagesDavid Turner · Lambda Days 2017
• 06mLightning Talk: The Lambda Calculus in C++ LambdasDavid Stone · CppCon 2022
• 39mA Little Taste of Dependent TypesDavid Christiansen · Strange Loop 2018