==================================================================== Real Closure ==================================================================== 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). ------- 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 ----------- 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``. ---------- REFERENCES ---------- .. [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. -------- EXAMPLES -------- 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: * )help RightOpenIntervalRootCharacterization * )help RealClosedField * )help RealRootCharacterizationCategory * )help UnivariatePolynomialCategory * )help Field * )help RealPolynomialUtilitiesPackage * )show RealClosure