$SPAD/src/input reclos.input

John Abbot and Timothy Daly

December 3, 2016

Abstract

Contents

1 License

— license —

--Copyright The Numerical Algorithms Group Limited 1991.

———-

— * —

)set break resume
)spool reclos.output
)set message test on
)set message auto off
)clear all
--S 1 of 70
Ran := RECLOS(FRAC INT)
--R
--R
--R   (1)  RealClosure(Fraction(Integer))
--R                                                                 Type: Domain
--E 1

———-

Some simple signs for square roots, these correspond to an extension of degree 16 of the rational numbers. these examples were given to me by J. Abbot

— * —

--S 2 of 70
fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran == sqrt(a)+sqrt(b) - sqrt(c)-sqrt(d)
--R
--R   Function declaration fourSquares : (RealClosure(Fraction(Integer)),
--R      RealClosure(Fraction(Integer)),RealClosure(Fraction(Integer)),
--R      RealClosure(Fraction(Integer))) -> RealClosure(Fraction(Integer))
--R      has been added to workspace.
--R                                                                   Type: Void
--E 2
--S 3 of 70
squareDiff1 := fourSquares(73,548,60,586)
--R
--R   Compiling function fourSquares with type (RealClosure(Fraction(
--R      Integer)),RealClosure(Fraction(Integer)),RealClosure(Fraction(
--R      Integer)),RealClosure(Fraction(Integer))) -> RealClosure(Fraction
--R      (Integer))
--R

--R           +---+    +--+    +---+    +--+
--R   (3)  - \|586  - \|60  + \|548  + \|73
--R                                         Type: RealClosure(Fraction(Integer))
--E 3
--S 4 of 70
recip(squareDiff1)
--R
--R
--R   (4)
--R             +---+          +--+  +--+         +--+ +---+            +---+
--R     ((54602\|548  + 149602\|73 )\|60  + 49502\|73 \|548  + 9900895)\|586
--R   +
--R             +--+ +---+             +--+            +---+            +--+
--R     (154702\|73 \|548  + 30941947)\|60  + 10238421\|548  + 28051871\|73
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 4
--S 5 of 70
sign(squareDiff1)
--R
--R
--R   (5)  1
--R                                                        Type: PositiveInteger
--E 5
--S 6 of 70
squareDiff2 := fourSquares(165,778,86,990)
--R
--R
--R           +---+    +--+    +---+    +---+
--R   (6)  - \|990  - \|86  + \|778  + \|165
--R                                         Type: RealClosure(Fraction(Integer))
--E 6
--S 7 of 70
recip(squareDiff2)
--R
--R
--R   (7)
--R                +---+           +---+  +--+          +---+ +---+
--R       ((556778\|778  + 1209010\|165 )\|86  + 401966\|165 \|778  + 144019431)
--R    *
--R        +---+
--R       \|990
--R   +
--R              +---+ +---+              +--+             +---+             +---+
--R     (1363822\|165 \|778  + 488640503)\|86  + 162460913\|778  + 352774119\|165
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 7

--S 8 of 70
sign(squareDiff2)
--R
--R
--R   (8)  1
--R                                                        Type: PositiveInteger
--E 8
--S 9 of 70
squareDiff3 := fourSquares(217,708,226,692)
--R
--R
--R           +---+    +---+    +---+    +---+
--R   (9)  - \|692  - \|226  + \|708  + \|217
--R                                         Type: RealClosure(Fraction(Integer))
--E 9
--S 10 of 70
recip(squareDiff3)
--R
--R
--R   (10)
--R               +---+         +---+  +---+         +---+ +---+             +---+
--R     ((- 34102\|708  - 61598\|217 )\|226  - 34802\|217 \|708  - 13641141)\|692
--R   +
--R              +---+ +---+             +---+            +---+            +---+
--R     (- 60898\|217 \|708  - 23869841)\|226  - 13486123\|708  - 24359809\|217
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 10
--S 11 of 70
sign(squareDiff3)
--R
--R
--R   (11)  - 1
--R                                                                Type: Integer
--E 11
--S 12 of 70
squareDiff4 := fourSquares(155,836,162,820)
--R
--R
--R            +---+    +---+    +---+    +---+
--R   (12)  - \|820  - \|162  + \|836  + \|155
--R                                         Type: RealClosure(Fraction(Integer))
--E 12
--S 13 of 70
recip(squareDiff4)

