To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-bound variables are used at most once) plus structural recursion does not enforce termination, even if you restrict the recursor so that the function to be iterated is closed when you reduce ("closed at reduction"). You have to restrict it so that recursion terms are disallowed entirely unless the function to be iterated is closed ("closed at cons...
All content for Iowa Type Theory Commute is the property of Aaron Stump and is served directly from their servers
with no modification, redirects, or rehosting. The podcast is not affiliated with or endorsed by Podjoint in any way.
To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-bound variables are used at most once) plus structural recursion does not enforce termination, even if you restrict the recursor so that the function to be iterated is closed when you reduce ("closed at reduction"). You have to restrict it so that recursion terms are disallowed entirely unless the function to be iterated is closed ("closed at cons...
In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating language, upon which one may then erect as exotic a type system as one wishes. By enforcing termination already for the untyped language, we no longer have to make the type system do the heavy work of enforcing termination.
Iowa Type Theory Commute
To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-bound variables are used at most once) plus structural recursion does not enforce termination, even if you restrict the recursor so that the function to be iterated is closed when you reduce ("closed at reduction"). You have to restrict it so that recursion terms are disallowed entirely unless the function to be iterated is closed ("closed at cons...
