Theory & Models of Lambda Calculus: Typed and Untyped (Part 2)
summary
Claims a concrete semantic model: use the powerset of the integers with enumeration operators to interpret application and abstraction, and show that Church numerals and primitive recursive constructions embed into lambda terms. Demonstrates recursion via the Y combinator, encodes all recursively enumerable functions to prove undecidability of combinator equality, and constructs types as quotients of subspaces connecting to categorical semantics. Slides and worked examples live at the linked GitHub.
AI-written summary · about
chapters (7)
- 0:00Start
- 1:20Primitive Recursion
- 2:05Composition of Functions
- 6:57Partial Recursive Function
- 19:06Combinators
- 22:30The Clash between Free and Bound Variables
- 27:00Categorical Semantics
related talks
45mPractical Lambda Calculus
01h 12mTruth about Types
41mWar Time Proofs and Futuristic Programs
01h 52mIsomorphic Reasoning: Counting with Types Part 3
49mSemantic Foundations for Probabilistic Programming
01h 20mA Practical Introduction to Haskell GADTs
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
02h 28mIsomorphic Reasoning: Counting with Types Part 2