open-axiom repository from github
\documentclass{article}
\usepackage{open-axiom}
\begin{document}
\title{\$SPAD/src/algebra card.spad}
\author{Stephen M. Watt}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
\section{domain CARD CardinalNumber}
<<domain CARD CardinalNumber>>=
import Boolean
import NonNegativeInteger
)abbrev domain CARD CardinalNumber
++ Author: S.M. Watt
++ Date Created: June 1986
++ Date Last Updated: May 1990
++ Basic Operations: Aleph, +, -, *, **
++ Related Domains:
++ Also See:
++ AMS Classifications:
++ Keywords: cardinal number, transfinite arithmetic
++ Examples:
++ References:
++ Goedel, "The consistency of the continuum hypothesis",
++ Ann. Math. Studies, Princeton Univ. Press, 1940
++ Description:
++ Members of the domain CardinalNumber are values indicating the
++ cardinality of sets, both finite and infinite. Arithmetic operations
++ are defined on cardinal numbers as follows.
++
++ If \spad{x = #X} and \spad{y = #Y} then
++ \spad{x+y = #(X+Y)} \tab{30}disjoint union
++ \spad{x-y = #(X-Y)} \tab{30}relative complement
++ \spad{x*y = #(X*Y)} \tab{30}cartesian product
++ \spad{x**y = #(X**Y)} \tab{30}\spad{X**Y = \{g| g:Y->X\}}
++
++ The non-negative integers have a natural construction as cardinals
++ \spad{0 = #\{\}}, \spad{1 = \{0\}}, \spad{2 = \{0, 1\}}, ..., \spad{n = \{i| 0 <= i < n\}}.
++
++ That \spad{0} acts as a zero for the multiplication of cardinals is
++ equivalent to the axiom of choice.
++
++ The generalized continuum hypothesis asserts
++ \center{\spad{2**Aleph i = Aleph(i+1)}}
++ and is independent of the axioms of set theory [Goedel 1940].
++
++ Three commonly encountered cardinal numbers are
++ \spad{a = #Z} \tab{30}countable infinity
++ \spad{c = #R} \tab{30}the continuum
++ \spad{f = #\{g| g:[0,1]->R\}}
++
++ In this domain, these values are obtained using
++ \spad{a := Aleph 0}, \spad{c := 2**a}, \spad{f := 2**c}.
++
CardinalNumber: Join(OrderedSet, AbelianMonoid, Monoid,
RetractableTo NonNegativeInteger) with
commutative "*"
++ a domain D has \spad{commutative("*")} if it has an operation
++ \spad{"*": (D,D) -> D} which is commutative.
-: (%,%) -> Union(%,"failed")
++ \spad{x - y} returns an element z such that \spad{z+y=x} or "failed"
++ if no such element exists.
**: (%, %) -> %
++ \spad{x**y} returns \spad{#(X**Y)} where \spad{X**Y} is defined
++ as \spad{\{g| g:Y->X\}}.
Aleph: NonNegativeInteger -> %
++ Aleph(n) provides the named (infinite) cardinal number.
finite?: % -> Boolean
++ finite?(\spad{a}) determines whether
++ \spad{a} is a finite cardinal,
++ i.e. an integer.
countable?: % -> Boolean
++ countable?(\spad{a}) determines
++ whether \spad{a} is a countable cardinal,
++ i.e. an integer or \spad{Aleph 0}.
generalizedContinuumHypothesisAssumed?: () -> Boolean
++ generalizedContinuumHypothesisAssumed?()
++ tests if the hypothesis is currently assumed.
generalizedContinuumHypothesisAssumed: Boolean -> Boolean
++ generalizedContinuumHypothesisAssumed(bool)
++ is used to dictate whether the hypothesis is to be assumed.
== add
NNI ==> NonNegativeInteger
FINord ==> -1
DUMMYval ==> -1
Rep := Record(order: Integer, ival: Integer)
GCHypothesis: Reference(Boolean) := ref false
-- Creation
0 == [FINord, 0]
1 == [FINord, 1]
coerce(n:NonNegativeInteger):% == [FINord, n]
Aleph n == [n, DUMMYval]
-- Output
ALEPHexpr := "Aleph"::OutputForm
coerce(x: %): OutputForm ==
x.order = FINord => (x.ival)::OutputForm
prefix(ALEPHexpr, [(x.order)::OutputForm])
-- Manipulation
x = y ==
x.order ~= y.order => false
finite? x => x.ival = y.ival
true -- equal transfinites
x < y ==
x.order < y.order => true
x.order > y.order => false
finite? x => x.ival < y.ival
false -- equal transfinites
x:% + y:% ==
finite? x and finite? y => [FINord, x.ival+y.ival]
max(x, y)
x - y ==
x < y => "failed"
finite? x => [FINord, x.ival-y.ival]
x > y => x
"failed" -- equal transfinites
x:% * y:% ==
finite? x and finite? y => [FINord, x.ival*y.ival]
x = 0 or y = 0 => 0
max(x, y)
n:NonNegativeInteger * x:% ==
finite? x => [FINord, n*x.ival]
n = 0 => 0
x
(x: %) ** (y: %) ==
y = 0 =>
x ~= 0 => 1
error "0**0 not defined for cardinal numbers."
finite? y =>
not finite? x => x
[FINord,x.ival**(y.ival):NNI]
x = 0 => 0
x = 1 => 1
deref GCHypothesis => [max(x.order-1, y.order) + 1, DUMMYval]
error "Transfinite exponentiation only implemented under GCH"
finite? x == x.order = FINord
countable? x == x.order < 1
retract(x:%):NonNegativeInteger ==
finite? x => (x.ival)::NNI
error "Not finite"
retractIfCan(x:%):Union(NonNegativeInteger, "failed") ==
finite? x => (x.ival)::NNI
"failed"
-- State manipulation
generalizedContinuumHypothesisAssumed?() == deref GCHypothesis
generalizedContinuumHypothesisAssumed b == setref(GCHypothesis,b)
@
\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 CARD CardinalNumber>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}