/usr/share/axiom-20170501/src/algebra/ORDFUNS.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 | )abbrev package ORDFUNS OrderingFunctions
++ Author: Barry Trager
++ Description:
++ This package provides ordering functions on vectors which
++ are suitable parameters for OrderedDirectProduct.
OrderingFunctions(dim,S) : SIG == CODE where
dim : NonNegativeInteger
S : OrderedAbelianMonoid
VS ==> Vector S
SIG ==> with
pureLex : (VS,VS) -> Boolean
++ pureLex(v1,v2) return true if the vector v1 is less than the
++ vector v2 in the lexicographic ordering.
totalLex : (VS,VS) -> Boolean
++ totalLex(v1,v2) return true if the vector v1 is less than the
++ vector v2 in the ordering which is total degree refined by
++ lexicographic ordering.
reverseLex : (VS,VS) -> Boolean
++ reverseLex(v1,v2) return true if the vector v1 is less than the
++ vector v2 in the ordering which is total degree refined by
++ the reverse lexicographic ordering.
CODE ==> add
n:NonNegativeInteger:=dim
-- pure lexicographical ordering
pureLex(v1:VS,v2:VS) : Boolean ==
for i in 1..n repeat
if qelt(v1,i) < qelt(v2,i) then return true
if qelt(v2,i) < qelt(v1,i) then return false
false
-- total ordering refined with lex
totalLex(v1:VS,v2:VS) :Boolean ==
n1:S:=0
n2:S:=0
for i in 1..n repeat
n1:= n1+qelt(v1,i)
n2:=n2+qelt(v2,i)
n1<n2 => true
n2<n1 => false
for i in 1..n repeat
if qelt(v1,i) < qelt(v2,i) then return true
if qelt(v2,i) < qelt(v1,i) then return false
false
-- reverse lexicographical ordering
reverseLex(v1:VS,v2:VS) :Boolean ==
n1:S:=0
n2:S:=0
for i in 1..n repeat
n1:= n1+qelt(v1,i)
n2:=n2+qelt(v2,i)
n1<n2 => true
n2<n1 => false
for i in reverse(1..n) repeat
if qelt(v2,i) < qelt(v1,i) then return true
if qelt(v1,i) < qelt(v2,i) then return false
false
|