Zulip Chat Archive

Stream: general

Topic: a dedup linter?


view this post on Zulip Mario Carneiro (Aug 17 2020 at 01:22):

What we want to avoid is anything that is O(n^2)

view this post on Zulip Mario Carneiro (Aug 17 2020 at 01:24):

False negatives here are because the expr ordering is fairly strict and might not pick up on theorems that we would say are the same but differ in some behind the scenes detail like variable names

view this post on Zulip Notification Bot (Aug 17 2020 at 02:05):

This topic was moved here from #new members > Starting to contribute to mathlib by Jalex Stark

view this post on Zulip Jalex Stark (Aug 17 2020 at 02:43):

okay, so I guess we can a little bit farther by computing a normal form for exprs that forgets variable names. informally speaking, the algorithm is like
Fix a canonical infinite list of names.
for a given expr, put an order on the variables names by traversing the expr tree and writing them down in the order you see them
rename the nth variable in this expr list to the nth variable in the canonical list

view this post on Zulip Jalex Stark (Aug 17 2020 at 02:44):

but this approach doesn't seem like it will get you to a much coarser notion of equivalence than this uh "syntactic equality up to renaming variables"

view this post on Zulip Mario Carneiro (Aug 17 2020 at 03:18):

I think expr.lt already does something like this. I would try just using it and see if it needs tweaking after

view this post on Zulip Johan Commelin (Aug 17 2020 at 03:49):

@Jalex Stark Maybe you can make all variables explicit during this step, because that might be another source of "the same, but not syntactially so"

view this post on Zulip Johan Commelin (Aug 17 2020 at 03:50):

And if the order of two assumptions doesn't matter to the type checker, sort them by their types. That might take care of permutations of the variables.

view this post on Zulip Jalex Stark (Aug 17 2020 at 10:09):

Initially with that suggestion I was worried about dependence of later args on earlier ones. But we're just trying to construct a function on expr whose preinages form the right equivalence relation. We don't need the image to be something we can elaborate! (I'll not sure "elaborate" is the right concept.)

view this post on Zulip Rob Lewis (Aug 17 2020 at 10:17):

expr.alpha_eqv compares expressions ignoring binder type and bound variable names.

#eval expr.alpha_eqv `(λ {x : }, 0) `(λ y : , 0)

view this post on Zulip Jalex Stark (Aug 17 2020 at 21:19):

I guess the next step is to peek into the implementation of expr.alpha_eqv and see whether it is already computing normal form exprs and checking expr equality, since that's really what's needed for the linter.


Last updated: May 14 2021 at 14:20 UTC