Efficient Evaluation with Controlled Definition Unfolding
summary
Proposes an evaluator-for-elaboration that preserves definition unfoldings by representing top-level names as delayed top-level unfolding nodes in the semantic domain, evaluating into closures and neutrals and only forcing unfoldings when needed. Uses normalization-by-evaluation with quote/eval interleaving, keeps for each term a pair of least-and-most-unfolded values so unification and conversion can choose minimal expansion, and applies immediate light inlining/let-motion after meta solutions. Cuts classic exponential 2^n blowups to linear and avoids common quadratic elaboration cases while keeping user-facing output readable.
AI-written summary · about
chapters (9)
- 0:00Controlled definition unfolding
- 0:41Performance in unfolding
- 4:58Core terms and semantics
- 13:25Interleaving evaluation
- 17:23Unification with value pairs
- 19:10Meta solutions for elaboration
- 20:56Optimizing elaboration output
- 23:04Record field sharing issues
- 25:10Q&A
related talks
35mPractical Normalization by Evaluation for EDSLs
01h 01mA partial history of partial evaluation
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
15mEquality Saturation Theory Exploration à la Carte
28mEta conversion for the unit type (is still not that simple)
17mAutomated Expected Value Analysis of Recursive Programs
29mObserving Definitional Equality