/usr/lib/open-axiom/src/algebra/cra.spad is in open-axiom-source 1.4.1+svn~2626-2ubuntu2.
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 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 | --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.
)abbrev package CRAPACK CRApackage
++ This package \undocumented{}
CRApackage(R:EuclideanDomain): Exports == Implementation where
Exports == with
modTree: (R,List R) -> List R
++ modTree(r,l) \undocumented{}
chineseRemainder: (List R, List R) -> R
++ chineseRemainder(lv,lm) returns a value \axiom{v} such that, if
++ x is \axiom{lv.i} modulo \axiom{lm.i} for all \axiom{i}, then
++ x is \axiom{v} modulo \axiom{lm(1)*lm(2)*...*lm(n)}.
chineseRemainder: (List List R, List R) -> List R
++ chineseRemainder(llv,lm) returns a list of values, each of which
++ corresponds to the Chinese remainder of the associated element of
++ \axiom{llv} and axiom{lm}. This is more efficient than applying
++ chineseRemainder several times.
multiEuclideanTree: (List R, R) -> List R
++ multiEuclideanTree(l,r) \undocumented{}
Implementation == add
BB:=BalancedBinaryTree(R)
x:BB
-- Definition for modular reduction mapping with several moduli
modTree(a,lm) ==
t := balancedBinaryTree(#lm, 0$R)
setleaves!(t,lm)
mapUp!(t,"*")
leaves mapDown!(t, a, "rem")
chineseRemainder(lv:List(R), lm:List(R)):R ==
#lm ~= #lv => error "lists of moduli and values not of same length"
x := balancedBinaryTree(#lm, 0$R)
x := setleaves!(x, lm)
mapUp!(x,"*")
y := balancedBinaryTree(#lm, 1$R)
y := mapUp!(copy y,x,#1 * #4 + #2 * #3)
(u := extendedEuclidean(value y, value x,1)) case "failed" =>
error "moduli not relatively prime"
inv := u . coef1
linv := modTree(inv, lm)
l := [(u*v) rem m for v in lv for u in linv for m in lm]
y := setleaves!(y,l)
value(mapUp!(y, x, #1 * #4 + #2 * #3)) rem value(x)
chineseRemainder(llv:List List(R), lm:List(R)):List(R) ==
x := balancedBinaryTree(#lm, 0$R)
x := setleaves!(x, lm)
mapUp!(x,"*")
y := balancedBinaryTree(#lm, 1$R)
y := mapUp!(copy y,x,#1 * #4 + #2 * #3)
(u := extendedEuclidean(value y, value x,1)) case "failed" =>
error "moduli not relatively prime"
inv := u . coef1
linv := modTree(inv, lm)
retVal:List(R) := []
for lv in llv repeat
l := [(u3*v) rem m for v in lv for u3 in linv for m in lm]
y := setleaves!(y,l)
retVal := cons(value(mapUp!(y, x, #1*#4+#2*#3)) rem value(x),retVal)
reverse retVal
extEuclidean: (R, R, R) -> List R
extEuclidean(a, b, c) ==
u := extendedEuclidean(a, b, c)
u case "failed" => error [c, " not spanned by ", a, " and ",b]
[u.coef2, u.coef1]
multiEuclideanTree(fl, rhs) ==
x := balancedBinaryTree(#fl, rhs)
x := setleaves!(x, fl)
mapUp!(x,"*")
leaves mapDown!(x, rhs, extEuclidean)
|