/usr/share/axiom-20170501/src/algebra/MONADWU.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 | )abbrev category MONADWU MonadWithUnit
++ Authors: J. Grabmeier, R. Wisbauer
++ Date Created: 01 March 1991
++ Date Last Updated: 11 June 1991
++ Reference:
++ Jaco68 Structure and Representations of Jordan Algebras
++ Description:
++ MonadWithUnit is the class of multiplicative monads with unit,
++ that is, sets with a binary operation and a unit element.
++
++ Axioms\br
++ \tab{5}leftIdentity("*":(%,%)->%,1) for example, 1*x=x\br
++ \tab{5}rightIdentity("*":(%,%)->%,1) for example, x*1=x
++
++ Common Additional Axioms\br
++ \tab{5}unitsKnown - if "recip" says "failed", it PROVES input wasn't a unit
MonadWithUnit() : Category == SIG where
SIG ==> Monad with
1 : constant -> %
++ \spad{1} returns the unit element, denoted by 1.
one? : % -> Boolean
++ one?(a) tests whether \spad{a} is the unit 1.
rightPower : (%,NonNegativeInteger) -> %
++ rightPower(a,n) returns the \spad{n}-th right power of \spad{a},
++ that is, \spad{rightPower(a,n) := rightPower(a,n-1) * a} and
++ \spad{rightPower(a,0) := 1}.
leftPower : (%,NonNegativeInteger) -> %
++ leftPower(a,n) returns the \spad{n}-th left power of \spad{a},
++ that is, \spad{leftPower(a,n) := a * leftPower(a,n-1)} and
++ \spad{leftPower(a,0) := 1}.
"**" : (%,NonNegativeInteger) -> %
++ \spad{a**n} returns the \spad{n}-th power of \spad{a},
++ defined by repeated squaring.
recip : % -> Union(%,"failed")
++ recip(a) returns an element, which is both a left and a right
++ inverse of \spad{a},
++ or \spad{"failed"} if such an element doesn't exist or cannot
++ be determined (see unitsKnown).
leftRecip : % -> Union(%,"failed")
++ leftRecip(a) returns an element, which is a left inverse of
++ \spad{a}, or \spad{"failed"} if such an element doesn't exist
++ or cannot be determined (see unitsKnown).
rightRecip : % -> Union(%,"failed")
++ rightRecip(a) returns an element, which is a right inverse of
++ \spad{a}, or \spad{"failed"} if such an element doesn't exist
++ or cannot be determined (see unitsKnown).
add
import RepeatedSquaring(%)
one? x == x = 1
x:% ** n:NonNegativeInteger ==
zero? n => 1
expt(x,n pretend PositiveInteger)
rightPower(a,n) ==
zero? n => 1
res := 1
for i in 1..n repeat res := res * a
res
leftPower(a,n) ==
zero? n => 1
res := 1
for i in 1..n repeat res := a * res
res
|