diff options
Diffstat (limited to 'src/algebra/retract.spad.pamphlet')
| -rw-r--r-- | src/algebra/retract.spad.pamphlet | 137 |
1 files changed, 137 insertions, 0 deletions
diff --git a/src/algebra/retract.spad.pamphlet b/src/algebra/retract.spad.pamphlet new file mode 100644 index 00000000..8738f2cf --- /dev/null +++ b/src/algebra/retract.spad.pamphlet @@ -0,0 +1,137 @@ +\documentclass{article} +\usepackage{axiom} +\begin{document} +\title{\$SPAD/src/algebra retract.spad} +\author{Manuel Bronstein} +\maketitle +\begin{abstract} +\end{abstract} +\eject +\tableofcontents +\eject +\section{category FRETRCT FullyRetractableTo} +<<category FRETRCT FullyRetractableTo>>= +)abbrev category FRETRCT FullyRetractableTo +++ Author: Manuel Bronstein +++ Description: +++ A is fully retractable to B means that A is retractable to B, and, +++ in addition, if B is retractable to the integers or rational +++ numbers then so is A. +++ In particular, what we are asserting is that there are no integers +++ (rationals) in A which don't retract into B. +++ Date Created: March 1990 +++ Date Last Updated: 9 April 1991 +FullyRetractableTo(S: Type): Category == RetractableTo(S) with + if (S has RetractableTo Integer) then RetractableTo Integer + if (S has RetractableTo Fraction Integer) then + RetractableTo Fraction Integer + add + if not(S is Integer) then + if (S has RetractableTo Integer) then -- induction + coerce(n:Integer):% == n::S::% + retract(r:%):Integer == retract(retract(r)@S) + + retractIfCan(r:%):Union(Integer, "failed") == + (u:= retractIfCan(r)@Union(S,"failed")) case "failed"=> "failed" + retractIfCan(u::S) + + if not(S is Fraction Integer) then + if (S has RetractableTo Fraction Integer) then -- induction + coerce(n:Fraction Integer):% == n::S::% + retract(r:%):Fraction(Integer) == retract(retract(r)@S) + + retractIfCan(r:%):Union(Fraction Integer, "failed") == + (u:=retractIfCan(r)@Union(S,"failed")) case "failed"=>"failed" + retractIfCan(u::S) + +@ +\section{package INTRET IntegerRetractions} +<<package INTRET IntegerRetractions>>= +)abbrev package INTRET IntegerRetractions +++ Author: Manuel Bronstein +++ Description: Provides integer testing and retraction functions. +++ Date Created: March 1990 +++ Date Last Updated: 9 April 1991 +IntegerRetractions(S:RetractableTo(Integer)): with + integer : S -> Integer + ++ integer(x) returns x as an integer; + ++ error if x is not an integer; + integer? : S -> Boolean + ++ integer?(x) is true if x is an integer, false otherwise; + integerIfCan: S -> Union(Integer, "failed") + ++ integerIfCan(x) returns x as an integer, + ++ "failed" if x is not an integer; + == add + integer s == retract s + integer? s == retractIfCan(s) case Integer + integerIfCan s == retractIfCan s + +@ +\section{package RATRET RationalRetractions} +<<package RATRET RationalRetractions>>= +)abbrev package RATRET RationalRetractions +++ Author: Manuel Bronstein +++ Description: rational number testing and retraction functions. +++ Date Created: March 1990 +++ Date Last Updated: 9 April 1991 +RationalRetractions(S:RetractableTo(Fraction Integer)): with + rational : S -> Fraction Integer + ++ rational(x) returns x as a rational number; + ++ error if x is not a rational number; + rational? : S -> Boolean + ++ rational?(x) returns true if x is a rational number, + ++ false otherwise; + rationalIfCan: S -> Union(Fraction Integer, "failed") + ++ rationalIfCan(x) returns x as a rational number, + ++ "failed" if x is not a rational number; + == add + rational s == retract s + rational? s == retractIfCan(s) case Fraction(Integer) + rationalIfCan s == retractIfCan s + +@ +\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>> + +<<category FRETRCT FullyRetractableTo>> +<<package INTRET IntegerRetractions>> +<<package RATRET RationalRetractions>> +@ +\eject +\begin{thebibliography}{99} +\bibitem{1} nothing +\end{thebibliography} +\end{document} |