/usr/share/axiom-20170501/src/algebra/ORDCOMP.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | )abbrev domain ORDCOMP OrderedCompletion
++ Author: Manuel Bronstein
++ Date Created: 4 Oct 1989
++ Date Last Updated: 1 Nov 1989
++ Description:
++ Completion with + and - infinity.
++ Adjunction of two real infinites quantities to a set.
OrderedCompletion(R) : SIG == CODE where
R : SetCategory
B ==> Boolean
SIG ==> Join(SetCategory, FullyRetractableTo R) with
plusInfinity : () -> %
++ plusInfinity() returns +infinity.
minusInfinity: () -> %
++ minusInfinity() returns -infinity.
finite? : % -> B
++ finite?(x) tests if x is finite.
infinite? : % -> B
++ infinite?(x) tests if x is +infinity or -infinity,
whatInfinity : % -> SingleInteger
++ whatInfinity(x) returns 0 if x is finite,
++ 1 if x is +infinity, and -1 if x is -infinity.
if R has AbelianGroup then AbelianGroup
if R has OrderedRing then OrderedRing
if R has IntegerNumberSystem then
rational? : % -> Boolean
++ rational?(x) tests if x is a finite rational number.
rational : % -> Fraction Integer
++ rational(x) returns x as a finite rational number.
++ Error: if x cannot be so converted.
rationalIfCan : % -> Union(Fraction Integer, "failed")
++ rationalIfCan(x) returns x as a finite rational number if
++ it is one and "failed" otherwise.
CODE ==> add
Rep := Union(fin:R, inf:B) -- true = +infinity, false = -infinity
coerce(r:R):% == [r]
retract(x:%):R == (x case fin => x.fin; error "Not finite")
finite? x == x case fin
infinite? x == x case inf
plusInfinity() == [true]
minusInfinity() == [false]
retractIfCan(x:%):Union(R, "failed") ==
x case fin => x.fin
"failed"
coerce(x:%):OutputForm ==
x case fin => (x.fin)::OutputForm
e := "infinity"::OutputForm
x.inf => empty() + e
- e
whatInfinity x ==
x case fin => 0
x.inf => 1
-1
x = y ==
x case inf =>
y case inf => not xor(x.inf, y.inf)
false
y case inf => false
x.fin = y.fin
if R has AbelianGroup then
0 == [0$R]
n:Integer * x:% ==
x case inf =>
n > 0 => x
n < 0 => [not(x.inf)]
error "Undefined product"
[n * x.fin]
- x ==
x case inf => [not(x.inf)]
[- (x.fin)]
x + y ==
x case inf =>
y case fin => x
xor(x.inf, y.inf) => error "Undefined sum"
x
y case inf => y
[x.fin + y.fin]
if R has OrderedRing then
fininf: (B, R) -> %
1 == [1$R]
characteristic() == characteristic()$R
fininf(b, r) ==
r > 0 => [b]
r < 0 => [not b]
error "Undefined product"
x:% * y:% ==
x case inf =>
y case inf =>
xor(x.inf, y.inf) => minusInfinity()
plusInfinity()
fininf(x.inf, y.fin)
y case inf => fininf(y.inf, x.fin)
[x.fin * y.fin]
recip x ==
x case inf => 0
(u := recip(x.fin)) case "failed" => "failed"
[u::R]
x < y ==
x case inf =>
y case inf =>
xor(x.inf, y.inf) => y.inf
false
not(x.inf)
y case inf => y.inf
x.fin < y.fin
if R has IntegerNumberSystem then
rational? x == finite? x
rational x == rational(retract(x)@R)
rationalIfCan x ==
(r:= retractIfCan(x)@Union(R,"failed")) case "failed" =>"failed"
rational(r::R)
|