diff options
| author | dos-reis <gdr@axiomatics.org> | 2007-08-14 05:14:52 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2007-08-14 05:14:52 +0000 |
| commit | ab8cc85adde879fb963c94d15675783f2cf4b183 (patch) | |
| tree | c202482327f474583b750b2c45dedfc4e4312b1d /src/algebra/card.spad.pamphlet | |
| download | open-axiom-ab8cc85adde879fb963c94d15675783f2cf4b183.tar.gz | |
Initial population.
Diffstat (limited to 'src/algebra/card.spad.pamphlet')
| -rw-r--r-- | src/algebra/card.spad.pamphlet | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/algebra/card.spad.pamphlet b/src/algebra/card.spad.pamphlet new file mode 100644 index 00000000..a1585083 --- /dev/null +++ b/src/algebra/card.spad.pamphlet @@ -0,0 +1,206 @@ +\documentclass{article} +\usepackage{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>>= +)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 + 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?() == GCHypothesis() + generalizedContinuumHypothesisAssumed b == (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} |