On Wed, 31 Aug 2016, Waldek Hebisch wrote:
I have now adjusted algebra so that it compiles with minimal
structure on completition.
thanks. My local solution was "LeftCompletion" and "RightCompletion"
(see attachment). Does it still make sense to include it?
best,
Franz
)abbrev domain LCOMP LeftCompletion
++ Completion with - infinity
++ Author: Franz Lehner
++ Description: Adjunction of negative real infinite quantity to a set.
++ Date Created: 24 Aug 2016
LeftCompletion(R : SetCategory) : Exports == Implementation where
B ==> Boolean
Exports ==> Join(SetCategory, FullyRetractableTo R) with
minusInfinity : () -> % ++ minusInfinity() returns -infinity.
finite? : % -> B
++ finite?(x) tests if x is finite.
infinite? : % -> B
++ infinite?(x) tests if x is -infinity,
if R has OrderedSet then OrderedSet
if R has OrderedAbelianMonoid then OrderedAbelianMonoid
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.
Implementation ==> 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
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
- e
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 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 OrderedAbelianMonoid then
0 == [0$R]
x + y ==
x case inf => x
y case inf => y
[x.fin + y.fin]
n : NonNegativeInteger * x : % ==
x case inf => x
[n * x.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)
)abbrev domain RCOMP RightCompletion
++ Completion with - infinity
++ Author: Franz Lehner
++ Description: Adjunction of positive real infinite quantity to a set.
++ Date Created: 24 Aug 2016
RightCompletion(R : SetCategory) : Exports == Implementation where
B ==> Boolean
Exports ==> Join(SetCategory, FullyRetractableTo R) with
plusInfinity : () -> % ++ plusInfinity() returns +infinity.
finite? : % -> B
++ finite?(x) tests if x is finite.
infinite? : % -> B
++ infinite?(x) tests if x is +infinity or -infinity,
if R has OrderedSet then OrderedSet
if R has OrderedAbelianMonoid then OrderedAbelianMonoid
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.
Implementation ==> 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]
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
x = y ==
x case inf =>
y case inf => true
false
y case inf => false
x.fin = y.fin
if R has OrderedSet then
x < y ==
x case inf => false
y case inf => true
x.fin < y.fin
if R has AbelianMonoid then
0 == [0$R]
x + y ==
x case inf => x
y case inf => y
[x.fin + y.fin]
n : NonNegativeInteger * x : % ==
x case inf => x
[n * x.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)
