Generating variable names within rewrites

[Kixiron]

I want to generate new/fresh variable names within rewrite rules, but I'm not really sure how to go about it, any tips?

[Bastacyclop]

Hi @Kixiron, consider using something like DeBruijn indices instead of variable names if it makes sense for your language.

Otherwise there is an example of generating fresh names deterministically in the lambda calculus test: https://github.com/egraphs-good/egg/blob/main/tests/lambda.rs#L153

[mwillsey]

As far as generating fresh names, you could just generate them using a global variable or something (behind a mutex), right?

This is my fault, but you shouldn't take the lambda.rs example as the gold standard way to do bindings/substitution. This is still very much an open problem (one @Bastacyclop is acutely aware of), and I'd love to have a better example one day.

The lambda example is just demonstrating that one could do substitution this way, by tracking free variables in the analysis data. You don't have to track free variables if you're willing to make every variable fresh on every substitution.

As far as a "better way", I think the best way right now to handle substitution and binding is to do it "outside" the e-graph. Basically, use an analysis to keep a canonical version of each term (or you could just manually extract), then you can do substitution outside the e-graph and put the results back it.

[Kixiron]

Could you elaborate on "use an analysis to keep a canonical version of each term (or you could just manually extract), then you can do substitution outside the e-graph and put the results back it"?

[mwillsey]

Sure. At a high level, I'm saying that you should do substitution on full terms (probably represented as RecExprs) rather than trying to do that in the e-graph. So say you have an e-class c, and in it is some term that can be reduced/substituted. I'm saying to, instead of plumbing this through with rewrites, just extract a term from c, do the reduction "manually" however youd like, and then add the result back into eclass c.

So to do this you have two options I think. First, is just do it all manually. Every once in a while, extract a term for every e-class in the e-graph, see if it can be reduces, and union the results back into the respective eclass. To do this more 'on-the-fly', you'll want to avoid doing all that extraction, so you can use an analysis that tracks the "best" term in each e-class. It could do this by just comparing costs in merge and taking the smaller one, and on make building a canonical term out of that e-node and the canonical terms of it's children e-classes.

[Kixiron]

I ended up making this which is likely ill-advised and inefficient

struct CaptureAvoid {
    fresh: Var,
    pattern: Pattern,
}

impl CaptureAvoid {
    #[track_caller]
    fn new(fresh: &str, pattern: &str) -> Self {
        let fresh = fresh.parse().unwrap();
        let pattern = pattern.parse().unwrap();

        Self { fresh, pattern }
    }
}

impl Applier<Operator, OperatorAnalyzer> for CaptureAvoid {
    fn apply_one(&self, egraph: &mut EGraph, eclass: Id, subst: &Subst) -> Vec<Id> {
        let mut subst = subst.clone();

        // Create the new symbol and substitute it for the fresh variable
        let sym = Operator::Symbol(unique_symbol());
        subst.insert(self.fresh, egraph.add(sym));

        // Apply the inner pattern with the substituted variable
        self.pattern.apply_one(egraph, eclass, &subst)
    }
}

unique_symbol() just increments an atomic

[Kixiron]

De Bruijn indices were the kicker I think, they work rather well for allowing things to be unified