Podcasts Technology Iowa Type Theory Commute Lamping's abstract algorithm

Lamping's abstract algorithm

Published: July 25, 2020, 8 p.m.

b'

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

'