Theory & Models of Lambda Calculus: Typed and Untyped (Part 3)
summary
Claims a concrete model of lambda calculus built on the powerset of the integers, using enumeration operators as the actual implementation of application and abstraction. Tools are point-set topology (finite-set basis, open sets as unions) and continuity conditions that force semantic functions to be continuous implies monotone, yielding fixed points and recursion. Shows how types arise as quotients/subspaces and how the model composes into categorical semantics.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:10Topology
- 5:00Intervals
- 5:44Functions
- 6:15Infinite Many
- 7:48Open Sets
- 13:18Encoding
- 20:00Epsilon Delta
- 22:03Neighborhood
- 25:28PZero Spacers
- 31:52Cardinality
- 36:13who will solve
- 41:45who will describe an open set
- 48:19continuous functions
related talks
01h 12mTruth about Types
45mPractical Lambda Calculus
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
41mWar Time Proofs and Futuristic Programs
01h 01mCategory Theory - Part 2 of 6
43mPropositions as Types
01h 20mA Practical Introduction to Haskell GADTs
57mPropositions as Types