Iowa Type Theory Commute

Duplicating redexes as the central problem of optimal reduction


Listen Later

We discussed last time how with a graph-sharing implementation of untyped lambda calculus, it can happen that you are forced to break sharing and copy a lambda abstraction.  We discuss in this episode the central issue with doing that, namely copying redexes and copying applications which could turn into redexes following other beta reductions.  The high-level idea of the proposed solution is also discussed, namely lazy graph duplication.

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

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

16 ratings