--R
--R
--R   (13)
--R               +---+         +---+  +---+         +---+ +---+             +---+
--R     ((- 37078\|836  - 86110\|155 )\|162  - 37906\|155 \|836  - 13645107)\|820
--R   +
--R              +---+ +---+             +---+            +---+            +---+
--R     (- 85282\|155 \|836  - 30699151)\|162  - 13513901\|836  - 31384703\|155
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 13
--S 14 of 70
sign(squareDiff4)
--R
--R
--R   (14)  - 1
--R                                                                Type: Integer
--E 14
--S 15 of 70
squareDiff5 := fourSquares(591,772,552,818)
--R
--R
--R            +---+    +---+    +---+    +---+
--R   (15)  - \|818  - \|552  + \|772  + \|591
--R                                         Type: RealClosure(Fraction(Integer))
--E 15
--S 16 of 70
recip(squareDiff5)
--R
--R
--R   (16)
--R             +---+         +---+  +---+         +---+ +---+             +---+
--R     ((70922\|772  + 81058\|591 )\|552  + 68542\|591 \|772  + 46297673)\|818
--R   +
--R            +---+ +---+             +---+            +---+            +---+
--R     (83438\|591 \|772  + 56359389)\|552  + 47657051\|772  + 54468081\|591
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 16
--S 17 of 70
sign(squareDiff5)
--R
--R
--R   (17)  1
--R                                                        Type: PositiveInteger
--E 17
--S 18 of 70

squareDiff6 := fourSquares(434,1053,412,1088)
--R
--R
--R            +----+    +---+    +----+    +---+
--R   (18)  - \|1088  - \|412  + \|1053  + \|434
--R                                         Type: RealClosure(Fraction(Integer))
--E 18
--S 19 of 70
recip(squareDiff6)
--R
--R
--R   (19)
--R                +----+          +---+  +---+          +---+ +----+
--R       ((115442\|1053  + 179818\|434 )\|412  + 112478\|434 \|1053  + 76037291)
--R    *
--R        +----+
--R       \|1088
--R   +
--R           +---+ +----+              +---+            +----+             +---+
--R   (182782\|434 \|1053  + 123564147)\|412  + 77290639\|1053  + 120391609\|434
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 19
--S 20 of 70
sign(squareDiff6)
--R
--R
--R   (20)  1
--R                                                        Type: PositiveInteger
--E 20
--S 21 of 70
squareDiff7 := fourSquares(514,1049,446,1152)
--R
--R
--R            +----+    +---+    +----+    +---+
--R   (21)  - \|1152  - \|446  + \|1049  + \|514
--R                                         Type: RealClosure(Fraction(Integer))
--E 21
--S 22 of 70
recip(squareDiff7)
--R
--R
--R   (22)
--R                +----+          +---+  +---+          +---+ +----+
--R       ((349522\|1049  + 499322\|514 )\|446  + 325582\|514 \|1049  + 239072537)
--R    *
--R        +----+

