Iowa Type Theory Commute

Lambda graphs with duplicators and start of Lamping's abstract algorithm


Listen Later

In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables.  I also start discussing the beginning of Lampings' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy 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