Theory & Models of Lambda Calculus: Typed and Untyped (Part 5)
summary
Model uses the powerset of N with enumeration operators to model application and abstraction; closure operators correspond to subspaces and fixed points equal their ranges. Concrete constructions: pairing via even/odd encoding, product and arrow types as C × D and C → D, and iteration of enumeration operators to generate closures. Claim: a nontrivial universal closure operator exists as a Y‑fixed point giving a subspace that satisfies all lambda‑calculus axioms. Extensions: partial equivalence relations for quotients and dependent product types.
AI-written summary · about
chapters (11)
- 0:00Start
- 5:14Lambda Abstraction
- 9:15Category Theory
- 21:17Closure Operators
- 26:30Isomorphism
- 30:24Universal Closure Operator
- 39:12Construction of the Real Line
- 42:22Group Theory
- 48:06Principle of Quantifiers in Predicate Calculus
- 50:18Partial Equivalence Relations
- 58:38Dependent Product
related talks
01h 12mTruth about Types
01h 01mCategory Theory - Part 2 of 6
45mPractical Lambda Calculus
01h 39mIsomorphic Reasoning: Counting with Types Part 1
01h 01mCategory Theory - Part 1 of 6
01h 52mIsomorphic Reasoning: Counting with Types Part 3
01h 00mCategory Theory - Part 5 of 6
41mWar Time Proofs and Futuristic Programs