path: root/src/algebra/complet.spad.pamphlet

\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 =>
          n > 0 => 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) ==
        r > 0 => [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}