# 9.66 RealClosure¶

The Real Closure 1.0 package provided by Renaud Rioboo (Renaud.Rioboo@lip6.fr) consists of different packages, categories and domains :

The package RealPolynomialUtilitiesPackage which needs a Field F and a UnivariatePolynomialCategory domain with coefficients in F. It computes some simple functions such as Sturm and Sylvester sequences (sturmSequencesturmSequenceRealPolynomialUtilitiesPackage, sylvesterSequencesylvesterSequenceRealPolynomialUtilitiesPackage).

The category RealRootCharacterizationCategory provides abstract functions to work with real roots of univariate polynomials. These resemble variables with some functionality needed to compute important operations.

The category RealClosedField provides common operations available over real closed fiels. These include finding all the roots of a univariate polynomial, taking square (and higher) roots, ...

The domain RightOpenIntervalRootCharacterization is the main code that provides the functionality of RealRootCharacterizationCategory for the case of archimedean fields. Abstract roots are encoded with a left closed right open interval containing the root together with a defining polynomial for the root.

The RealClosure domain is the end-user code. It provides usual arithmetic with real algebraic numbers, along with the functionality of a real closed field. It also provides functions to approximate a real algebraic number by an element of the base field. This approximation may either be absolute (approximateapproximateRealClosure) or relative (relativeApproxrelativeApproxRealClosure).

CAVEATS

Since real algebraic expressions are stored as depending on real roots which are managed like variables, there is an ordering on these. This ordering is dynamical in the sense that any new algebraic takes precedence over older ones. In particular every creation function raises a new real root. This has the effect that when you type something like sqrt(2) + sqrt(2) you have two new variables which happen to be equal. To avoid this name the expression such as in s2 := sqrt(2) ; s2 + s2

Also note that computing times depend strongly on the ordering you implicitly provide. Please provide algebraics in the order which seems most natural to you.

LIMITATIONS

These packages use algorithms which are published in [1] and [2] which are based on field arithmetics, in particular for polynomial gcd related algorithms. This can be quite slow for high degree polynomials and subresultants methods usually work best. Beta versions of the package try to use these techniques in a better way and work significantly faster. These are mostly based on unpublished algorithms and cannot be distributed. Please contact the author if you have a particular problem to solve or want to use these versions.

Be aware that approximations behave as post-processing and that all computations are done exactly. They can thus be quite time consuming when depending on several real roots.

REFERENCES

[1] R. Rioboo : Real Algebraic Closure of an ordered Field : Implementation in FriCAS. In proceedings of the ISSAC‘92 Conference, Berkeley 1992 pp. 206-215.

[2] Z. Ligatsikas, R. Rioboo, M. F. Roy : Generic computation of the real closure of an ordered field. In Mathematics and Computers in Simulation Volume 42, Issue 4-6, November 1996.

EXAMPLES

We shall work with the real closure of the ordered field of rational numbers.

Ran := RECLOS(FRAC INT)


 RealClosureFractionInteger

Type: Domain

Some simple signs for square roots, these correspond to an extension of degree 16 of the rational numbers. Examples provided by J. Abbot.

fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran == sqrt(a)+sqrt(b) -


sqrt(c)-sqrt(d)

Function declaration fourSquares : (RealClosure Fraction Integer,
RealClosure Fraction Integer,RealClosure Fraction Integer,
RealClosure Fraction Integer) -> RealClosure Fraction Integer has


Void

These produce values very close to zero.

squareDiff1 := fourSquares(73,548,60,586)


 -586-60+548+73

Type: RealClosure Fraction Integer

recip(squareDiff1)


 ((54602548+14960273)60+4950273548+9900895)586+(15470273548+30941947)60+10238421548+2805187173

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff1)


 1

Type: PositiveInteger

squareDiff2 := fourSquares(165,778,86,990)


 -990-86+778+165

Type: RealClosure Fraction Integer

recip(squareDiff2)


 ((556778778+1209010165)86+401966165778+144019431)990+(1363822165778+488640503)86+162460913778+352774119165

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff2)


 1

Type: PositiveInteger

squareDiff3 := fourSquares(217,708,226,692)


 -692-226+708+217

Type: RealClosure Fraction Integer

recip(squareDiff3)


 ((-34102708-61598217)226-34802217708-13641141)692+(-60898217708-23869841)226-13486123708-24359809217

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff3)


 -1

Type: Integer

squareDiff4 := fourSquares(155,836,162,820)


 -820-162+836+155

Type: RealClosure Fraction Integer

recip(squareDiff4)


 ((-37078836-86110155)162-37906155836-13645107)820+(-85282155836-30699151)162-13513901836-31384703155

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff4)


 -1

Type: Integer

squareDiff5 := fourSquares(591,772,552,818)


 -818-552+772+591

Type: RealClosure Fraction Integer

recip(squareDiff5)


 ((70922772+81058591)552+68542591772+46297673)818+(83438591772+56359389)552+47657051772+54468081591

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff5)


 1

Type: PositiveInteger

squareDiff6 := fourSquares(434,1053,412,1088)


 -1088-412+1053+434

Type: RealClosure Fraction Integer

recip(squareDiff6)


 ((1154421053+179818434)412+1124784341053+76037291)1088+(1827824341053+123564147)412+772906391053+120391609434

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff6)


 1

Type: PositiveInteger

squareDiff7 := fourSquares(514,1049,446,1152)


 -1152-446+1049+514

