Ensure alpha conversion always runs when a new variable is bound#414
Ensure alpha conversion always runs when a new variable is bound#414
Conversation
|
|
||
| # we also make the old cons cache_key point to the new mangled value. | ||
| # this guarantees that alpha-conversion only runs once for this expression. | ||
| cls._cons_cache[cache_key] = result |
There was a problem hiding this comment.
This line ensures that _alpha_mangle does not break cons-hashing.
|
The CI failures are |
Update: I believe I have fixed this by forcing alpha-renaming substitution to run under |
|
This recent paper seems quite relevant, although it solves a slightly different problem. |
This PR fixes a longstanding alpha-conversion edge case by guaranteeing that newly bound variables are always alpha-renamed, which is currently not the case due to the way alpha-conversion interacts with cons-hashing. For context, this issue turned out to be the root cause of some strange, difficult-to-debug errors that came up when I tested
funsor.adjointwithfunsor.sum_product.modified_partial_sum_product. I imagine @ordabayevy will run into this at some point, so think of this PR as preemptive unblocking.Recall that alpha conversion in Funsor is implemented with name-mangling of subexpressions in
reflect: whenever a variable is newly bound in a Funsor expression, we append to its name a unique suffix of the formf"__BOUND_{identifier}".However, to ensure that expressions that bind variables are cons-hashed, we have to avoid mangling names twice. This is currently achieved by only mangling bound variables whose names do not already contain a
__BOUND_suffix, a heuristic that can sometimes break down when subexpressions containing mangled inputs are temporarily exposed for further processing. This PR switches to always mangling bound variables and should guarantee that alpha-conversion always behaves as expected.Tested:
mastertest_alpha_conversion.pyand implicitly in any test that compares identities of expressions with bound variables (x1 is x2)