Iowa Type Theory Commute

Schematic Affine Recursion, Oh My!


Listen Later

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 construction").  But this prevents higher-order functions like map, which need to repeat a computation involving a variable f to be mapped over the elements of a list.  The solution is to allow schematic definition of terms, using schema variables ranging over closed terms.

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

19 ratings


More shows like Iowa Type Theory Commute

View all
The Changelog: Software Development, Open Source by Changelog Media

The Changelog: Software Development, Open Source

288 Listeners

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas by Sean Carroll | Wondery

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas

4,196 Listeners

Interesting Times with Ross Douthat by New York Times Opinion

Interesting Times with Ross Douthat

7,215 Listeners

Tech Won't Save Us by Paris Marx

Tech Won't Save Us

580 Listeners

Dwarkesh Podcast by Dwarkesh Patel

Dwarkesh Podcast

531 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

16,221 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

14 Listeners

Software Unscripted by Richard Feldman

Software Unscripted

29 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

67 Listeners