Introducing free variables with rewrite rules (e.g. tuning parameters)

[Bastacyclop]

Hi!
I would like to define rewrite rules that introduce free variables on their right-hand-side. In particular, I would like to introduce tunable parameters like m in the following rule, where n.t is the type of an array of n elements of type t:

(a : n.t) => join(split(m, a) : (n/m).m.t)

How would one do this efficiently in egg? If we create a fresh variable on every rule application, we will create many equivalent tuning parameters, and overload the e-graph. This is also a problem for bound variables, but for those it is possible to use DeBruijn indices to mitigate the problem. What is a reasonable solution for free variables?

[mwillsey]

Hmm. This is tricky. You could try to use the e-class id (or some other data of from the substitution) to generate a kinda deterministic name for the new variable.

[Bastacyclop]

Right, combined with some smarter rewrite rule scheduler to avoid triggering this rule too often, it might be a good enough start.

[pavpanchekha]

Here's what we (actually just @oflatt) did in our attempt at eggifying (scrambling?) our series expansion algorithm. Think about what the tunable parameter depends on, on your left-hand side. I have no idea in your example, but let's assume the choice of m depends on a, n, and also t. Then define a function a-free-parameter with three arguments, and instead of m write (a-free-parameter a n t). So your example was this (transcribing with S-expression syntax so you can follow what I'm doing:

(typeof a (vector t n))
=>
(join (typeof (split m a) (vector (vector t m) (/ n m))))

and it turns into this:

(typeof a (vector t n))
=>
(join (typeof (split (a-free-parameter a n t)) (vector (vector t (a-free-parameter a n t)) (/ n (a-free-parameter a n t)))))

Obviously do this with code, you'll go crazy doing this replacement by hand. If you're doing extraction, you can give this function a cost of 1 no matter its arguments, so it is functionally a constant. This will unify and deduplicate correctly, I think.

[Bastacyclop]

Interesting trick! Sadly I don't think that the choice of m depends on the left-hand-side in this case, unless with the restriction that a given array can only be split in a single way in any context (same a implies same m). In the general case, you might want to split a with different values of m, if a is used multiple times in different contexts.

[pavpanchekha]

You can still have it depend on a in that case. If you want a truly fresh variable then I'd use a dynamic rewrite that introduces an actually new variable—but then of course there will be no sharing.