Zulip Chat Archive

Stream: general

Topic: Let binding efficiency


Seul Baek (Dec 24 2018 at 00:04):

If a term foo appears multiple times in a definition in such a way that each occurrence of it will have to be normalized, does the definition become more efficiently computable by using let x := foo in in the beginning? The assumption is that x will be structured in a way that forces (some) normalization with the let binding (e.g., if foo : A × B, then let (a,b) := foo).

Mario Carneiro (Dec 24 2018 at 00:08):

yes, although lean does that sometimes on its own, during the common subexpression elimination pass

Mario Carneiro (Dec 24 2018 at 00:08):

do you mean in the VM or the kernel?

Mario Carneiro (Dec 24 2018 at 00:09):

Note that let (a,b) := foo is not a let binding at all, it is just notation for a recursor

Seul Baek (Dec 24 2018 at 00:10):

I meant the kernel, although I'd be curious about the VM as well.

Mario Carneiro (Dec 24 2018 at 00:11):

In the kernel, I am not positive but I would guess that it depends on how shared the expression object is in memory

Mario Carneiro (Dec 24 2018 at 00:11):

using a let binding like that is a good way to make sure that the same expression object is used in each place

Mario Carneiro (Dec 24 2018 at 00:12):

but there will be some overhead with unfolding it

Mario Carneiro (Dec 24 2018 at 00:12):

The kernel caches the whnf operation, so it won't need to calculate it many times if it is asked for multiple times

Mario Carneiro (Dec 24 2018 at 00:13):

but I'm not sure whether the same expression in different contexts can cause a problem (since this might mean renaming vars and unsharing)

Seul Baek (Dec 24 2018 at 00:17):

The main downside I'm experiencing with let is that it doesn't play nice with the simplifier when I have to prove properties about definitions which include it (_match_1 all over the place) and requires extra definitional lemmas for unfolding. So I was wondering if there are reasons to use it other than its concision.

Seul Baek (Dec 24 2018 at 00:20):

If let (a,b) := foo is not a let binding, is there something else I can do to normalize foo and bind it to fresh term(s)?

Mario Carneiro (Dec 24 2018 at 00:33):

like I said, it's just a recursor. If you don't like the _match_1 stuff, you can use tactics instead to construct the term, which don't leave this junk in the term

Mario Carneiro (Dec 24 2018 at 00:33):

i.e. by cases foo with a b; exact

Mario Carneiro (Dec 24 2018 at 00:33):

it's equivalent to writing prod.rec explicitly in the term

Seul Baek (Dec 24 2018 at 00:51):

I see. Thanks!


Last updated: Aug 03 2023 at 10:10 UTC