Podcasts Technology Iowa Type Theory Commute Duplicating redexes as the central problem of optimal reduction

Duplicating redexes as the central problem of optimal reduction

Published: June 21, 2020, 3 a.m.

b'

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.\\xa0 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.\\xa0 The high-level idea of the proposed solution is also discussed, namely lazy graph duplication.

'