Zulip Chat Archive

Stream: maths

Topic: constructive real algebraic numbers


view this post on Zulip Reid Barton (Nov 13 2019 at 12:06):

Not really a Lean question but the real algebraic numbers form a real closed field constructively, right? What's the easiest way to see this?

view this post on Zulip Reid Barton (Nov 13 2019 at 12:07):

I'm supposed to represent a real algebraic number by a polynomial together with an interval of rationals on which it has a unique root, or something?

view this post on Zulip Ulrik Buchholtz (Nov 13 2019 at 12:10):

I think the original reference is Madison 1970, but there may have been some improvements since.

view this post on Zulip Ulrik Buchholtz (Nov 13 2019 at 12:11):

Madison just pairs a polynomial together with the number of roots left of the desired root.

view this post on Zulip Reid Barton (Nov 13 2019 at 12:13):

Oh thanks. Let's suppose I already believe in quantifier elimination for real closed fields. Then it's easy to see how to decide the ordering on such descriptions. Let's suppose I also believe that given polynomials f and g I can find a polynomial whose roots are the sums of the roots of f and g. Is it easy to see how to pick out the index of the correct root?

view this post on Zulip Reid Barton (Nov 13 2019 at 12:14):

And same for products

view this post on Zulip Reid Barton (Nov 13 2019 at 12:14):

I guess this is probably in this 3-page paper, which I can't conveniently download at the moment

view this post on Zulip Ulrik Buchholtz (Nov 13 2019 at 12:27):

I guess this is probably in this 3-page paper, which I can't conveniently download at the moment

Actually, it's not, since he just shows that the relations x+y=z x + y = z and xy=z xy = z are decidable. (Check you mail for the paper.) I don't see immediately how compute the representations of x+y x + y and xy xy from those of x x and y y .

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:27):

Is his proof constructive?

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:28):

I think there are methods using resultants and such, to go from x and y to x + y and xy.

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:28):

I don't remember the details, but I think it can be done quite constructively

view this post on Zulip Ulrik Buchholtz (Nov 13 2019 at 12:30):

Yes, I think it's constructive. There are bunch of other representations where you pair a polynomial with either an interval, a Cauchy sequence, or something else. (I see Thom representations and sign representations and what-not…)

view this post on Zulip Reid Barton (Nov 13 2019 at 12:39):

The algorithms for arithmetic in the Madison paper are of the form "try every representation until you find one that works" (tested by quantifier elimination). I guess those won't satisfy a constructivist.

view this post on Zulip Reid Barton (Nov 13 2019 at 12:41):

I feel like this is the sort of thing someone would definitely have already formalized in Coq

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:41):

Why? :see_no_evil: It would only have doubly-exponential running time...

view this post on Zulip Reid Barton (Nov 13 2019 at 12:43):

Because you don't know that the search will actually succeed unless you already proved (meaning constructively) that a solution exists

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:43):

How about you combine the two representations: both small intervals around the roots and a pointer to the interval you care about.

view this post on Zulip Reid Barton (Nov 13 2019 at 12:43):

in which case you don't need the search

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:43):

That might lead to rather efficient add/mul ?

view this post on Zulip Reid Barton (Nov 13 2019 at 12:45):

Aha, https://hal.inria.fr/hal-00671809v2

view this post on Zulip Johan Commelin (Nov 13 2019 at 12:46):

@Cyril Cohen We are watching you :grinning_face_with_smiling_eyes: :wink:

view this post on Zulip Patrick Massot (Nov 13 2019 at 12:49):

Why are we loosing Reid? What happened? He used to be doing mathematics!

view this post on Zulip Chris Hughes (Nov 13 2019 at 13:22):

I remember talking to Cyril about this. This is one place where Lean wins over Coq, because of quotients. In order to remain constructive in Coq, he had to reduce each number to a canonical, but I think he said most computer implementations actually don't reduce each number to a canonical form.

view this post on Zulip Reid Barton (Nov 13 2019 at 13:38):

Interesting.
I was going to ask @Mario Carneiro to automatically export the construction from Coq and import it into Lean (while remaining constructive of course) but I guess he's off the hook

view this post on Zulip Wojciech Nawrocki (Nov 29 2019 at 22:25):

Out of curiosity @Reid Barton what's your usecase for real algebraics? Wenda Li has been doing some great work on using them for efficiently deciding certain kinds of univariate polynomial inequalities in Isabelle: paper1 paper2


Last updated: May 19 2021 at 02:10 UTC