Initial population.

1 files changed, 414 insertions, 0 deletions

diff --git a/src/algebra/oct.spad.pamphlet b/src/algebra/oct.spad.pamphlet
new file mode 100644
index 00000000..680cb040
--- /dev/null
+++ b/src/algebra/oct.spad.pamphlet
@@ -0,0 +1,414 @@
+\documentclass{article}
+\usepackage{axiom}
+\begin{document}
+\title{\$SPAD/src/algebra oct.spad}
+\author{Robert Wisbauer, Johannes Grabmeier}
+\maketitle
+\begin{abstract}
+\end{abstract}
+\eject
+\tableofcontents
+\eject
+\section{category OC OctonionCategory}
+<<category OC OctonionCategory>>=
+)abbrev category OC OctonionCategory
+++ Author: R. Wisbauer, J. Grabmeier
+++ Date Created: 05 September 1990
+++ Date Last Updated: 19 September 1990
+++ Basic Operations: _+, _*, octon, real, imagi, imagj, imagk,
+++  imagE, imagI, imagJ, imagK
+++ Related Constructors: QuaternionCategory
+++ Also See: 
+++ AMS Classifications:
+++ Keywords: octonion, non-associative algebra, Cayley-Dixon  
+++ References: e.g. I.L Kantor, A.S. Solodovnikov:
+++  Hypercomplex Numbers, Springer Verlag Heidelberg, 1989,
+++  ISBN 0-387-96980-2
+++ Description:
+++  OctonionCategory gives the categorial frame for the 
+++  octonions, and eight-dimensional non-associative algebra, 
+++  doubling the the quaternions in the same way as doubling
+++  the Complex numbers to get the quaternions.
+-- Examples: octonion.input
+ 
+OctonionCategory(R: CommutativeRing): Category ==
+  -- we are cheating a little bit, algebras in \Language{}
+  -- are mainly considered to be associative, but that's not 
+  -- an attribute and we can't guarantee that there is no piece
+  -- of code which implicitly
+  -- uses this. In a later version we shall properly combine
+  -- all this code in the context of general, non-associative
+  -- algebras, which are meanwhile implemented in \Language{}
+  Join(Algebra R, FullyRetractableTo R, FullyEvalableOver R) with
+     conjugate: % -> % 
+       ++ conjugate(o) negates the imaginary parts i,j,k,E,I,J,K of octonian o.
+     real:    % -> R 
+       ++ real(o) extracts real part of octonion o.
+     imagi:   % -> R      
+       ++ imagi(o) extracts the i part of octonion o.
+     imagj:   % -> R                
+       ++ imagj(o) extracts the j part of octonion o.
+     imagk:   % -> R 
+       ++ imagk(o) extracts the k part of octonion o.
+     imagE:   % -> R 
+       ++ imagE(o) extracts the imaginary E part of octonion o.
+     imagI:   % -> R              
+       ++ imagI(o) extracts the imaginary I part of octonion o.
+     imagJ:   % -> R      
+       ++ imagJ(o) extracts the imaginary J part of octonion o.
+     imagK:   % -> R
+       ++ imagK(o) extracts the imaginary K part of octonion o.
+     norm:    % -> R 
+       ++ norm(o) returns the norm of an octonion, equal to
+       ++ the sum of the squares
+       ++ of its coefficients.
+     octon: (R,R,R,R,R,R,R,R) -> %   
+       ++ octon(re,ri,rj,rk,rE,rI,rJ,rK) constructs an octonion 
+       ++ from scalars. 
+     if R has Finite then Finite
+     if R has OrderedSet then OrderedSet
+     if R has ConvertibleTo InputForm then ConvertibleTo InputForm
+     if R has CharacteristicZero then CharacteristicZero
+     if R has CharacteristicNonZero then CharacteristicNonZero
+     if R has RealNumberSystem then
+       abs:   % -> R 
+         ++ abs(o) computes the absolute value of an octonion, equal to 
+         ++ the square root of the \spadfunFrom{norm}{Octonion}.
+     if R has IntegerNumberSystem then
+       rational?    : % -> Boolean
+         ++ rational?(o) tests if o is rational, i.e. that all seven
+         ++ imaginary parts are 0.
+       rational     : % -> Fraction Integer
+         ++ rational(o) returns the real part if all seven 
+         ++ imaginary parts are 0.
+         ++ Error: if o is not rational.
+       rationalIfCan: % -> Union(Fraction Integer, "failed")
+         ++ rationalIfCan(o) returns the real part if
+         ++ all seven imaginary parts are 0, and "failed" otherwise.
+     if R has Field then
+       inv : % -> % 
+         ++ inv(o) returns the inverse of o if it exists.
+ add
+     characteristic() == 
+       characteristic()$R
+     conjugate x ==
+       octon(real x, - imagi x, - imagj x, - imagk x, - imagE x,_
+       - imagI x, - imagJ x, - imagK x)
+     map(fn, x)       ==
+       octon(fn real x,fn imagi x,fn imagj x,fn imagk x, fn imagE x,_
+       fn imagI x, fn imagJ x,fn imagK x)
+     norm x ==
+       real x * real x + imagi x * imagi x + _
+       imagj x * imagj x + imagk x * imagk x + _
+       imagE x * imagE x + imagI x * imagI x + _
+       imagJ x * imagJ x + imagK x * imagK x
+     x = y            ==
+       (real x = real y) and (imagi x = imagi y) and _
+       (imagj x = imagj y) and (imagk x = imagk y) and _
+       (imagE x = imagE y) and (imagI x = imagI y) and _
+       (imagJ x = imagJ y) and (imagK x = imagK y)
+     x + y            ==
+       octon(real x + real y, imagi x + imagi y,_
+       imagj x + imagj y, imagk x + imagk y,_
+       imagE x + imagE y, imagI x + imagI y,_
+       imagJ x + imagJ y, imagK x + imagK y)
+     - x              ==
+       octon(- real x, - imagi x, - imagj x, - imagk x,_
+       - imagE x, - imagI x, - imagJ x, - imagK x)
+     r:R * x:%        ==
+       octon(r * real x, r * imagi x, r * imagj x, r * imagk x,_
+       r * imagE x, r * imagI x, r * imagJ x, r * imagK x)
+     n:Integer * x:%  ==
+       octon(n * real x, n * imagi x, n * imagj x, n * imagk x,_
+       n * imagE x, n * imagI x, n * imagJ x, n * imagK x)
+     coerce(r:R)      ==
+       octon(r,0$R,0$R,0$R,0$R,0$R,0$R,0$R)
+     coerce(n:Integer)      ==
+       octon(n :: R,0$R,0$R,0$R,0$R,0$R,0$R,0$R)
+     zero? x ==
+       zero? real x and zero? imagi x and _
+       zero? imagj x and zero? imagk x and _
+       zero? imagE x and zero? imagI x and _
+       zero? imagJ x and zero? imagK x
+     retract(x):R ==
+       not (zero? imagi x and zero? imagj x and zero? imagk x and _
+       zero? imagE x and zero? imagI x and zero? imagJ x and zero? imagK x)=>
+         error "Cannot retract octonion."
+       real x
+     retractIfCan(x):Union(R,"failed") ==
+       not (zero? imagi x and zero? imagj x and zero? imagk x and _
+       zero? imagE x and zero? imagI x and zero? imagJ x and zero? imagK x)=>
+         "failed"
+       real x
+ 
+     coerce(x:%):OutputForm ==
+         part,z : OutputForm
+         y : %
+         zero? x => (0$R) :: OutputForm
+         not zero?(real x) =>
+           y := octon(0$R,imagi(x),imagj(x),imagk(x),imagE(x),
+             imagI(x),imagJ(x),imagK(x))
+           zero? y => real(x) :: OutputForm
+           (real(x) :: OutputForm) + (y :: OutputForm)
+         -- we know that the real part is 0
+         not zero?(imagi(x)) =>
+           y := octon(0$R,0$R,imagj(x),imagk(x),imagE(x),
+             imagI(x),imagJ(x),imagK(x))
+           z :=
+             part := "i"::Symbol::OutputForm
+--             one? imagi(x) => part
+             (imagi(x) = 1) => part
+             (imagi(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part and i part are 0
+         not zero?(imagj(x)) =>
+           y := octon(0$R,0$R,0$R,imagk(x),imagE(x),
+             imagI(x),imagJ(x),imagK(x))
+           z :=
+             part := "j"::Symbol::OutputForm
+--             one? imagj(x) => part
+             (imagj(x) = 1) => part
+             (imagj(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part and i and j parts are 0
+         not zero?(imagk(x)) =>
+           y := octon(0$R,0$R,0$R,0$R,imagE(x),
+             imagI(x),imagJ(x),imagK(x))
+           z :=
+             part := "k"::Symbol::OutputForm
+--             one? imagk(x) => part
+             (imagk(x) = 1) => part
+             (imagk(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part,i,j,k parts are 0
+         not zero?(imagE(x)) =>
+           y := octon(0$R,0$R,0$R,0$R,0$R,
+             imagI(x),imagJ(x),imagK(x))
+           z :=
+             part := "E"::Symbol::OutputForm
+--             one? imagE(x) => part
+             (imagE(x) = 1) => part
+             (imagE(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part,i,j,k,E parts are 0
+         not zero?(imagI(x)) =>
+           y := octon(0$R,0$R,0$R,0$R,0$R,0$R,imagJ(x),imagK(x))
+           z :=
+             part := "I"::Symbol::OutputForm
+--             one? imagI(x) => part
+             (imagI(x) = 1) => part
+             (imagI(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part,i,j,k,E,I parts are 0
+         not zero?(imagJ(x)) =>
+           y := octon(0$R,0$R,0$R,0$R,0$R,0$R,0$R,imagK(x))
+           z :=
+             part := "J"::Symbol::OutputForm
+--             one? imagJ(x) => part
+             (imagJ(x) = 1) => part
+             (imagJ(x) :: OutputForm) * part
+           zero? y => z
+           z + (y :: OutputForm)
+         -- we know that the real part,i,j,k,E,I,J parts are 0
+         part := "K"::Symbol::OutputForm
+--         one? imagK(x) => part
+         (imagK(x) = 1) => part
+         (imagK(x) :: OutputForm) * part
+ 
+     if R has Field then
+       inv x ==
+         (norm x) = 0 => error "This octonion is not invertible."
+         (inv norm x) * conjugate x
+     if R has ConvertibleTo InputForm then
+       convert(x:%):InputForm ==
+         l : List InputForm := [convert("octon" :: Symbol),
+           convert(real x)$R, convert(imagi x)$R, convert(imagj x)$R,_
+             convert(imagk x)$R, convert(imagE x)$R,_
+             convert(imagI x)$R, convert(imagJ x)$R,_
+             convert(imagK x)$R]
+         convert(l)$InputForm
+     if R has OrderedSet then
+       x < y ==
+         real x = real y =>
+          imagi x = imagi y =>
+           imagj x = imagj y =>
+            imagk x = imagk y =>
+             imagE x = imagE y =>
+              imagI x = imagI y =>
+               imagJ x = imagJ y =>
+                imagK x < imagK y
+               imagJ x < imagJ y
+              imagI x < imagI y
+             imagE x < imagE y
+            imagk x < imagk y 
+           imagj x < imagj y 
+          imagi x < imagi y 
+         real x < real y
+ 
+     if R has RealNumberSystem then
+       abs x == sqrt norm x
+ 
+     if R has IntegerNumberSystem then
+       rational? x ==
+         (zero? imagi x) and (zero? imagj x) and (zero? imagk x) and _ 
+         (zero? imagE x) and (zero? imagI x) and (zero? imagJ x) and _
+         (zero? imagK x)
+       rational  x ==
+         rational? x => rational real x
+         error "Not a rational number"
+       rationalIfCan x ==
+         rational? x => rational real x
+         "failed"
+
+@
+\section{domain OCT Octonion}
+<<domain OCT Octonion>>=
+)abbrev domain OCT Octonion
+++ Author: R. Wisbauer, J. Grabmeier
+++ Date Created: 05 September 1990
+++ Date Last Updated: 20 September 1990
+++ Basic Operations: _+,_*,octon,image,imagi,imagj,imagk,
+++  imagE,imagI,imagJ,imagK
+++ Related Constructors: Quaternion
+++ Also See: AlgebraGivenByStructuralConstants
+++ AMS Classifications:
+++ Keywords: octonion, non-associative algebra, Cayley-Dixon  
+++ References: e.g. I.L Kantor, A.S. Solodovnikov:
+++  Hypercomplex Numbers, Springer Verlag Heidelberg, 1989,
+++  ISBN 0-387-96980-2
+++ Description:
+++  Octonion implements octonions (Cayley-Dixon algebra) over a
+++  commutative ring, an eight-dimensional non-associative
+++  algebra, doubling the quaternions in the same way as doubling
+++  the complex numbers to get the quaternions 
+++  the main constructor function is {\em octon} which takes 8
+++  arguments: the real part, the i imaginary part, the j 
+++  imaginary part, the k imaginary part, (as with quaternions)
+++  and in addition the imaginary parts E, I, J, K.
+-- Examples: octonion.input
+--)boot $noSubsumption := true
+Octonion(R:CommutativeRing): export == impl where
+ 
+  QR ==> Quaternion R
+ 
+  export ==> Join(OctonionCategory R, FullyRetractableTo QR)  with
+    octon: (QR,QR) -> %
+      ++ octon(qe,qE) constructs an octonion from two quaternions
+      ++ using the relation {\em O = Q + QE}.
+  impl ==> add
+    Rep := Record(e: QR,E: QR)
+ 
+    0 == [0,0]
+    1 == [1,0]
+ 
+    a,b,c,d,f,g,h,i : R
+    p,q : QR
+    x,y : %
+ 
+    real  x == real (x.e)
+    imagi x == imagI (x.e)
+    imagj x == imagJ (x.e)
+    imagk x == imagK (x.e)
+    imagE x == real (x.E)
+    imagI x == imagI (x.E)
+    imagJ x == imagJ (x.E)
+    imagK x == imagK (x.E)
+    octon(a,b,c,d,f,g,h,i) == [quatern(a,b,c,d)$QR,quatern(f,g,h,i)$QR]
+    octon(p,q) == [p,q]
+    coerce(q) == [q,0$QR] 
+    retract(x):QR ==
+      not(zero? imagE x and zero? imagI x and zero? imagJ x and zero? imagK x)=>
+        error "Cannot retract octonion to quaternion."
+      quatern(real x, imagi x,imagj x, imagk x)$QR
+    retractIfCan(x):Union(QR,"failed") ==
+      not(zero? imagE x and zero? imagI x and zero? imagJ x and zero? imagK x)=>
+        "failed"
+      quatern(real x, imagi x,imagj x, imagk x)$QR
+    x * y == [x.e*y.e-(conjugate y.E)*x.E, y.E*x.e + x.E*(conjugate y.e)]
+
+@
+\section{package OCTCT2 OctonionCategoryFunctions2}
+<<package OCTCT2 OctonionCategoryFunctions2>>=
+)abbrev package OCTCT2 OctonionCategoryFunctions2
+--% OctonionCategoryFunctions2
+++ Author: Johannes Grabmeier
+++ Date Created: 10 September 1990
+++ Date Last Updated: 10 September 1990
+++ Basic Operations: map
+++ Related Constructors: 
+++ Also See: 
+++ AMS Classifications:
+++ Keywords: octonion, non-associative algebra, Cayley-Dixon  
+++ References:
+++ Description:
+++  OctonionCategoryFunctions2 implements functions between
+++  two octonion domains defined over different rings. 
+++  The function map is used 
+++  to coerce between octonion types.
+ 
+OctonionCategoryFunctions2(OR,R,OS,S) : Exports ==
+  Implementation where
+    R  : CommutativeRing
+    S  : CommutativeRing
+    OR : OctonionCategory R
+    OS : OctonionCategory S
+    Exports == with
+      map:     (R -> S, OR) -> OS
+        ++ map(f,u) maps f onto the component parts of the octonion
+        ++ u.
+    Implementation == add
+      map(fn : R -> S, u : OR): OS ==
+        octon(fn real u, fn imagi u, fn imagj u, fn imagk u,_
+        fn imagE u, fn imagI u, fn imagJ u, fn imagK u)$OS
+
+@
+\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 OC OctonionCategory>>
+<<domain OCT Octonion>>
+<<package OCTCT2 OctonionCategoryFunctions2>>
+@
+\eject
+\begin{thebibliography}{99}
+\bibitem{1} nothing
+\end{thebibliography}
+\end{document}