The Real Closure 1.0 package provided by Renaud Rioboo 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 sturmSequence, sylvesterSequence.
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, approximate or relative (relativeApprox).
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.
This packages uses 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.
| [1] | R. Rioboo : Real Algebraic Closure of an ordered Field : Implementation in Axiom. 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. |
We shall work with the real closure of the ordered field of rational numbers.
Ran := RECLOS(FRAC INT)
RealClosure Fraction Integer
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)
Type: Void
These produce values very close to zero.
squareDiff1 := fourSquares(73,548,60,586)
+---+ +--+ +---+ +--+
- \|586 - \|60 + \|548 + \|73
Type: RealClosure Fraction Integer
recip(squareDiff1)
+---+ +--+ +--+ +--+ +---+ +---+
((54602\|548 + 149602\|73 )\|60 + 49502\|73 \|548 + 9900895)\|586
+
+--+ +---+ +--+ +---+ +--+
(154702\|73 \|548 + 30941947)\|60 + 10238421\|548 + 28051871\|73
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)
+---+ +---+ +--+ +---+ +---+
((556778\|778 + 1209010\|165 )\|86 + 401966\|165 \|778 + 144019431)
*
+---+
\|990
+
+---+ +---+ +--+ +---+ +---+
(1363822\|165 \|778 + 488640503)\|86 + 162460913\|778 + 352774119\|165
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)
+---+ +---+ +---+ +---+ +---+ +---+
((- 34102\|708 - 61598\|217 )\|226 - 34802\|217 \|708 - 13641141)\|692
+
+---+ +---+ +---+ +---+ +---+
(- 60898\|217 \|708 - 23869841)\|226 - 13486123\|708 - 24359809\|217
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)
+---+ +---+ +---+ +---+ +---+ +---+
((- 37078\|836 - 86110\|155 )\|162 - 37906\|155 \|836 - 13645107)\|820
+
+---+ +---+ +---+ +---+ +---+
(- 85282\|155 \|836 - 30699151)\|162 - 13513901\|836 - 31384703\|155
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)
+---+ +---+ +---+ +---+ +---+ +---+
((70922\|772 + 81058\|591 )\|552 + 68542\|591 \|772 + 46297673)\|818
+
+---+ +---+ +---+ +---+ +---+
(83438\|591 \|772 + 56359389)\|552 + 47657051\|772 + 54468081\|591
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)
+----+ +---+ +---+ +---+ +----+
((115442\|1053 + 179818\|434 )\|412 + 112478\|434 \|1053 + 76037291)
*
+----+
\|1088
+
+---+ +----+ +---+ +----+ +---+
(182782\|434 \|1053 + 123564147)\|412 + 77290639\|1053 + 120391609\|434
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)
+----+ +---+ +---+ +---+ +----+
((349522\|1049 + 499322\|514 )\|446 + 325582\|514 \|1049 + 239072537)
*
+----+
\|1152
+
+---+ +----+ +---+ +----+ +---+
(523262\|514 \|1049 + 384227549)\|446 + 250534873\|1049 + 357910443\|514
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)
+----+ +---+ +---+ +---+ +----+
(- 214702\|1751 - 651782\|190 )\|208 - 224642\|190 \|1751
+
- 129571901
*
+----+
\|1698
+
+---+ +----+ +---+ +----+
(- 641842\|190 \|1751 - 370209881)\|208 - 127595865\|1751
+
+---+
- 387349387\|190
Type: Union(RealClosure Fraction Integer,...)
sign(squareDiff8)
- 1
Type: Integer
This should give three digits of precision
relativeApprox(squareDiff8,10**(-3))::Float
- 0.2340527771 5937700123 E -10
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 2
[? - 4? + 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 - 3 \|\|5 - 2 + \|\|10 + 3 \|\|5 + 2 = \|10\|2 + 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 - 2 \|\|2 - 1 + \|\|5 + 2 \|\|2 + 1 = \|2\|10 + 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)
+-------------+
3| +-+ +-+
\|2\|7 - 3\|3
Type: RealClosure Fraction Integer
e2 := sqrt(2*s7+3*s3,3)
+-------------+
3| +-+ +-+
\|2\|7 + 3\|3
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)
4 7 2 100
x + - x + 30x - ---
3 3
Type: UnivariatePolynomial(x,RealClosure Fraction Integer)
Add some cubic roots
r1 := sqrt(7633)$Ran
+----+
\|7633
Type: RealClosure Fraction Integer
alpha := sqrt(5*r1-436,3)/3
+--------------+
1 3| +----+
- \|5\|7633 - 436
3
Type: RealClosure Fraction Integer
beta := -sqrt(5*r1+436,3)/3
+--------------+
1 3| +----+
- - \|5\|7633 + 436
3
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
5 3
x + 10x + 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)
+-----------+
5| +---+
\|\|153 - 11
Type: RealClosure Fraction Integer
beta2 := -sqrt(r2+11,5)
+-----------+
5| +---+
- \|\|153 + 11
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
+---------+
| +-+ +-+
\|4\|2 + 9 = 2\|2 + 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
+-----------+ +---------+
| +-+ | +-+ +-+
\|- 2\|6 + 5 + \|2\|6 + 5 = 2\|3
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\|- 10\|29 + 55 - 2\|29 + 16 = - \|2\|29 + 11 + \|2\|5 + 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
+--------------------------------+
| +-+ +-+ +-+ +-+ +-+ +-+
\|(34\|2 + 46)\|5 + 70\|2 + 112 = (\|2 + 3)\|5 + 4\|2 + 5
Type: Equation RealClosure Fraction Integer
dst6::Boolean
true
Type: Boolean
f3:Ran:=sqrt(3,5)
5+-+
\|3
Type: RealClosure Fraction Integer
f25:Ran:=sqrt(1/25,5)
+--+
| 1
5|--
\|25
Type: RealClosure Fraction Integer
f32:Ran:=sqrt(32/5,5)
+--+
|32
5|--
\| 5
Type: RealClosure Fraction Integer
f27:Ran:=sqrt(27/5,5)
+--+
|27
5|--
\| 5
Type: RealClosure Fraction Integer
dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)
+---------------+
| +--+ +--+ +--+
| |27 |32 5+-+2 5+-+ | 1
3|- 5|-- + 5|-- = (- \|3 + \|3 + 1) 5|--
\| \| 5 \| 5 \|25
Type: Equation RealClosure Fraction Integer
dst5::Boolean
true
Type: Boolean
See Also: