Zulip Chat Archive

Stream: lean4 dev

Topic: publications on locally nameless optimizations

Mathis Bouverot-Dupuis (Jan 20 2025 at 22:57):

Hello ! In the definition of Expr, I see that some information about free variables/metavariables/de Bruijn indices/etc is cached (for optimization purposes) : https://github.com/leanprover/lean4/blob/c07f64a6212247ef789d4cef39e237b4a4b61696/src/Lean/Expr.lean#L130

Does someone know if this optimization is documented in any published form ? In a Lean paper, or even in a paper unrelated to Lean ?

Henrik Böving (Jan 20 2025 at 23:00):

I don't know of any Lean related paper. But it's not particularly difficult to implement so I wouldn't be surprised if there is not really a mention of doing this thing in academia in general given the pressure for novelty.

Henrik Böving (Jan 20 2025 at 23:05):

Is there a particular reason you are looking for a paper to cite?

Mathis Bouverot-Dupuis (Jan 20 2025 at 23:14):

Yes I would assume this has been mentioned in some paper, but I don't know which...

Mathis Bouverot-Dupuis (Jan 20 2025 at 23:16):

I'm referring to this optimization in an upcoming paper and I would like to point readers to a paper to avoid having to go into too much detail

Mathis Bouverot-Dupuis (Jan 20 2025 at 23:17):

Surely someone has benchmarked the performance impact of this stuff :pray:

Last updated: May 02 2025 at 03:31 UTC