Zulip Chat Archive

Stream: general

Topic: polynomial eval dot notation


Bolton Bailey (Feb 02 2022 at 07:31):

This is a bit surprising,

import data.polynomial.eval

example (p : polynomial ) : p.eval = (λ x, p.eval x) := sorry
-- p is expected to have type polynomial (polynomial (polynomial ℕ))

Is there any way to tell lean that the dot notation for polynomial.eval is always supposed to be for the second argument?

Yaël Dillies (Feb 02 2022 at 08:52):

Unfortunately not as far as I'm aware. The trick is to apply the function enough for Lean to figure out what you're dot notating on, and not use dot notation when that's impossible.

Kevin Buzzard (Feb 02 2022 at 09:00):

Ha ha exactly this happened to me in a live lean session yesterday and I just resorted to lambdas

Yakov Pechersky (Feb 02 2022 at 14:01):

One reason it's not this way is because "eval 0" is a pretty useful function to apply to the various polynomials as is. "eval r" is a ring_hom, for all r, for example.

Eric Rodriguez (Feb 02 2022 at 14:09):

i'm still sad that we can't make map a bundled morphism because of dot notation

Chris Hughes (Feb 02 2022 at 15:53):

Eric Rodriguez said:

i'm still sad that we can't make map a bundled morphism because of dot notation

I would much rather it be bundled and lose the notation.

Eric Rodriguez (Feb 02 2022 at 15:54):

there's something like 1K uses in the library, plus we'd want to migrate map_zero/one/mul/add... to use the fun_like ones. I'm happy to help with that, but I really don't want to start that and then be told "oh actually we don't like this"

Bolton Bailey (Aug 14 2023 at 17:10):

Reviving this thread to bring up a new MWE. It seems I can use dot notation to eval a Polynomial, but not a MvPolynomial. Why is this?

import Mathlib

open scoped BigOperators Classical

section Matrix

variable {F} [Field F] [Fintype F] {H : Subgroup Fˣ} [Fintype H]

lemma lincheck_to_sumcheck_matrix_completeness (z_hat_M z_hat : Polynomial F)
  (f_M : MvPolynomial (Fin 2) F) (r : MvPolynomial (Fin 2) F) :
    (fun x => Polynomial.eval x z_hat_M) =
      Matrix.mulVec
        (fun x y => MvPolynomial.eval ![x, y] f_M)
        (fun y => z_hat.eval y) := by
  sorry

lemma lincheck_to_sumcheck_matrix_completeness' (z_hat_M z_hat : Polynomial F)
  (f_M : MvPolynomial (Fin 2) F) (r : MvPolynomial (Fin 2) F) :
    (fun x => Polynomial.eval x z_hat_M) =
      Matrix.mulVec
        (fun x y => f_M.eval ![x, y]) -- invalid field notation, function 'MvPolynomial.eval' does not have argument with type (MvPolynomial ...) that can be used, it must be explicit or implicit with a unique name
        (fun y => z_hat.eval y) := by
  sorry


end Matrix

Eric Wieser (Aug 14 2023 at 17:15):

docs#MvPolynomial.eval is a RingHom which confuses dot notation, docs#Polynomial.eval is a regular function

Antoine Chambert-Loir (Aug 16 2023 at 19:18):

Doesn't this call for some homogeneization?

David Ang (Aug 16 2023 at 20:03):

I think eval should always be a regular function

David Ang (Aug 16 2023 at 20:07):

There’s also the question of map being a ring homomorphism or not

Eric Wieser (Aug 16 2023 at 20:09):

Once upon a time I think we had Polynomial = MvPolynomial Unit, which has the big advantage that the APIs are completely homogenous, but the big disadvantage that the APIs are completely homogenous.

Bolton Bailey (Aug 16 2023 at 20:15):

What do people think of having two functions, say eval and eval_at something else, with different argument orders/one is a hom and the other is a plain function?

Yury G. Kudryashov (Aug 16 2023 at 21:06):

Which one is the simp normal form?

Eric Wieser (Aug 16 2023 at 21:21):

We already have two functions for polynomial, docs#Polynomial.eval and docs#Polynomial.evalRingHom

Bolton Bailey (Aug 16 2023 at 21:22):

