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

\documentclass{article}
\usepackage{open-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::OutputForm
             one? imagi(x) => 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::OutputForm
             one? imagj(x) => 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::OutputForm
             one? imagk(x) => 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::OutputForm
             one? imagE(x) => 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::OutputForm
             one? imagI(x) => 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::OutputForm
             one? imagJ(x) => 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::OutputForm
         one? imagK(x) => 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
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.
--Copyright (C) 2007-2009, Gabriel Dos Reis.
--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}