Theory and Models of Lambda Calculus Untyped and Typed - Part 2 of 5
summary
Concrete claims and artifacts: an algorithm that converts lambda abstractions into S and K combinators, worked examples and a Mathematica notebook with tests, demonstration that self‑application produces a fixed‑point via self‑application giving recursion, exploration of normal forms and the proof that the set of lambda expressions with normal forms is recursively enumerable but not recursive, and a semantic construction using the power set of the integers model with topology and continuous (enumeration) operators.
AI-written summary · about
chapters (14)
- 0:00Start
- 4:35Ada Rule
- 8:54Reorder the Variables
- 17:13Recursion by Search
- 24:27From Combinators to Lambda Calculus
- 24:57Alpha Rule
- 25:17Beta Rule
- 26:06The Ada Rule
- 32:09Prefix Operators and Postfix Operators
- 33:05Application as a Prefix Operator
- 35:36Modeling the Lambda Calculus
- 48:59Primitive Recursion
- 52:51The Product Apology
- 55:05Definitions of Continuity
related talks
34mAn introduction to Lambda Calculus
36mAbstract Machines for Good
48mIt’s birds all the way down: Fun Introduction to Lambda Calculus
30mLambda Calculus: The Origins of Functional Programming
21mλ-Calculus: A Brief History of Functional Programming
42mPractical Lambda Calculus
37mLearn You Some Lambda Calculus
53mIntroduction to Intuitionistic Type Theory