Type: RealClosure Fraction Integer

recip(squareDiff7)


 ((3495221049+499322514)446+3255825141049+239072537)1152+(5232625141049+384227549)446+2505348731049+357910443514

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff7)


 1

Type: PositiveInteger

squareDiff8 := fourSquares(190,1751,208,1698)


 -1698-208+1751+190

Type: RealClosure Fraction Integer

recip(squareDiff8)


 ((-2147021751-651782190)208-2246421901751-129571901)1698+(-6418421901751-370209881)208-1275958651751-387349387190

Type: Union(RealClosure Fraction Integer,...)

sign(squareDiff8)


 -1

Type: Integer

This should give three digits of precision

relativeApprox(squareDiff8,10^(-3))::Float


 -2.34053e-11

Type: Float

The sum of these 4 roots is 0

l := allRootsOf((x^2-2)^2-2)$Ran    [%A33,%A34,%A35,%A36] Type: List RealClosure Fraction Integer Check that they are all roots of the same polynomial removeDuplicates map(mainDefiningPolynomial,l)    [?4-4?2+2] Type: List Union(SparseUnivariatePolynomial RealClosure Fraction Integer,”failed”) We can see at a glance that they are separate roots map(mainCharacterization,l)    [[-2,-1[,[-1,0[,[0,1[,[1,2[] Type: List Union( RightOpenIntervalRootCharacterization( RealClosure Fraction Integer, SparseUnivariatePolynomial RealClosure Fraction Integer), “failed”) Check the sum and product [reduce(+,l),reduce(*,l)-2]    [0,0] Type: List RealClosure Fraction Integer A more complicated test that involve an extension of degree 256. This is a way of checking nested radical identities. (s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran)


 10

Type: RealClosure Fraction Integer

eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)


 -10-35-2+10+35+2=102+10

Type: Equation RealClosure Fraction Integer

eq1::Boolean


 true

Type: Boolean

eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)


 -5-22-1+5+22+1=210+2

Type: Equation RealClosure Fraction Integer

eq2::Boolean


 true

Type: Boolean

Some more examples from J. M. Arnaudies

s3 := sqrt(3)$Ran    3 Type: RealClosure Fraction Integer s7:= sqrt(7)$Ran


 7

Type: RealClosure Fraction Integer

e1 := sqrt(2*s7-3*s3,3)


 27-333

Type: RealClosure Fraction Integer

e2 := sqrt(2*s7+3*s3,3)


 27+333

Type: RealClosure Fraction Integer

This should be null

e2-e1-s3


 0

Type: RealClosure Fraction Integer

A quartic polynomial

pol : UP(x,Ran) := x^4+(7/3)*x^2+30*x-(100/3)


 x4+73x2+30x-1003

Type: UnivariatePolynomial(x,RealClosure Fraction Integer)

r1 := sqrt(7633)$Ran    7633 Type: RealClosure Fraction Integer alpha := sqrt(5*r1-436,3)/3    1357633-4363 Type: RealClosure Fraction Integer beta := -sqrt(5*r1+436,3)/3    -1357633+4363 Type: RealClosure Fraction Integer this should be null pol.(alpha+beta-1/3)    0 Type: RealClosure Fraction Integer A quintic polynomial qol : UP(x,Ran) := x^5+10*x^3+20*x+22    x5+10x3+20x+22 Type: UnivariatePolynomial(x,RealClosure Fraction Integer) Add some cubic roots r2 := sqrt(153)$Ran


 153

Type: RealClosure Fraction Integer

alpha2 := sqrt(r2-11,5)


 153-115

Type: RealClosure Fraction Integer

beta2 := -sqrt(r2+11,5)


 -153+115

Type: RealClosure Fraction Integer

this should be null

qol(alpha2+beta2)


 0

Type: RealClosure Fraction Integer

Finally, some examples from the book Computer Algebra by Davenport, Siret and Tournier (page 77). The last one is due to Ramanujan.

dst1:=sqrt(9+4*s2)=1+2*s2


 42+9=22+1

Type: Equation RealClosure Fraction Integer

dst1::Boolean


 true

Type: Boolean

s6:Ran:=sqrt 6


 6

Type: RealClosure Fraction Integer

dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3


 -26+5+26+5=23

Type: Equation RealClosure Fraction Integer

dst2::Boolean


 true

Type: Boolean

s29:Ran:=sqrt 29


 29

Type: RealClosure Fraction Integer

dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) =


sqrt(22+2*s5)-sqrt(11+2*s29)+s5


 2-1029+55-229+16=-229+11+25+22+5

Type: Equation RealClosure Fraction Integer

dst4::Boolean


 true

Type: Boolean

dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5


 (342+46)5+702+112=(2+3)5+42+5

Type: Equation RealClosure Fraction Integer

dst6::Boolean


 true

Type: Boolean

f3:Ran:=sqrt(3,5)


 35

Type: RealClosure Fraction Integer

f25:Ran:=sqrt(1/25,5)


 1255

Type: RealClosure Fraction Integer

f32:Ran:=sqrt(32/5,5)


 3255

Type: RealClosure Fraction Integer

f27:Ran:=sqrt(27/5,5)


 2755

Type: RealClosure Fraction Integer

dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3^2)


 -2755+32553=(-352+35+1)1255

Type: Equation RealClosure Fraction Integer

dst5::Boolean


 true

Type: Boolean