Theory & Models of Lambda Calculus: Typed and Untyped (Part 3)
summary
Presents a concrete model: represent data as subsets of N and functions as enumeration operators on P(N) so application becomes a lookup-table operation on finite approximations; continuity means continuous functions determined by finite approximations, so the space of representable functions stays countable and encodable as integers. Builds an algebra where lambda abstraction and application correspond to set operations, supports recursion via Y and yields the expected computability results (enumerable operators encode the continuous lambda model).
AI-written summary · about
chapters (7)
- 0:00Start
- 14:10Continuity
- 25:41Finite Sequences
- 26:59One-to-One Correspondence between Finite Sequences
- 30:59Coding Up a Continuous Function
- 53:07Conclusion
- 55:59Turing Machines
related talks
01h 12mTruth about Types
45mPractical Lambda Calculus
01h 52mIsomorphic Reasoning: Counting with Types Part 3
01h 39mIsomorphic Reasoning: Counting with Types Part 1
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
41mWar Time Proofs and Futuristic Programs
49mSemantic Foundations for Probabilistic Programming
02h 28mIsomorphic Reasoning: Counting with Types Part 2