Initial population.

1 files changed, 377 insertions, 0 deletions

diff --git a/src/algebra/complet.spad.pamphlet b/src/algebra/complet.spad.pamphlet
new file mode 100644
index 00000000..2dc03ae7
--- /dev/null
+++ b/src/algebra/complet.spad.pamphlet
@@ -0,0 +1,377 @@
+\documentclass{article}
+\usepackage{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 =>
+          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)
+
+@
+\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
+      (n = 1) => 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)
+
+@
+\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}