--R       \|1152
--R   +
--R           +---+ +----+              +---+             +----+             +---+
--R   (523262\|514 \|1049  + 384227549)\|446  + 250534873\|1049  + 357910443\|514
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 22
--S 23 of 70
sign(squareDiff7)
--R
--R
--R   (23)  1
--R                                                        Type: PositiveInteger
--E 23
--S 24 of 70
squareDiff8 := fourSquares(190,1751,208,1698)
--R
--R
--R            +----+    +---+    +----+    +---+
--R   (24)  - \|1698  - \|208  + \|1751  + \|190
--R                                         Type: RealClosure(Fraction(Integer))
--E 24
--S 25 of 70
recip(squareDiff8)
--R
--R
--R   (25)
--R                     +----+          +---+  +---+          +---+ +----+
--R           (- 214702\|1751  - 651782\|190 )\|208  - 224642\|190 \|1751
--R         +
--R           - 129571901
--R    *
--R        +----+
--R       \|1698
--R   +
--R               +---+ +----+              +---+             +----+
--R     (- 641842\|190 \|1751  - 370209881)\|208  - 127595865\|1751
--R   +
--R                 +---+
--R     - 387349387\|190
--R                              Type: Union(RealClosure(Fraction(Integer)),...)
--E 25
--S 26 of 70
sign(squareDiff8)
--R
--R
--R   (26)  - 1

--R                                                                Type: Integer
--E 26
--S 27 of 70
relativeApprox(squareDiff8,10**(-3))::Float
--R
--R
--R   (27)  - 0.2340527771 5937700123 E -10
--R                                                                  Type: Float
--E 27

———-

Test the Renaud Rioboo fix (Jan 2004)

— * —

--S 28 of 70
allRootsOf((x-2)*(x-3)*(x-4))$RECLOS(FRAC INT)
--R
--R
--R   (28)  [2,3,4]
--R                                   Type: List(RealClosure(Fraction(Integer)))
--E 28

———-

Check out if the sum of all roots is null. Example from P.V. Koseleff — * —

--S 29 of 70
l := allRootsOf((x**2-2)**2-2)$Ran
--R
--R
--R   (29)  [%A33,%A34,%A35,%A36]
--R                                   Type: List(RealClosure(Fraction(Integer)))
--E 29
--S 30 of 70
l.1+l.2+l.3+l.4
--R
--R
--R   (30)  0
--R                                         Type: RealClosure(Fraction(Integer))
--E 30
--S 31 of 70
removeDuplicates map(mainDefiningPolynomial,l)
--R
--R
--R           4     2
--R   (31)  [?  - 4?  + 2]

