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 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.
|
|
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
been added to workspace.
Void
These produce values very close to zero.
squareDiff1 := fourSquares(73,548,60,586)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: PositiveInteger
squareDiff2 := fourSquares(165,778,86,990)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: PositiveInteger
squareDiff3 := fourSquares(217,708,226,692)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: Integer
squareDiff4 := fourSquares(155,836,162,820)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: Integer
squareDiff5 := fourSquares(591,772,552,818)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: PositiveInteger
squareDiff6 := fourSquares(434,1053,412,1088)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: PositiveInteger
squareDiff7 := fourSquares(514,1049,446,1152)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: PositiveInteger
squareDiff8 := fourSquares(190,1751,208,1698)
Type: RealClosure Fraction Integer
|
|
Type: Union(RealClosure Fraction Integer,...)
Type: Integer
This should give three digits of precision
relativeApprox(squareDiff8,10**(-3))::Float
|
|
Type: Float
The sum of these 4 roots is 0
l := allRootsOf((x**2-2)**2-2)$Ran
Type: List RealClosure Fraction Integer
Check that they are all roots of the same polynomial
removeDuplicates map(mainDefiningPolynomial,l)
Type:
List Union(SparseUnivariatePolynomial RealClosure Fraction Integer,"failed")
We can see at a glance that they are separate roots
map(mainCharacterization,l)
|
|
Type:
List Union(
RightOpenIntervalRootCharacterization(
RealClosure Fraction Integer,
SparseUnivariatePolynomial RealClosure Fraction Integer),
"failed")
Check the sum and product
[reduce(+,l),reduce(*,l)-2]
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)
Type: RealClosure Fraction Integer
eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)
Type: Equation RealClosure Fraction Integer
Type: Boolean
eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)
Type: Equation RealClosure Fraction Integer
Type: Boolean
Some more examples from J. M. Arnaudies
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
This should be null
Type: RealClosure Fraction Integer
A quartic polynomial
pol : UP(x,Ran) := x**4+(7/3)*x**2+30*x-(100/3)
Type: UnivariatePolynomial(x,RealClosure Fraction Integer)
Add some cubic roots
Type: RealClosure Fraction Integer
alpha := sqrt(5*r1-436,3)/3
Type: RealClosure Fraction Integer
beta := -sqrt(5*r1+436,3)/3
Type: RealClosure Fraction Integer
this should be null
Type: RealClosure Fraction Integer
A quintic polynomial
qol : UP(x,Ran) := x**5+10*x**3+20*x+22
Type: UnivariatePolynomial(x,RealClosure Fraction Integer)
Add some cubic roots
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
this should be null
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
Type: Equation RealClosure Fraction Integer
Type: Boolean
Type: RealClosure Fraction Integer
dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3
Type: Equation RealClosure Fraction Integer
Type: Boolean
Type: RealClosure Fraction Integer
dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) = sqrt(22+2*s5)-sqrt(11+2*s29)+s5
|
|
Type: Equation RealClosure Fraction Integer
Type: Boolean
dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5
|
|
Type: Equation RealClosure Fraction Integer
Type: Boolean
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
Type: RealClosure Fraction Integer
dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)
|
|
Type: Equation RealClosure Fraction Integer
Type: Boolean