Iowa Type Theory Commute

Lamping's abstract algorithm


Listen Later

The simplified version of Lamping's algorithm for optimal beta-reduction is discussed.  We have duplicators which eat their way through lambda graphs.  When copying a lambda abstraction, we send one duplicator down the variable port, and another down the body port.  When they meet, they cancel each other and the duplication is done.  But duplication can get paused waiting for a value to come in on a wire from outside the lambda abstraction.  This can lead to a situation where some other duplication needs to duplicate a lambda graph containing frozen duplicators.  Then we have to decide, when two duplicators meet, should they cancel each other (signalling the end of a duplication on one level), or should one duplicate the duplicators (for an outer duplication of some lambda graph containing frozen duplicators).  The abstract algorithm leaves this choice undetermined.  The hairy versions of the algorithm add complex additional machinery to keep track of these levels of duplication to resolve that nondeterminism.

...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

289 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,175 Listeners

Interesting Times with Ross Douthat by New York Times Opinion

Interesting Times with Ross Douthat

7,230 Listeners

Tech Won't Save Us by Paris Marx

Tech Won't Save Us

571 Listeners

Dwarkesh Podcast by Dwarkesh Patel

Dwarkesh Podcast

508 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

15,984 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

13 Listeners

Software Unscripted by Richard Feldman

Software Unscripted

29 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

62 Listeners