--RType: List(Union(SparseUnivariatePolynomial(RealClosure(Fraction(Integer))),"failed"))
--E 31
--S 32 of 70
map(mainCharacterization,l)
--R
--R
--R   (32)  [[- 2,- 1[,[- 1,0[,[0,1[,[1,2[]
--RType: List(Union(RightOpenIntervalRootCharacterization(RealClosure(Fraction(Integer)),SparseUnivariatePolynomial(RealClosure(Fraction(Integer)))),"failed"))
--E 32
--S 33 of 70
[reduce(+,l),reduce(*,l)-2]
--R
--R
--R   (33)  [0,0]
--R                                   Type: List(RealClosure(Fraction(Integer)))
--E 33

———-

A more complicated test that involve an extension of degree 256 example by prof Kahan at ISSAC’92

— * —

)cl prop s2 s5 10
--S 34 of 70
(s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran)
--R
--R
--R          +--+
--R   (34)  \|10
--R                                         Type: RealClosure(Fraction(Integer))
--E 34
--S 35 of 70
eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)
--R
--R
--R            +---------+ +--------+    +---------+ +--------+   +-----------+
--R            | +--+      | +-+         | +--+      | +-+        |   +-+
--R   (35)  - \|\|10  - 3 \|\|5  - 2  + \|\|10  + 3 \|\|5  + 2 = \|10\|2  + 10
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 35
--S 36 of 70
eq1::Boolean
--R
--R

--R   (36)  true
--R                                                                Type: Boolean
--E 36

———-

Analogous one by [rr] — * —

--S 37 of 70
eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)
--R
--R
--R            +--------+ +--------+    +--------+ +--------+   +----------+
--R            | +-+      | +-+         | +-+      | +-+        |  +--+
--R   (37)  - \|\|5  - 2 \|\|2  - 1  + \|\|5  + 2 \|\|2  + 1 = \|2\|10  + 2
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 37
--S 38 of 70
eq2::Boolean
--R
--R
--R   (38)  true
--R                                                                Type: Boolean
--E 38

———-

These came from J.M. Arnaudies — * —

)cl prop s4 s7 e1 e2
--S 39 of 70
s3 := sqrt(3)$Ran
--R
--R
--R          +-+
--R   (39)  \|3
--R                                         Type: RealClosure(Fraction(Integer))
--E 39
--S 40 of 70
s7:= sqrt(7)$Ran
--R
--R
--R          +-+
--R   (40)  \|7
--R                                         Type: RealClosure(Fraction(Integer))

--E 40
--S 41 of 70
e1 := sqrt(2*s7-3*s3,3)
--R
--R
--R          +-------------+
--R         3|  +-+     +-+
--R   (41)  \|2\|7  - 3\|3
--R                                         Type: RealClosure(Fraction(Integer))
--E 41
--S 42 of 70
e2 := sqrt(2*s7+3*s3,3)
--R
--R
--R          +-------------+
--R         3|  +-+     +-+
--R   (42)  \|2\|7  + 3\|3
--R                                         Type: RealClosure(Fraction(Integer))
--E 42

———-

This should be null — * —

--S 43 of 70
ee1:=e2-e1=s3
--R
--R
--R          +-------------+    +-------------+
--R         3|  +-+     +-+    3|  +-+     +-+    +-+
--R   (43)  \|2\|7  + 3\|3   - \|2\|7  - 3\|3  = \|3
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 43
--S 44 of 70
ee1::Boolean
--R
--R
--R   (44)  true
--R                                                                Type: Boolean
--E 44
)cl prop pol r1 alpha beta
--S 45 of 70
pol : UP(x,Ran) := x**4+(7/3)*x**2+30*x-(100/3)
--R

--R
--R          4   7  2         100
--R   (45)  x  + - x  + 30x - ---
--R              3             3
--R                 Type: UnivariatePolynomial(x,RealClosure(Fraction(Integer)))
--E 45
--S 46 of 70
r1 := sqrt(7633)$Ran
--R
--R
--R          +----+
--R   (46)  \|7633
--R                                         Type: RealClosure(Fraction(Integer))
--E 46

———-

Cubic roots — * —

--S 47 of 70
alpha := sqrt(5*r1-436,3)/3
--R
--R
--R            +--------------+
--R         1 3|  +----+
--R   (47)  - \|5\|7633  - 436
--R         3
--R                                         Type: RealClosure(Fraction(Integer))
--E 47
--S 48 of 70
beta := -sqrt(5*r1+436,3)/3
--R
--R
--R              +--------------+
--R           1 3|  +----+
--R   (48)  - - \|5\|7633  + 436
--R           3
--R                                         Type: RealClosure(Fraction(Integer))
--E 48

———-

This should be null — * —

--S 49 of 70
pol.(alpha+beta-1/3)

--R
--R
--R   (49)  0
--R                                         Type: RealClosure(Fraction(Integer))
--E 49
)cl prop qol r2 alpha beta
--S 50 of 70
r2 := sqrt(153)$Ran
--R
--R
--R          +---+
--R   (50)  \|153
--R                                         Type: RealClosure(Fraction(Integer))
--E 50

———-

Roots of order 5 — * —

--S 51 of 70
alpha2 := sqrt(r2-11,5)
--R
--R
--R          +-----------+
--R         5| +---+
--R   (51)  \|\|153  - 11
--R                                         Type: RealClosure(Fraction(Integer))
--E 51
--S 52 of 70
beta2 := -sqrt(r2+11,5)
--R
--R
--R            +-----------+
--R           5| +---+
--R   (52)  - \|\|153  + 11
--R                                         Type: RealClosure(Fraction(Integer))
--E 52
--S 53 of 70
qol : UP(x,Ran) := x**5+10*x**3+20*x+22
--R
--R
--R          5      3
--R   (53)  x  + 10x  + 20x + 22
--R                 Type: UnivariatePolynomial(x,RealClosure(Fraction(Integer)))
--E 53

--S 54 of 70
qol(alpha2+beta2)
--R
--R
--R   (54)  0
--R                                         Type: RealClosure(Fraction(Integer))
--E 54
--S 55 of 70
dst1:=sqrt(9+4*s2)=1+2*s2
--R
--R
--R          +---------+
--R          |  +-+         +-+
--R   (55)  \|4\|2  + 9 = 2\|2  + 1
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 55
--S 56 of 70
dst1::Boolean
--R
--R
--R   (56)  true
--R                                                                Type: Boolean
--E 56
--S 57 of 70
s6:Ran:=sqrt 6
--R
--R
--R          +-+
--R   (57)  \|6
--R                                         Type: RealClosure(Fraction(Integer))
--E 57
--S 58 of 70
dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3
--R
--R
--R          +-----------+    +---------+
--R          |    +-+         |  +-+         +-+
--R   (58)  \|- 2\|6  + 5  + \|2\|6  + 5 = 2\|3
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 58
--S 59 of 70
dst2::Boolean
--R
--R

--S 60 of 70
s29:Ran:=sqrt 29
--R
--R
--R          +--+
--R   (60)  \|29
--R                                         Type: RealClosure(Fraction(Integer))
--E 60
--S 61 of 70
dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) = sqrt(22+2*s5)-sqrt(11+2*s29)+s5
--R
--R
--R   (61)
--R    +--------------------------------+
--R    |  +--------------+                    +-----------+    +----------+
--R    |  |     +--+           +--+           |  +--+          |  +-+          +-+
--R   \|2\|- 10\|29  + 55  - 2\|29  + 16 = - \|2\|29  + 11  + \|2\|5  + 22  + \|5
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 61
--S 62 of 70
dst4::Boolean
--R
--R
--R   (62)  true
--R                                                                Type: Boolean
--E 62
--S 63 of 70
dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5
--R
--R
--R          +--------------------------------+
--R          |    +-+       +-+      +-+           +-+      +-+     +-+
--R   (63)  \|(34\|2  + 46)\|5  + 70\|2  + 112 = (\|2  + 3)\|5  + 4\|2  + 5
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 63
--S 64 of 70
dst6::Boolean
--R
--R
--R   (64)  true
--R                                                                Type: Boolean
--E 64

--S 65 of 70
f3:Ran:=sqrt(3,5)
--R
--R
--R         5+-+
--R   (65)  \|3
--R                                         Type: RealClosure(Fraction(Integer))
--E 65
--S 66 of 70
f25:Ran:=sqrt(1/25,5)
--R
--R
--R          +--+
--R          | 1
--R   (66)  5|--
--R         \|25
--R                                         Type: RealClosure(Fraction(Integer))
--E 66
--S 67 of 70
f32:Ran:=sqrt(32/5,5)
--R
--R
--R          +--+
--R          |32
--R   (67)  5|--
--R         \| 5
--R                                         Type: RealClosure(Fraction(Integer))
--E 67
--S 68 of 70
f27:Ran:=sqrt(27/5,5)
--R
--R
--R          +--+
--R          |27
--R   (68)  5|--
--R         \| 5
--R                                         Type: RealClosure(Fraction(Integer))
--E 68
--S 69 of 70
dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)
--R
--R
--R          +---------------+
--R          |   +--+    +--+                         +--+
--R          |   |27     |32       5+-+2   5+-+       | 1

--R   (69)  3|- 5|--  + 5|--  = (- \|3   + \|3  + 1) 5|--
--R         \|  \| 5    \| 5                         \|25
--R                               Type: Equation(RealClosure(Fraction(Integer)))
--E 69
--S 70 of 70
dst5::Boolean
--R
--R
--R   (70)  true
--R                                                                Type: Boolean
--E 70
)spool
)lisp (bye)

———-

References^{[1] nothing}

18