Dear all,
for some unknown reason OrderedCompletion R required
R to have OrderedRing rather than OrderedSet to provide
"x < y". Strangely enough, OrderedSet was not even exported.
In order to make FriCAS fit for tropical algebra the attached patch tries
to repair this issue and also adds AbelianMonoid.
I don't know if it makes sense to add other structures at this point.
best,
Franz
Index: src/algebra/complet.spad
===================================================================
--- src/algebra/complet.spad (Revision 2008)
+++ src/algebra/complet.spad (Arbeitskopie)
@@ -17,7 +17,11 @@
++ 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 AbelianMonoid then AbelianMonoid
+ if R has OrderedAbelianGroup then OrderedAbelianGroup
+ if R has OrderedAbelianMonoid then OrderedAbelianMonoid
if R has OrderedRing then OrderedRing
+ if R has OrderedSet then OrderedSet
if R has IntegerNumberSystem then
rational? : % -> Boolean
++ rational?(x) tests if x is a finite rational number.
@@ -60,9 +64,34 @@
y case inf => false
x.fin = y.fin
- if R has AbelianGroup then
+ if R has OrderedSet then
+ 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 AbelianMonoid then
0 == [0$R]
+ 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]
+
+ n : PositiveInteger * x : % ==
+ x case inf =>
+ n > 0 => x
+ error "Undefined product"
+ [n * x.fin]
+
+ if R has AbelianGroup then
n : Integer * x : % ==
x case inf =>
n > 0 => x
@@ -74,13 +103,6 @@
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) -> %
@@ -107,15 +129,6 @@
(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)
@@ -168,6 +181,7 @@
++ finite?(x) tests if x is finite.
infinite? : % -> B
++ infinite?(x) tests if x is infinite.
+ if R has AbelianMonoid then AbelianMonoid
if R has AbelianGroup then AbelianGroup
if R has OrderedRing then OrderedRing
if R has IntegerNumberSystem then
@@ -199,9 +213,16 @@
y case "infinity" => false
x::R = y::R
- if R has AbelianGroup then
+ if R has AbelianMonoid then
0 == 0$R
+ x + y ==
+ x case "infinity" => x
+ y case "infinity" => y
+ x::R + y::R
+
+
+ if R has AbelianGroup then
n : Integer * x : % ==
x case "infinity" =>
zero? n => error "Undefined product"
@@ -212,10 +233,6 @@
x case "infinity" => error "Undefined inverse"
- (x::R)
- x + y ==
- x case "infinity" => x
- y case "infinity" => y
- x::R + y::R
if R has OrderedRing then
fininf : R -> %
