Start / Iowa Type Theory Commute / Duplicating redexes as the central problem of optimal reduction

Duplicating redexes as the central problem of optimal reduction

16 min • 21 juni 2020

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.