aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGabriel Dos Reis <gdr@axiomatics.org>2016-02-06 09:29:03 -0800
committerGabriel Dos Reis <gdr@axiomatics.org>2016-02-06 09:29:03 -0800
commit840651da76b018edd0fac7eac5087e8adb1701c8 (patch)
tree213eb01d7b75ebb6dc7c7da143e43b513e0dc326 /src
parentde24fd0cab54a21333221f0678f33787d74a5355 (diff)
downloadopen-axiom-840651da76b018edd0fac7eac5087e8adb1701c8.tar.gz
Rewrite capsule of IndexedDirectProductOrderedAbelianMonoidSup
Rewrite `subtractIfCan` and `sup` in terms of the mathematical operations and exported operations. This makes the correctness of the algorithms stand out.
Diffstat (limited to 'src')
-rw-r--r--src/algebra/indexedp.spad.pamphlet38
1 files changed, 18 insertions, 20 deletions
diff --git a/src/algebra/indexedp.spad.pamphlet b/src/algebra/indexedp.spad.pamphlet
index 6e131135..a9f36a64 100644
--- a/src/algebra/indexedp.spad.pamphlet
+++ b/src/algebra/indexedp.spad.pamphlet
@@ -280,32 +280,30 @@ IndexedDirectProductOrderedAbelianMonoid(A:OrderedAbelianMonoid,S:OrderedType):
IndexedDirectProductOrderedAbelianMonoidSup(A:OrderedAbelianMonoidSup,S:OrderedSet):
Join(OrderedAbelianMonoidSup,IndexedDirectProductCategory(A,S))
== IndexedDirectProductOrderedAbelianMonoid(A,S) add
- --representations
- Term == Record(k:S,c:A)
- Rep:= List Term
-
subtractIfCan(x,y) ==
- empty? y => just x
- empty? x => nothing
- x.first.k < y.first.k => nothing
- x.first.k > y.first.k =>
- t:= subtractIfCan(x.rest, y)
+ zero? y => just x
+ zero? x => nothing
+ leadingSupport x < leadingSupport y => nothing
+ leadingSupport x > leadingSupport y =>
+ t := subtractIfCan(reductum x, y)
t case nothing => nothing
- just cons( x.first, t)
- u := subtractIfCan(x.first.c, y.first.c)
+ just convert cons(leadingTerm x, terms t)
+ u := subtractIfCan(leadingCoefficient x, leadingCoefficient y)
u case nothing => nothing
- zero? u => subtractIfCan(x.rest, y.rest)
- t := subtractIfCan(x.rest, y.rest)
+ t := subtractIfCan(reductum x, reductum y)
+ zero? u => t
t case nothing => nothing
- just cons([x.first.k,u],t)
+ just convert cons(term(leadingSupport x,u),terms t)
sup(x,y) ==
- empty? y => x
- empty? x => y
- x.first.k < y.first.k => cons(y.first,sup(x,y.rest))
- x.first.k > y.first.k => cons(x.first,sup(x.rest,y))
- u:=sup(x.first.c, y.first.c)
- cons([x.first.k,u],sup(x.rest,y.rest))
+ zero? y => x
+ zero? x => y
+ leadingSupport x < leadingSupport y =>
+ convert cons(leadingTerm y,terms sup(x,reductum y))
+ leadingSupport x > leadingSupport y =>
+ convert cons(leadingTerm x,terms sup(reductum x,y))
+ u := sup(leadingCoefficient x, leadingCoefficient y)
+ convert cons(term(leadingSupport x,u),terms sup(reductum x,reductum y))
@
\section{domain IDPAG IndexedDirectProductAbelianGroup}