aboutsummaryrefslogtreecommitdiff
path: root/src/hyper/pages/RECLOS.ht
blob: 02f1145eda49525207df919b0668de9f73683685 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
% Copyright The Numerical Algorithms Group Limited 1992-94. All rights reserved.
% !! DO NOT MODIFY THIS FILE BY HAND !! Created by ht.awk.
\newcommand{\RealClosureXmpTitle}{RealClosure}
\newcommand{\RealClosureXmpNumber}{9.66}
%
% =====================================================================
\begin{page}{RealClosureXmpPage}{9.66 RealClosure}
% =====================================================================
\beginscroll


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

\begin{items}
\item The package \axiomType{RealPolynomialUtilitiesPackage} which needs a \axiomType{Field} {\em F} and a
\axiomType{UnivariatePolynomialCategory} domain with coefficients in {\em F}. It computes some
simple functions such as Sturm and Sylvester sequences 
(\axiomOpFrom{sturmSequence}{RealPolynomialUtilitiesPackage}, 
\axiomOpFrom{sylvesterSequence}{RealPolynomialUtilitiesPackage}).

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

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

\item The domain \axiomType{RightOpenIntervalRootCharacterization} is the main code that
provides the functionality of \axiomType{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.

\item  The \axiomType{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
(\axiomOpFrom{approximate}{RealClosure}) or relative (\axiomOpFrom{relativeApprox}{RealClosure}).


\end{items}

\centerline{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 \spad{sqrt(2) + sqrt(2)} you have two
new variables which happen to be equal. To avoid this name the expression such
as in \spad{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.

\centerline{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 excatly. They can thus be quite time consuming when
depending on several "real roots".

\centerline{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.

\centerline{EXAMPLES}
\xtc{
We shall work with the real closure of the ordered field of 
rational numbers.
}{
\spadpaste{Ran := RECLOS(FRAC INT) \bound{Ran}}
}
\xtc{
Some simple signs for square roots, these correspond to an extension
of degree 16 of the rational numbers. Examples provided by J. Abbot.
}{
\spadpaste{fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran == sqrt(a)+sqrt(b) - sqrt(c)-sqrt(d) \free{Ran} \bound{fs}}
}
\xtc{
These produce values very close to zero.
}{
\spadpaste{squareDiff1 := fourSquares(73,548,60,586) \free{fs}\bound{sd1}}
}
\xtc{
}{
\spadpaste{recip(squareDiff1)\free{sd1}}
}
\xtc{
}{
\spadpaste{sign(squareDiff1)\free{sd1}}
}
\xtc{
}{
\spadpaste{squareDiff2 := fourSquares(165,778,86,990) \free{fs}\bound{sd2}}
}
\xtc{
}{
\spadpaste{recip(squareDiff2)\free{sd2}}
}
\xtc{
}{
\spadpaste{sign(squareDiff2)\free{sd2}}
}
\xtc{
}{
\spadpaste{squareDiff3 := fourSquares(217,708,226,692) \free{fs}\bound{sd3}}
}
\xtc{
}{
\spadpaste{recip(squareDiff3)\free{sd3}}
}
\xtc{
}{
\spadpaste{sign(squareDiff3)\free{sd3}}
}
\xtc{
}{
\spadpaste{squareDiff4 := fourSquares(155,836,162,820)  \free{fs}\bound{sd4}}
}
\xtc{
}{
\spadpaste{recip(squareDiff4)\free{sd4}}
}
\xtc{
}{
\spadpaste{sign(squareDiff4)\free{sd4}}
}
\xtc{
}{
\spadpaste{squareDiff5 := fourSquares(591,772,552,818) \free{fs}\bound{sd5}}
}
\xtc{
}{
\spadpaste{recip(squareDiff5)\free{sd5}}
}
\xtc{
}{
\spadpaste{sign(squareDiff5)\free{sd5}}
}
\xtc{
}{
\spadpaste{squareDiff6 := fourSquares(434,1053,412,1088) \free{fs}\bound{sd6}}
}
\xtc{
}{
\spadpaste{recip(squareDiff6)\free{sd6}}
}
\xtc{
}{
\spadpaste{sign(squareDiff6)\free{sd6}}
}
\xtc{
}{
\spadpaste{squareDiff7 := fourSquares(514,1049,446,1152) \free{fs}\bound{sd7}}
}
\xtc{
}{
\spadpaste{recip(squareDiff7)\free{sd7}}
}
\xtc{
}{
\spadpaste{sign(squareDiff7)\free{sd7}}
}
\xtc{
}{
\spadpaste{squareDiff8 := fourSquares(190,1751,208,1698) \free{fs}\bound{sd8}}
}
\xtc{
}{
\spadpaste{recip(squareDiff8)\free{sd8}}
}
\xtc{
}{
\spadpaste{sign(squareDiff8)\free{sd8}}
}
\xtc{
This should give three digits of precision
}{
\spadpaste{relativeApprox(squareDiff8,10**(-3))::Float \free{sd8}}
}
\xtc{
The sum of these 4 roots is 0
}{
\spadpaste{l := allRootsOf((x**2-2)**2-2)$Ran \free{Ran} \bound{l}}
}
\xtc{
Check that they are all roots of the same polynomial
}{
\spadpaste{removeDuplicates map(mainDefiningPolynomial,l) \free{l}}
}
\xtc{
We can see at a glance that they are separate roots
}{
\spadpaste{map(mainCharacterization,l) \free{l}}
}
\xtc{
Check the sum and product
}{
\spadpaste{[reduce(+,l),reduce(*,l)-2] \free{l}}
}
\xtc{
A more complicated test that involve an extension of degree 256.
This is a way of checking nested radical identities.
}{
\spadpaste{(s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran) \free{Ran}\bound{s2}\bound{s5}\bound{s10}}
}
\xtc{
}{
\spadpaste{eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10) \free{s2}\free{s5}\free{s10}\bound{eq1}}
}
\xtc{
}{
\spadpaste{eq1::Boolean \free{eq1}}
}
\xtc{
}{
\spadpaste{eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)\free{s2}\free{s5}\free{s10}\bound{eq2}}
}
\xtc{
}{
\spadpaste{eq2::Boolean \free{eq2}}
}
\xtc{
Some more examples from J. M. Arnaudies
}{
\spadpaste{s3 := sqrt(3)$Ran \free{Ran}\bound{s3}}
}
\xtc{
}{
\spadpaste{s7:= sqrt(7)$Ran \free{Ran}\bound{s7}}
}
\xtc{
}{
\spadpaste{e1 := sqrt(2*s7-3*s3,3) \free{s7} \free{s3} \bound{e1}}
}
\xtc{
}{
\spadpaste{e2 := sqrt(2*s7+3*s3,3) \free{s7} \free{s3} \bound{e2}}
}
\xtc{
This should be null
}{
\spadpaste{e2-e1-s3 \free{e2} \free{e1} \free{s3}}
}
\xtc{
A quartic polynomial
}{
\spadpaste{pol : UP(x,Ran) := x**4+(7/3)*x**2+30*x-(100/3) \free{Ran} \bound{pol}}
}
\xtc{
Add some cubic roots
}{
\spadpaste{r1 := sqrt(7633)$Ran \free{Ran}\bound{r1}}
}
\xtc{
}{
\spadpaste{alpha := sqrt(5*r1-436,3)/3 \free{r1} \bound{alpha}}
}
\xtc{
}{
\spadpaste{beta := -sqrt(5*r1+436,3)/3 \free{r1} \bound{beta}}
}
\xtc{
this should be null
}{
\spadpaste{pol.(alpha+beta-1/3) \free{pol} \free{alpha} \free{beta}}
}
\xtc{
A quintic polynomial
}{
\spadpaste{qol : UP(x,Ran) := x**5+10*x**3+20*x+22 \free{Ran}\bound{qol}}
}
\xtc{
Add some cubic roots
}{
\spadpaste{r2 := sqrt(153)$Ran \free{Ran}\bound{r2}}
}
\xtc{
}{
\spadpaste{alpha2 := sqrt(r2-11,5) \free{r2}\bound{alpha2}}
}
\xtc{
}{
\spadpaste{beta2 := -sqrt(r2+11,5) \free{r2}\bound{beta2}}
}
\xtc{
this should be null
}{
\spadpaste{qol(alpha2+beta2) \free{qol}\free{alpha2}\free{beta2}}
}
\xtc{
Finally, some examples from the book Computer Algebra by 
Davenport, Siret and Tournier (page 77).
The last one is due to Ramanujan.
}{
\spadpaste{dst1:=sqrt(9+4*s2)=1+2*s2 \free{s2}\bound{dst1}}
}
\xtc{
}{
\spadpaste{dst1::Boolean \free{dst1}}
}
\xtc{
}{
\spadpaste{s6:Ran:=sqrt 6 \free{Ran}\bound{s6}}
}
\xtc{
}{
\spadpaste{dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3 \free{s6}\free{s3}\bound{dst2}}
}
\xtc{
}{
\spadpaste{dst2::Boolean \free{dst2}}
}
\xtc{
}{
\spadpaste{s29:Ran:=sqrt 29 \free{Ran}\bound{s29}}
}
\xtc{
}{
\spadpaste{dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) = sqrt(22+2*s5)-sqrt(11+2*s29)+s5 \free{s29}\free{s5}\bound{dst4}}
}
\xtc{
}{
\spadpaste{dst4::Boolean \free{dst4}}
}
\xtc{
}{
\spadpaste{dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5 \free{s2}\free{s5}\bound{dst6}}
}
\xtc{
}{
\spadpaste{dst6::Boolean \free{dst6}}
}
\xtc{
}{
\spadpaste{f3:Ran:=sqrt(3,5) \free{Ran}\bound{f3}}
}
\xtc{
}{
\spadpaste{f25:Ran:=sqrt(1/25,5) \free{Ran}\bound{f25}}
}
\xtc{
}{
\spadpaste{f32:Ran:=sqrt(32/5,5) \free{Ran}\bound{f32}}
}
\xtc{
}{
\spadpaste{f27:Ran:=sqrt(27/5,5) \free{Ran}\bound{f27}}
}
\xtc{
}{
\spadpaste{dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)\free{f32}\free{f27}\free{f25}\free{f3}\bound{dst5}}
}
\xtc{
}{
\spadpaste{dst5::Boolean \free{dst5}}
}

\endscroll
\autobuttons
\end{page}
%