Zulip Chat Archive

Stream: general

Topic: Choice for a sum of polynomials


Bolton Bailey (Jul 25 2022 at 17:26):

Here's a minimal working error:

import data.polynomial.basic

open_locale big_operators

variables {F : Type} [field F]

def fri_poly (f : ) (p : polynomial F) :  -> polynomial F
| 0 := p
| (n+1) :=  (split : fin f), (fri_poly n)

equation compiler failed to generate bytecode for 'fri_poly._main' nested exception message: code generation failed, VM does not have code for 'classical.choice'

How exactly does this definition depend on choice?

Reid Barton (Jul 25 2022 at 17:28):

Probably to add polynomials

Eric Rodriguez (Jul 25 2022 at 17:30):

def fri_poly (f : ) (p : polynomial F) :   polynomial F
| 0 := p
| (n+1) := fri_poly n

#eval fri_poly 1 (1 : polynomial )

still fails thoguh

Bolton Bailey (Jul 25 2022 at 17:37):

Well ℕ is not a field

Reid Barton (Jul 25 2022 at 17:51):

I assume that one is due to the coercion (it probably wants to determine whether the coefficient is nonzero)

Eric Wieser (Jul 25 2022 at 18:02):

Fails in what way @Eric Rodriguez?

Junyan Xu (Jul 25 2022 at 18:28):

#eval fri_poly 1 (1 : polynomial ℚ) /- code generation failed, VM does not have code for 'classical.choice' -/
#eval fri_poly 1 (0 : polynomial ℚ) /- result type does not have an instance of type class 'has_repr', dumping internal representation (fri_poly._main (#0 #0 (_main._lambda_1)) (#0 (rat.add._main) (#0 ... (omitted) -/
I think docs#polynomial.has_one uses the classical decidability instance (via docs#finsupp.single) while docs#polynomial.has_zero doesn't.

Kyle Miller (Jul 25 2022 at 19:44):

code generation failed is an internal error, suggesting that the noncomputability checker is not working correctly for this example. It has to do with the equation compiler creating an auxiliary definition that needs to be compiled.

The easy short-term fix is to put noncomputable! on the definition to force everything to be noncomputable, which should hopefully work here.

Eric Wieser (Jul 25 2022 at 20:07):

The reason for choice here is that docs#polynomial.has_one is noncomputable


Last updated: Dec 20 2023 at 11:08 UTC