constructive real algebraic numbers

Stream: maths

[Reid Barton]

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?

[Reid Barton]

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?

[Ulrik Buchholtz]

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

[Ulrik Buchholtz]

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

[Reid Barton]

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?

[Reid Barton]

And same for products

[Reid Barton]

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

[Ulrik Buchholtz]

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$ and $xy = z$ are decidable. (Check you mail for the paper.) I don't see immediately how compute the representations of $x + y$ and $xy$ from those of $x$ and $y$.

[Johan Commelin]

Is his proof constructive?

[Johan Commelin]

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

[Johan Commelin]

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

[Ulrik Buchholtz]

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…)

[Reid Barton]

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.

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

in which case you don't need the search

[Johan Commelin]

That might lead to rather efficient add/mul ?

[Reid Barton]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Chris Hughes]

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.

[Reid Barton]

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

[Wojciech Nawrocki]

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