I don't really know what the criteria are for a good simp normal form. I think I would prefer eval (the polynomial first argument order) to be more widely used because this is how I think functions are usually designed.

Bolton Bailey (Aug 16 2023 at 21:24):

I guess what I'm suggesting then is that we redefine MvPolynomial.eval to have the polynomial argument first, rewrite everything we can to use the new eval argument order, and rewrite the things we can't to use evalRingHom.toFun.

Bolton Bailey (Aug 16 2023 at 21:27):

The overriding concern to me is that I am used to hearing "we evaluate a polynomial p at point x", and so this is the order of arguments I expect to see and use in the majority of cases where I am not taking advantage of the homomorphism structure of the particular point evaluation.

Bolton Bailey (Aug 16 2023 at 21:30):

Eric Wieser said:

docs#MvPolynomial.eval is a RingHom which confuses dot notation, docs#Polynomial.eval is a regular function

By the way, while I now understand this is why I was experiencing a bug, I think I don't get why this is the case. Even if the default argument order doesn't change, why is a different decision made for Polynomial versus MvPolynomial on the point of the point-first function being a hom?

Eric Wieser (Aug 16 2023 at 22:36):

Probably because different people made the decision without communicating

Eric Wieser (Aug 16 2023 at 22:37):

Or someone decided to change both, but only got around to changing one

Eric Wieser (Aug 16 2023 at 22:38):

Bolton Bailey said:

The overriding concern to me is that I am used to hearing "we evaluate a polynomial p at point x", and so this is the order of arguments I expect to see and use in the majority of cases where I am not taking advantage of the homomorphism structure of the particular point evaluation.

docs#Function.eval uses the same convention as docs#Polynomial.eval, both of which go against your intuition here.

Bolton Bailey (Aug 17 2023 at 00:52):

Wild. I see that docs#RatFunc.eval does as well, though the docstring does have the same form as the natural-language sentence I gave.

Bolton Bailey (Aug 17 2023 at 00:56):

Maybe the issue is that apply is the more natural word for the operation with my conception of the ordering, but that there is already a meaning for that?

Bolton Bailey (Aug 17 2023 at 00:58):

I am partially also thinking of functions like docs#List.nthLe or docs#Vector.get, which have the "function like structure" argument first.

Damiano Testa (Aug 17 2023 at 06:59):

It could be that the order is so that eval x is the function that happens to also be the homomorphism, as opposed to the (non-existing in Lean 3) (eval · x).

Damiano Testa (Aug 17 2023 at 07:00):

If I remember correctly, in Lean 3, certain things could/could not work depending on the order of the arguments.

Damiano Testa (Aug 17 2023 at 07:02):

(I also find the order eval polynomial point more natural, but the possibility of writing p.eval x anyway makes this rarely an issue for me.)

Mario Carneiro (Aug 17 2023 at 07:20):

This actually looks like a bug or at least an issue to be reported and decide whether we want this behavior. If T.foo : α -> T -> T then I expect (t:T).foo a to mean T.foo a t even if it is applied in the special case where α := T

Mario Carneiro (Aug 17 2023 at 07:21):

that is, the decision of which variable to treat as the main one should be done based on the constant's type before instantiation (possibly with the current behavior as fallback so that T.foo : α -> α -> α still works when applied with α := T)

Mario Carneiro (Aug 17 2023 at 07:24):

actually, this doesn't even work:

def Nat.foo {α} : α  α  α := fun _ y => y
#check (1:Nat).foo 2

invalid field notation, function 'Nat.foo' does not have argument with type (Nat ...) that can be used, it must be explicit or implicit with a unique name

so this seems more like a bug / inconsistent behavior

Mario Carneiro (Aug 17 2023 at 07:27):

Oh I was mislead, the initial issue is from lean 3, this does not replicate in lean 4

Eric Wieser (Aug 17 2023 at 08:19):

@Mario Carneiro, I'm confused by your comment; isn't the problem with dot notation for docs#MvPolynomial.eval due toT.foo : α -> SomeHom T U not knowing how to tell that SomeHom expects a T argument?

Mario Carneiro (Aug 17 2023 at 08:35):

yes, my comment was about the wrong issue

Mario Carneiro (Aug 17 2023 at 08:35):

because this issue was continued from a completely different one


Last updated: Dec 20 2023 at 11:08 UTC