Allow bubbling args over their own lambda to find more inventions

[theoxo]

Lol I just realized I never pushed this. All that hard work for naught (almost). Luckily I didn't accidentally rm -rf / this weekend : ------- )

Matt: We should address the TODOs you wrote down on your phone before we merge this.

[mlb2251]

good call! The things were:

• why was the assertion about applam.len() == 1 firing, like where did that second applam with the same invention come from exactly?
• is it really true that the same set of inventions works on a tree after you shift the free variables (and does the change that this pull request makes affect that at all?)
• (non essential) can we actually not build up applams in the downshift worklist loop and instead just do best_inventions? We suspect those applams aren't being used for anything.

[mlb2251]

why was the assertion about applam.len() == 1 firing, like where did that second applam with the same invention come from exactly?

That assert was just there to ensure I could get away with applam[0] instead of min(applam) because prior to this commit we never had two different applams that have the same invention for a single original node. But now we do, which isn't an issue it just means that we need to be careful because there's not a one to one mapping between inventions and applams at each node.

An example of how this new pull request allows for a node to yield two different applams that have the same invention is: given the original node (lam (e $0)) where e is any expression, there are two ways to get the invention (lam (#0 $0)). We can either directly abstract e and get this invention with the argument e, or we can abstract (e $0) to get the invention (lam #0) then bubble this over the lambda which by this new pull request is allowed and turns the body into (lam (#0 $0)) and the arg into (lam (e $0))

A downside is this could increase the number of applams, potentially by a factor of two wherever this happens. I see a 30% slowdown (11s -> 8s) however this might be necessary for the gain of what the PR introduces. I spent a bit trying to filter out obvious cases like banning the (lam (e $0)) situation in particular, but it didn't help the speed (and it resulted in less compression so it seems this case is important). Could have been my mistake in implementing a fix, but I think we should just leave it as is for now since it seems likely to be a necessary slowdown.

[mlb2251]

(non essential) can we actually not build up applams in the downshift worklist loop and instead just do best_inventions? We suspect those applams aren't being used for anything.

Moved to #2

[mlb2251]

is it really true that the same set of inventions works on a tree after you shift the free variables (and does the change that this pull request makes affect that at all?)

yes. Same inventions and same costs.

• Intuition: we're talking about shifting free variables to other free variables.
  • Since they're free vars, we dont need to worry about which lambda theyre bound to or shifting affecitng anything like that - the lambdas are way above us out of reach. So basically we're opaque to what the specific index is, we just know it's something out of reach. And theres no semantics associated with indices other than that so it's pretty meaningless.
  • And since theyre free variables we have to abstract them like they cant show up in the body of the invention bc that wouldnt be a valid invention. So they must be in the arguments to the invention.
  • And its totally fine to swap out one argument for another that never changes whether the invention is allowed.
• so yes the same valid inventions apply since by definition a valid invention has no free vars. Shifting could change something about the applams but we arent doing anything with applams here so thats fine. We're only copying over the inventions that apply.