A Calculus of Delayed Reductions
summary
Introduce the Calculus of Delayed Reductions (CDR) that tweaks CBPV: forcing only variables, thunking only non-forced computations, and a new substitution that immediately strips force/thunk pairs. CDR models single-step CBN and CBV reductions (mapping preserves reduction and types), removes the U/unblocking rule, and gives a one-to-one interpretation into lambdabar-mu-mutilde via a CK-style abstract machine. The implementation succeeds at simulating both strategies without the Levy explosion.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:28Calculus of delayed reductions
- 2:54Lambda calculus refresher
- 4:19Call by push value syntax
- 6:24Types in call by push value
- 8:14Interpreting call by value in call by push value
- 10:03Interpreting call by name in call by push value
- 12:13Calculus of delayed reductions
- 13:38Call by value and call by name in CDR
- 15:32Lambda bar μ̄ calculus overview
- 17:41Reduction strategies in Λbμ̄
- 19:51Type assignment in Λbμ̄
- 20:32Interpreting CDR in Lambda bar mu mutil
- 22:44CK machine and Λbμ̄
- 25:55Conclusion
- 27:27Q&A
related talks
40mAn Introduction to Combinator Compilers and Graph Reduction Machines
17mNotions of Stack-manipulating Computation and Relative Monads
27mA General Fine-Grained Reduction Theory for Effect Handlers
01h 00mTheory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5
45mA categorical view of computational effects
43mReducers
01h 21mNon-local compiler transformations in the presence of dynamic dispatch
21mλ-Calculus: A Brief History of Functional Programming