Zulip Chat Archive

Stream: new members

Topic: e-graphs


view this post on Zulip Bryan Gin-ge Chen (Mar 21 2021 at 15:52):

Welcome! I guess you're talking about the paper "Efficient E-matching for SMT Solvers"? I'm probably not the right person to try to answer your question but maybe @Mario Carneiro or @Gabriel Ebner can help.

view this post on Zulip Mario Carneiro (Mar 21 2021 at 15:53):

What are e-graphs? Maybe I know them by another name, but that doesn't ring a bell

view this post on Zulip Miguel Raz Guzmán Macedo (Mar 27 2021 at 20:07):

Chiming here - would also be interested in knowing about egraph use in Lean. I take it the pattern matcher for tactics got an algorithmkc overhaul from Lean 3

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 11 2021 at 20:33):

Bump. Does the synbolic rewriter in rfl use a particular algorithm for egraphs?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 11 2021 at 20:33):

If one wanted to add tactics similar to RUBI, would that be by overloading simp?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 11 2021 at 20:37):

https://rulebasedintegration.org/

view this post on Zulip Eric Wieser (Apr 11 2021 at 21:22):

What do you mean by the symbolic rewriter in rfl?

view this post on Zulip Eric Wieser (Apr 11 2021 at 21:23):

rfl is just a shorthand for docs#eq.refl, a constructor for docs#eq

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:07):

(deleted)

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:11):

@Eric Wieser here's waht I understand:

  1. Lean4 has a "symbolic" rewriter for terms in the goals
    From the manual:
-- You can prove theorems about your functions.
-- The following theorem states that for any natural number `a`,
-- adding 2 twice produces a value equal to `a + 4`.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
  -- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
  -- until they are identical.
  rfl
  1. the eq.refl you pointed to is in mathlib, aka Lean3.
  2. In RUBI, the symbolic term rewriter is crucial for performance and solvability of integration problems.
  3. Leo published a fundamental paper of egraphs for symbolic term rewriting, and @Alessandro and I are wondering if that was implemented as the symbolic term rewriter in Lean4.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:11):

Lean 4's rfl is the same as lean 3's rfl. It's not a "symbolic rewriter", it compares values up to a relation called definitional equality

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:12):

Thanks Mario, nice to see you around here too :D

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:12):

which involves weakly normalizing both sides to a constructor

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:12):

I am everywhere

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:13):

Well I'm bringing this up because I'm "close" :tm: to porting RUBI to Julia, and from there porting RUBI to Lean wouldn't be "that much" additional effort. I would want to know which tactic I could dump a lhs = rhs ruleset, if at all feasible.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:14):

As far as I know, nothing about egraphs or symbolic term rewriting is involved in the implementation of rfl and/or defeq in any version of lean. This is much more based on literature on dependent type theory, reduction and strong normalization stuff

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:15):

Oh neat.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:15):

However, you will find more of leo's creativity in the simp tactic, which does symbolic term rewriting closer to what you are talking about

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:15):

Ah, that's the one. So I could in theory overload simp with a bunch of these integration rules, right?

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:16):

yes

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:16):

We've done that for derivatives in mathlib

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:16):

I think integration too but I guess the coverage is lower

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:17):

its ability to pattern match on lambdas is limited though, so most likely you would do a full integration routine as a dedicated tactic

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:17):

Ouch.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:20):

I mean, it's pretty hard to recognize that in the function \lam x, sin x * (2 / cos x) you want to pull out the constant factor 2 (let's say this is a preprocessing step)

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:21):

you would have a huge number of possible patterns to look for to find the 2

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:22):

Yup, that's a transformation that egraphs can achieve linear in the number of patterns that match, without running into the phase ordering problem of some transformations will bork others.

Hence why we're asking :D

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:22):

This is a good overview (that I'm still becoming familiar with myself)
https://egraphs-good.github.io/

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:25):

I don't think I have seen anything like this implemented in lean

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:25):

It is possible to implement it yourself, of course

view this post on Zulip Mario Carneiro (Apr 12 2021 at 01:26):

(in lean 3 or lean 4, although it's probably better suited for lean 4)

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:36):

Yeah, condolences to the mathlib crowd, I'm learning Lean4 - the garbage collector's too good to pass up :muscle:

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 01:37):

(And in fact it will probably do amazingly in the benchmarks what with the functional but in place style not generating tons of allocations in all the symbolic computations.)


Last updated: May 13 2021 at 18:26 UTC