\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} <>= )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} <>= )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} <>= )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} <>= )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} <>= )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} <>= --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. @ <<*>>= <> <> <> <> <> <> @ \eject \begin{thebibliography}{99} \bibitem{1} nothing \end{thebibliography} \end{document}