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

17 ratings


More shows like Iowa Type Theory Commute

View all
Software Engineering Radio by se-radio@computer.org

Software Engineering Radio

273 Listeners

This American Life by This American Life

This American Life

90,978 Listeners

Planet Money by NPR

Planet Money

30,773 Listeners

CppCast by Timur Doumler & Phil Nash

CppCast

106 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,131 Listeners

ADSP: Algorithms + Data Structures = Programs by Conor Hoekstra, Bryce Adelstein Lelbach & Ben Deane

ADSP: Algorithms + Data Structures = Programs

36 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

16,002 Listeners

The Array Cast by The Array Cast

The Array Cast

35 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

13 Listeners

The Weekly Show with Jon Stewart by Comedy Central

The Weekly Show with Jon Stewart

10,745 Listeners

The Rest Is Politics by Goalhanger

The Rest Is Politics

3,324 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

59 Listeners

Developer Voices by Kris Jenkins

Developer Voices

30 Listeners