Zulip Chat Archive

Stream: general

Topic: why is this slow?


view this post on Zulip Kenny Lau (Sep 16 2018 at 09:44):

import data.polynomial
import linear_algebra.multivariate_polynomial
import ring_theory.associated

universe u

namespace algebraic_closure

variables (k : Type u) [field k] [decidable_eq k]

def irred : set (polynomial k) :=
{ p | irreducible p }

def big_ring : Type u :=
mv_polynomial (irred k) k

instance : comm_ring (big_ring k) :=
mv_polynomial.comm_ring

set_option profiler true
def big_ideal : set (big_ring k) :=
span $  p : irred k, { polynomial.eval₂ mv_polynomial.C (mv_polynomial.X p) p.1 }
/-
parsing took 0.154ms
elaboration of big_ideal took 7.53s
type checking of big_ideal took 9.17ms
decl post-processing of big_ideal took 11.1ms
compilation of algebraic_closure.big_ideal took 0.205ms
-/

end algebraic_closure

view this post on Zulip Kenny Lau (Sep 16 2018 at 09:44):

is there any way to make this faster?

view this post on Zulip Kenny Lau (Sep 16 2018 at 09:48):

@Chris Hughes

view this post on Zulip Chris Hughes (Sep 16 2018 at 10:01):

This compiles in no time. I don't know the solution though.

def big_ideal : set (mv_polynomial (irred k) k) :=
span $  p : irred k, { polynomial.eval₂ mv_polynomial.C (mv_polynomial.X p) p.1 }

view this post on Zulip Kenny Lau (Sep 16 2018 at 10:46):

@Kevin Buzzard @Chris Hughes I suspect Chris's span is the wrong one, which means we will have to once again wait for the refactoring

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 10:48):

So what exactly is being refactored? Yeah I am putting "research level" coding on hold at the minute and thinking more about organisational stuff. The question of why it's slow is still of independent interest. What is causing the hold-up? Is it type class inference?

view this post on Zulip Kenny Lau (Sep 16 2018 at 10:49):

if we specify that we're talking about the span as an ideal (which is this case) or that we're talking about the span as a k-module (which is not this case) then it would be more convenient

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:02):

@Mario Carneiro is this another +1 for saying which ring we're talking about explicitly?

I guess there is also now the option of making the "ideal" version of things into its own little interface -- e.g. ideal.span could mean "the span of this subset of the ring R as an R-module"

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:02):

I would love to be able to debug this sort of thing. Presumably the by exact insertion changes the elaboration strategy somehow. But in my mind this just raises a bunch of questions as to how it's working and how the change makes any difference.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:02):

def big_ideal' : set (big_ring k) :=
by exact (span $  p : irred k, { polynomial.eval₂ mv_polynomial.C (mv_polynomial.X p) p.1 })

is much quicker for me and seems to give the same answer.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:17):

Stupid #print notation ⋃ gives me a useless answer. I had to grep through the source code to find it's set.Union.

view this post on Zulip Chris Hughes (Sep 16 2018 at 11:18):

So in future presumably span will take the ring as an explicit argument?

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:36):

hopefully. Hey I got Kenny's version working quickly:

def big_ideal' : set (big_ring k) :=
span $  p : irred k, {@polynomial.eval₂ _ _ _ _ _ mv_polynomial.C _ (mv_polynomial.X p) p.1}

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:36):

I'm hoping that submodule will as well.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:37):

In your polynomial code, module R (polynomial R) takes precedence over module (polynomial R) (polynomial R) making it really difficult to talk about ideals of polynomial rings!

view this post on Zulip Chris Hughes (Sep 16 2018 at 11:43):

Change it then. I didn't really think about that problem when I wrote it.

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:45):

rofl

def big_ideal' : set (big_ring k) :=
span $  p : irred k, {@polynomial.eval₂ k _ _ (big_ring k) _ mv_polynomial.C _ (mv_polynomial.X p) p.1}

breaks it again -- apparently explictly telling Lean to use big_ring k rather than letting it work it out for itself is a bad idea. @Mario Carneiro what is going on here?

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 11:48):

Adding instance : is_semiring_hom (mv_polynomial.C : k → big_ring k) := by apply_instance speeds Kenny's original code up a bit.


Last updated: May 14 2021 at 13:24 UTC