open-axiom repository from github
\documentclass{article}
\usepackage{open-axiom}
\begin{document}
\title{\$SPAD/src/algebra complet.spad}
\author{Manuel Bronstein}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
\section{domain ORDCOMP OrderedCompletion}
<<domain ORDCOMP OrderedCompletion>>=
)abbrev domain ORDCOMP OrderedCompletion
++ Completion with + and - infinity
++ Author: Manuel Bronstein
++ Description: Adjunction of two real infinites quantities to a set.
++ Date Created: 4 Oct 1989
++ Date Last Updated: 1 Nov 1989
OrderedCompletion(R:SetCategory): Exports == Implementation where
B ==> Boolean
Exports ==> 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.
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]
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 =>
positive? n => x
negative? n => [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) ==
positive? r => [b]
negative? r => [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)
@
\section{package ORDCOMP2 OrderedCompletionFunctions2}
<<package ORDCOMP2 OrderedCompletionFunctions2>>=
)abbrev package ORDCOMP2 OrderedCompletionFunctions2
++ Lifting of maps to ordered completions
++ Author: Manuel Bronstein
++ Description: Lifting of maps to ordered completions.
++ Date Created: 4 Oct 1989
++ Date Last Updated: 4 Oct 1989
OrderedCompletionFunctions2(R, S): Exports == Implementation where
R, S: SetCategory
ORR ==> OrderedCompletion R
ORS ==> OrderedCompletion S
Exports ==> with
map: (R -> S, ORR) -> ORS
++ map(f, r) lifts f and applies it to r, assuming that
++ f(plusInfinity) = plusInfinity and that
++ f(minusInfinity) = minusInfinity.
map: (R -> S, ORR, ORS, ORS) -> ORS
++ map(f, r, p, m) lifts f and applies it to r, assuming that
++ f(plusInfinity) = p and that f(minusInfinity) = m.
Implementation ==> add
map(f, r) == map(f, r, plusInfinity(), minusInfinity())
map(f, r, p, m) ==
zero?(n := whatInfinity r) => (f retract r)::ORS
one? n => p
m
@
\section{domain ONECOMP OnePointCompletion}
<<domain ONECOMP OnePointCompletion>>=
)abbrev domain ONECOMP OnePointCompletion
++ Completion with infinity
++ Author: Manuel Bronstein
++ Description: Adjunction of a complex infinity to a set.
++ Date Created: 4 Oct 1989
++ Date Last Updated: 1 Nov 1989
OnePointCompletion(R:SetCategory): Exports == Implementation where
B ==> Boolean
Exports ==> Join(SetCategory, FullyRetractableTo R) with
infinity : () -> %
++ infinity() returns infinity.
finite? : % -> B
++ finite?(x) tests if x is finite.
infinite?: % -> B
++ infinite?(x) tests if x is infinite.
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 is not a rational number.
rationalIfCan: % -> Union(Fraction Integer, "failed")
++ rationalIfCan(x) returns x as a finite rational number if
++ it is one, "failed" otherwise.
Implementation ==> add
Rep := Union(R, "infinity")
coerce(r:R):% == r
retract(x:%):R == (x case R => x::R; error "Not finite")
finite? x == x case R
infinite? x == x case "infinity"
infinity() == "infinity"
retractIfCan(x:%):Union(R, "failed") == (x case R => x::R; "failed")
coerce(x:%):OutputForm ==
x case "infinity" => "infinity"::OutputForm
x::R::OutputForm
x = y ==
x case "infinity" => y case "infinity"
y case "infinity" => false
x::R = y::R
if R has AbelianGroup then
0 == 0$R
n:Integer * x:% ==
x case "infinity" =>
zero? n => error "Undefined product"
infinity()
n * x::R
- x ==
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 -> %
1 == 1$R
characteristic == characteristic$R
fininf r ==
zero? r => error "Undefined product"
infinity()
x:% * y:% ==
x case "infinity" =>
y case "infinity" => y
fininf(y::R)
y case "infinity" => fininf(x::R)
x::R * y::R
recip x ==
x case "infinity" => 0
zero?(x::R) => infinity()
(u := recip(x::R)) case "failed" => "failed"
u::R::%
x < y ==
x case "infinity" => false -- do not change the order
y case "infinity" => true -- of those two tests
x::R < y::R
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)
before?(x,y) ==
x case "infinity" => false
y case "infinity" => true
before?(x::R, y::R)
@
\section{package ONECOMP2 OnePointCompletionFunctions2}
<<package ONECOMP2 OnePointCompletionFunctions2>>=
)abbrev package ONECOMP2 OnePointCompletionFunctions2
++ Lifting of maps to one-point completions
++ Author: Manuel Bronstein
++ Description: Lifting of maps to one-point completions.
++ Date Created: 4 Oct 1989
++ Date Last Updated: 4 Oct 1989
OnePointCompletionFunctions2(R, S): Exports == Implementation where
R, S: SetCategory
OPR ==> OnePointCompletion R
OPS ==> OnePointCompletion S
Exports ==> with
map: (R -> S, OPR) -> OPS
++ map(f, r) lifts f and applies it to r, assuming that
++ f(infinity) = infinity.
map: (R -> S, OPR, OPS) -> OPS
++ map(f, r, i) lifts f and applies it to r, assuming that
++ f(infinity) = i.
Implementation ==> add
map(f, r) == map(f, r, infinity())
map(f, r, i) ==
(u := retractIfCan r) case R => (f(u::R))::OPS
i
@
\section{package INFINITY Infinity}
<<package INFINITY Infinity>>=
)abbrev package INFINITY Infinity
++ Top-level infinity
++ Author: Manuel Bronstein
++ Description: Default infinity signatures for the interpreter;
++ Date Created: 4 Oct 1989
++ Date Last Updated: 4 Oct 1989
Infinity(): with
infinity : () -> OnePointCompletion Integer
++ infinity() returns infinity.
plusInfinity : () -> OrderedCompletion Integer
++ plusInfinity() returns plusIinfinity.
minusInfinity: () -> OrderedCompletion Integer
++ minusInfinity() returns minusInfinity.
== add
infinity() == infinity()$OnePointCompletion(Integer)
plusInfinity() == plusInfinity()$OrderedCompletion(Integer)
minusInfinity() == minusInfinity()$OrderedCompletion(Integer)
@
\section{License}
<<license>>=
--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
-- - Redistributions of source code must retain the above copyright
-- notice, this list of conditions and the following disclaimer.
--
-- - Redistributions in binary form must reproduce the above copyright
-- notice, this list of conditions and the following disclaimer in
-- the documentation and/or other materials provided with the
-- distribution.
--
-- - Neither the name of The Numerical ALgorithms Group Ltd. nor the
-- names of its contributors may be used to endorse or promote products
-- derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
@
<<*>>=
<<license>>
<<domain ORDCOMP OrderedCompletion>>
<<package ORDCOMP2 OrderedCompletionFunctions2>>
<<domain ONECOMP OnePointCompletion>>
<<package ONECOMP2 OnePointCompletionFunctions2>>
<<package INFINITY Infinity>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}