--* From BMT%WATSON.vnet.ibm.com@yktvmh.watson.ibm.com Thu Jun 24 20:29:21 1993 --* Received: from yktvmh.watson.ibm.com by radical.watson.ibm.com (AIX 3.2/UCB 5.64/900524) --* id AA18813; Thu, 24 Jun 1993 20:29:21 -0400 --* Received: from watson.vnet.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3) --* with BSMTP id 9769; Thu, 24 Jun 93 20:30:09 EDT --* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0" --* id --* for asbugs@watson; Thu, 24 Jun 93 20:30:08 -0400 --* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0" --* id 2003; Thu, 24 Jun 1993 20:30:06 EDT --* Received: from cyst.watson.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3) --* with TCP; Thu, 24 Jun 93 20:30:04 EDT --* Received: from spadserv.watson.ibm.com by cyst.watson.ibm.com (AIX 3.2/UCB 5.64/900528) --* id AA20996; Thu, 24 Jun 1993 20:30:20 -0400 --* Received: by spadserv.watson.ibm.com (AIX 3.2/UCB 5.64/900524) --* id AA12579; Thu, 24 Jun 1993 20:32:49 -0400 --* Date: Thu, 24 Jun 1993 20:32:49 -0400 --* From: bmt@spadserv.watson.ibm.com --* X-External-Networks: yes --* Message-Id: <9306250032.AA12579@spadserv.watson.ibm.com> --* To: asbugs@watson.ibm.com --* Subject: Bad case 6 (line 1533 in absyn.c) [catdef.as][28.I (current)] --@ Fixed by: SSD Wed Jul 28 18:16:40 1993 --@ Tested by: none --@ Summary: No longer gets bugBadCase; now gets many type errors #include "aslib.as" --Copyright The Numerical Algorithms Group Limited 1991. Boolean ==> Bits --% attributes unitsKnown: Category == with --% Basic AXIOM Categories --% SetCategory +++ Author: +++ Date Created: +++ Date Last Updated: +++ 09/09/92 RSS added latex and hash +++ Basic Functions: +++ Related Constructors: Object +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ \spadtype{SetCategory} is the basic category for describing a collection +++ of elements with \spadop{=} (equality) and \spadfun{coerce} to output form. +++ +++ Conditional Attributes: +++ canonical\tab{15}data structure equality is the same as \spadop{=} SetCategory(): Category == Join(Object, CoercibleTo OutputForm) with --operations =: (%,%) -> Boolean ++ x=y tests if x and y are equal. hash: % -> SmallInteger ++ hash(s) calculates a hash code for s. latex: % -> String ++ latex(s) returns a LaTeX-printable output ++ representation of s. add hash(s : %): SmallInteger == 0$SmallInteger latex(s : %): String == "\mbox{\bf Unimplemented}" --% StepThrough +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A class of objects which can be 'stepped through'. +++ Repeated applications of \spadfun{nextItem} is guaranteed never to +++ return duplicate items and only return "failed" after exhausting +++ all elements of the domain. +++ This assumes that the sequence starts with \spad{init()}. +++ For infinite domains, repeated application +++ of \spadfun{nextItem} is not required to reach all possible domain elements +++ starting from any initial element. +++ +++ Conditional attributes: +++ infinite\tab{15}repeated \spad{nextItem}'s are never "failed". StepThrough(): Category == SetCategory with --operations init: constant -> % ++ init() chooses an initial object for stepping. nextItem: % -> Union(%,"failed") ++ nextItem(x) returns the next item, or "failed" if domain is exhausted. --% SemiGroup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ the class of all multiplicative semigroups, i.e. a set +++ with an associative operation \spadop{*}. +++ +++ Axioms: +++ \spad{associative(*:(%,%)->%)}\tab{30}\spad{ (x*y)*z = x*(y*z)} +++ +++ Conditional attributes: +++ \spad{commutative(*:(%,%)->%)}\tab{30}\spad{ x*y = y*x } SemiGroup(): Category == SetCategory with --operations *: (%,%) -> % ++ x*y returns the product of x and y. ^: (%,PositiveInteger) -> % ++ x^n returns the repeated product ++ of x n times, i.e. exponentiation. add import RepeatedSquaring(%) (x:% ^ n:PositiveInteger):% == expt(x,n) --% Monoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The class of multiplicative monoids, i.e. semigroups with a +++ multiplicative identity element. +++ +++ Axioms: +++ \spad{leftIdentity(*:(%,%)->%,1)}\tab{30}\spad{1*x=x} +++ \spad{rightIdentity(*:(%,%)->%,1)}\tab{30}\spad{x*1=x} +++ +++ Conditional attributes: +++ unitsKnown\tab{15}\spadfun{recip} only returns "failed" on non-units Monoid(): Category == SemiGroup with --operations 1: constant -> % ++ 1 is the multiplicative identity. one?: % -> Boolean ++ one?(x) tests if x is equal to 1. ^: (%,NonNegativeInteger) -> % ++ x^n returns the repeated product of x ++ n times, i.e. exponentiation. recip: % -> Union(%,"failed") ++ recip(x) tries to compute the multiplicative inverse for x ++ or "failed" if it cannot find the inverse (see unitsKnown). add import RepeatedSquaring(%) one?(x:%): Boolean == x = 1 recip(x:%):Union(%,"failed") == one? x => x "failed" (x:% ^ n:NonNegativeInteger):% == zero? n => 1 expt(x,n pretend PositiveInteger) --% Group +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The class of multiplicative groups, i.e. monoids with +++ multiplicative inverses. +++ +++ Axioms: +++ \spad{leftInverse(*:(%,%)->%,inv)}\tab{30}\spad{ inv(x)*x = 1 } +++ \spad{rightInverse(*:(%,%)->%,inv)}\tab{30}\spad{ x*inv(x) = 1 } Group(): Category == Monoid with --operations inv: % -> % ++ inv(x) returns the inverse of x. /: (%,%) -> % ++ x/y is the same as x times the inverse of y. ^: (%,Integer) -> % ++ x^n returns x raised to the integer power n. unitsKnown ++ unitsKnown asserts that recip only returns ++ "failed" for non-units. conjugate: (%,%) -> % ++ conjugate(p,q) computes \spad{inv(q) * p * q}; this is 'right action ++ by conjugation'. commutator: (%,%) -> % ++ commutator(p,q) computes \spad{inv(p) * inv(q) * p * q}. add import RepeatedSquaring(%) (x:% / y:%):% == x*inv(y) recip(x:%):Union(%,"failed") == inv(x) (x:% ^ n:Integer):% == zero? n => 1 n<0 => expt(inv(x),(-n) pretend PositiveInteger) expt(x,n pretend PositiveInteger) conjugate(p:%,q:%):% == inv(q) * p * q commutator(p:%,q:%):% == inv(p) * inv(q) * p * q --% AbelianSemiGroup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ the class of all additive (commutative) semigroups, i.e. +++ a set with a commutative and associative operation \spadop{+}. +++ +++ Axioms: +++ \spad{associative(+:(%,%)->%)}\tab{30}\spad{ (x+y)+z = x+(y+z) } +++ \spad{commutative(+:(%,%)->%)}\tab{30}\spad{ x+y = y+x } AbelianSemiGroup(): Category == SetCategory with --operations +: (%,%) -> % ++ x+y computes the sum of x and y. *: (PositiveInteger,%) -> % ++ n*x computes the left-multiplication of x by the positive integer n. ++ This is equivalent to adding x to itself n times. add import RepeatedDoubling(%) if not (% has Ring) then (n:PositiveInteger * x:%):% == double(n,x) --% AbelianMonoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The class of multiplicative monoids, i.e. semigroups with an +++ additive identity element. +++ +++ Axioms: +++ \spad{leftIdentity(+:(%,%)->%,0)}\tab{30}\spad{ 0+x=x } +++ \spad{rightIdentity(+:(%,%)->%,0)}\tab{30}\spad{ x+0=x } -- following domain must be compiled with subsumption disabled -- define SourceLevelSubset to be EQUAL AbelianMonoid(): Category == AbelianSemiGroup with --operations 0: constant -> % ++ 0 is the additive identity element. zero?: % -> Boolean ++ zero?(x) tests if x is equal to 0. *: (NonNegativeInteger,%) -> % ++ n * x is left-multiplication by a non negative integer add import RepeatedDoubling(%) zero?(x:%):Boolean == x = 0 (n:PositiveInteger * x:%):% == (n::NonNegativeInteger) * x if not (% has Ring) then (n:NonNegativeInteger * x:%):% == zero? n => 0 double(n pretend PositiveInteger,x) --% CancellationAbelianMonoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: Davenport & Trager I +++ Description: +++ This is an \spadtype{AbelianMonoid} with the cancellation property, i.e. +++ \spad{ a+b = a+c => b=c }. +++ This is formalised by the partial subtraction operator, +++ which satisfies the axioms listed below: +++ +++ Axioms: +++ \spad{c = a+b <=> c-b = a} CancellationAbelianMonoid(): Category == AbelianMonoid with --operations subtractIfCan: (%,%) -> Union(%,"failed") ++ subtractIfCan(x, y) returns an element z such that \spad{z+y=x} ++ or "failed" if no such element exists. --% AbelianGroup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The class of abelian groups, i.e. additive monoids where +++ each element has an additive inverse. +++ +++ Axioms: +++ \spad{-(-x) = x} +++ \spad{x+(-x) = 0} -- following domain must be compiled with subsumption disabled AbelianGroup(): Category == CancellationAbelianMonoid with --operations -: % -> % ++ -x is the additive inverse of x. -: (%,%) -> % ++ x-y is the difference of x and y ++ i.e. \spad{x + (-y)}. -- subsumes the partial subtraction from previous *: (Integer,%) -> % ++ n*x is the product of x by the integer n. add (x:% - y:%):% == x+(-y) subtractIfCan(x:%, y:%):Union(%, "failed") == (x-y) :: Union(%,"failed") (n:NonNegativeInteger * x:%):% == (n::Integer) * x import RepeatedDoubling(%) if not (% has Ring) then (n:Integer * x:%):% == zero? n => 0 n>0 => double(n pretend PositiveInteger,x) double((-n) pretend PositiveInteger,-x) --% Rng +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of associative rings, not necessarily commutative, and not +++ necessarily with a 1. This is a combination of an abelian group +++ and a semigroup, with multiplication distributing over addition. +++ +++ Axioms: +++ \spad{ x*(y+z) = x*y + x*z} +++ \spad{ (x+y)*z = x*z + y*z } +++ +++ Conditional attributes: +++ \spadnoZeroDivisors\tab{25}\spad{ ab = 0 => a=0 or b=0} Rng(): Category == Join(AbelianGroup,SemiGroup) --% LeftModule +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of left modules over an rng (ring not necessarily with unit). +++ This is an abelian group which supports left multiplation by elements of +++ the rng. +++ +++ Axioms: +++ \spad{ (a*b)*x = a*(b*x) } +++ \spad{ (a+b)*x = (a*x)+(b*x) } +++ \spad{ a*(x+y) = (a*x)+(a*y) } LeftModule(R:Rng):Category == AbelianGroup with --operations *: (R,%) -> % ++ r*x returns the left multiplication of the module element x ++ by the ring element r. --% RightModule +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of right modules over an rng (ring not necessarily with unit). +++ This is an abelian group which supports right multiplation by elements of +++ the rng. +++ +++ Axioms: +++ \spad{ x*(a*b) = (x*a)*b } +++ \spad{ x*(a+b) = (x*a)+(x*b) } +++ \spad{ (x+y)*x = (x*a)+(y*a) } RightModule(R:Rng):Category == AbelianGroup with --operations *: (%,R) -> % ++ x*r returns the right multiplication of the module element x ++ by the ring element r. --% Ring +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of rings with unity, always associative, but +++ not necessarily commutative. Ring(): Category == Join(Rng,Monoid,LeftModule(%:Rng)) with --operations characteristic: () -> NonNegativeInteger ++ characteristic() returns the characteristic of the ring ++ this is the smallest positive integer n such that ++ \spad{n*x=0} for all x in the ring, or zero if no such n ++ exists. --We can not make this a constant, since some domains are mutable coerce: Integer -> % ++ coerce(i) converts the integer i to a member of the given domain. -- recip: % -> Union(%,"failed") -- inherited from Monoid unitsKnown ++ recip truly yields ++ reciprocal or "failed" if not a unit. ++ Note: \spad{recip(0) = "failed"}. add coerce(n:Integer):% == n * 1$% --% BiModule +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A \spadtype{BiModule} is both a left and right module with respect +++ to potentially different rings. +++ +++ Axiom: +++ \spad{ r*(x*s) = (r*x)*s } BiModule(R:Ring,S:Ring):Category == Join(LeftModule(R),RightModule(S)) with leftUnitary ++ \spad{1 * x = x} rightUnitary ++ \spad{x * 1 = x} --% EntireRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Entire Rings (non-commutative Integral Domains), i.e. a ring +++ not necessarily commutative which has no zero divisors. +++ +++ Axioms: +++ \spad{ab=0 => a=0 or b=0} -- known as noZeroDivisors +++ \spad{not(1=0)} EntireRing():Category == Join(Ring,BiModule(%:Ring,%:Ring)) with noZeroDivisors ++ if a product is zero then one of the factors ++ must be zero. --% CharacteristicZero +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Rings of Characteristic Zero. CharacteristicZero():Category == Ring --% CharacteristicNonZero +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Rings of Characteristic Non Zero CharacteristicNonZero():Category == Ring with charthRoot: % -> Union(%,"failed") ++ charthRoot(x) returns the pth root of x ++ where p is the characteristic of the ring. --% CommutativeRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of commutative rings with unity, i.e. rings where +++ \spadop{*} is commutative, and which have a multiplicative identity. +++ element. CommutativeRing():Category == Join(Ring,BiModule(%:Ring,%:Ring)) with commutative(*) ++ multiplication is commutative. --% Module +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of modules over a commutative ring. +++ +++ Axioms: +++ \spad{1*x = x} +++ \spad{(a*b)*x = a*(b*x)} +++ \spad{(a+b)*x = (a*x)+(b*x)} +++ \spad{a*(x+y) = (a*x)+(a*y)} Module(R:CommutativeRing): Category == BiModule(R,R) add if not(R is %) then (x:% * r:R):% == r*x --% Algebra +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of associative algebras (modules which are themselves rings). +++ +++ Axioms: +++ \spad{(b+c)::% = (b::%) + (c::%)} +++ \spad{(b*c)::% = (b::%) * (c::%)} +++ \spad{(1::R)::% = 1::%} +++ \spad{b*x = (b::%)*x} +++ \spad{r*(a*b) = (r*a)*b = a*(r*b)} Algebra(R:CommutativeRing): Category == Join(Ring, Module R) with --operations coerce: R -> % ++ coerce(r) maps the ring element r to a member of the algebra. add coerce(x:R):% == x * 1$% --% LinearlyExplicitRingOver +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ An extension ring with an explicit linear dependence test. LinearlyExplicitRingOver(R:Ring): Category == Ring with reducedSystem: Matrix % -> Matrix R ++ reducedSystem(A) returns a matrix B such that \spad{A x = 0} and \spad{B x = 0} ++ have the same solutions in R. reducedSystem: (Matrix %,Vector %) -> Record(mat:Matrix R,vec:Vector R) ++ reducedSystem(A, v) returns a matrix B and a vector w such that ++ \spad{A x = v} and \spad{B x = w} have the same solutions in R. --% FullyLinearlyExplicitRingOver +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ S is \spadtype{FullyLinearlyExplicitRingOver R} means that S is a +++ \spadtype{LinearlyExplicitRingOver R} and, in addition, if R is a +++ \spadtype{LinearlyExplicitRingOver Integer}, then so is S --FullyLinearlyExplicitRingOver(R:Ring):Category == -- LinearlyExplicitRingOver R with -- if (R has LinearlyExplicitRingOver Integer) then -- LinearlyExplicitRingOver Integer -- add -- if not(R is Integer) then -- if (R has LinearlyExplicitRingOver Integer) then -- reducedSystem(m:Matrix %):Matrix(Integer) == -- reducedSystem(reducedSystem(m)@Matrix(R)) -- -- reducedSystem(m:Matrix %, v:Vector %): -- Record(mat:Matrix(Integer), vec:Vector(Integer)) == -- rec := reducedSystem(m, v)@Record(mat:Matrix R, vec:Vector R) -- reducedSystem(rec.mat, rec.vec) --% IntegralDomain +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: Davenport & Trager I +++ Description: +++ The category of commutative integral domains, i.e. commutative +++ rings with no zero divisors. +++ +++ Conditional attributes: +++ canonicalUnitNormal\tab{20}the canonical field is the same for all associates +++ canonicalsClosed\tab{20}the product of two canonicals is itself canonical IntegralDomain(): Category == Join(CommutativeRing, Algebra(%:CommutativeRing), EntireRing) with --operations exquo: (%,%) -> Union(%,"failed") ++ exquo(a,b) either returns an element c such that ++ \spad{c*b=a} or "failed" if no such element can be found. unitNormal: % -> Record(unit:%,canonical:%,associate:%) ++ unitNormal(x) tries to choose a canonical element ++ from the associate class of x. ++ The attribute canonicalUnitNormal, if asserted, means that ++ the "canonical" element is the same across all associates of x ++ if \spad{unitNormal(x) = [u,c,a]} then ++ \spad{u*c = x}, \spad{a*u = 1}. unitCanonical: % -> % ++ \spad{unitCanonical(x)} returns \spad{unitNormal(x).canonical}. associates?: (%,%) -> Boolean ++ associates?(x,y) tests whether x and y are associates, i.e. ++ differ by a unit factor. unit?: % -> Boolean ++ unit?(x) tests whether x is a unit, i.e. is invertible. add -- declaration x,y: % -- definitions UCA ==> Record(unit:%,canonical:%,associate:%) if not (% has Field) then unitNormal(x:%):UCA == [1$%,x,1$%]$UCA -- the non-canonical definition unitCanonical(x:%):% == unitNormal(x).canonical -- always true recip(x:%):Union(%,"failed") == if zero? x then "failed" else exquo(1$%,x) unit?(x:%):Boolean == (recip x case "failed" => false; true) if % has canonicalUnitNormal then associates?(x:%, y:%):Boolean == (unitNormal x).canonical = (unitNormal y).canonical -- else -- associates?(x:%, y:%):Boolean == -- zero? x => zero? y -- zero? y => false -- exquo(x,y) case "failed" => false -- exquo(y,x) case "failed" => false -- true --% GcdDomain +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: Davenport & Trager 1 +++ Description: +++ This category describes domains where +++ \spadfun{gcd} can be computed but where there is no guarantee +++ of the existence of \spadfun{factor} operation for factorisation into irreducibles. +++ However, if such a \spadfun{factor} operation exist, factorization will be +++ unique up to order and units. GcdDomain(): Category == IntegralDomain with --operations gcd: (%,%) -> % ++ gcd(x,y) returns the greatest common divisor of x and y. -- gcd(x,y) = gcd(y,x) in the presence of canonicalUnitNormal, -- but not necessarily elsewhere gcd: List(%) -> % ++ gcd(l) returns the common gcd of the elements in the list l. lcm: (%,%) -> % ++ lcm(x,y) returns the least common multiple of x and y. -- lcm(x,y) = lcm(y,x) in the presence of canonicalUnitNormal, -- but not necessarily elsewhere lcm: List(%) -> % ++ lcm(l) returns the least common multiple of the elements of the list l. add lcm(x: %,y: %):% == y = 0 => 0 x = 0 => 0 LCM : Union(%,"failed") := exquo(y, gcd(x,y)) LCM case % => x * LCM error "bad gcd in lcm computation" lcm(l:List %):% == reduce(lcm,l,1,0) gcd(l:List %):% == reduce(gcd,l,0,1) --% UniqueFactorizationDomain +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A constructive unique factorization domain, i.e. where +++ we can constructively factor members into a product of +++ a finite number of irreducible elements. UniqueFactorizationDomain(): Category == GcdDomain with --operations prime?: % -> Boolean ++ prime?(x) tests if x can never be written as the product of two ++ non-units of the ring, ++ i.e., x is an irreducible element. squareFree : % -> Factored(%) ++ squareFree(x) returns the square-free factorization of x ++ i.e. such that the factors are pairwise relatively prime ++ and each has multiple prime factors. squareFreePart: % -> % ++ squareFreePart(x) returns a product of prime factors of ++ x each taken with multiplicity one. factor: % -> Factored(%) ++ factor(x) returns the factorization of x into irreducibles. add squareFreePart(x:%):% == unit(s := squareFree x) * reduce(*,[f.factor for f in factors s]) --% PrincipalIdealDomain +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of constructive principal ideal domains, i.e. +++ where a single generator can be constructively found for +++ any ideal given by a finite set of generators. +++ Note that this constructive definition only implies that +++ finitely generated ideals are principal. It is not clear +++ what we would mean by an infinitely generated ideal. PrincipalIdealDomain(): Category == GcdDomain with --operations principalIdeal: List % -> Record(coef:List %,generator:%) ++ principalIdeal([f1,...,fn]) returns a record whose ++ generator component is a generator of the ideal ++ generated by \spad{[f1,...,fn]} whose coef component satisfies ++ \spad{generator = sum (input.i * coef.i)} expressIdealMember: (List %,%) -> Union(List %,"failed") ++ expressIdealMember([f1,...,fn],h) returns a representation ++ of h as a linear combination of the fi or "failed" if h ++ is not in the ideal generated by the fi. --% EuclideanDomain +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A constructive euclidean domain, i.e. one can divide producing +++ a quotient and a remainder where the remainder is either zero +++ or is smaller (\spadfun{euclideanSize}) than the divisor. +++ +++ Conditional attributes: +++ multiplicativeValuation\tab{25}\spad{Size(a*b)=Size(a)*Size(b)} +++ additiveValuation\tab{25}\spad{Size(a*b)=Size(a)+Size(b)} EuclideanDomain(): Category == PrincipalIdealDomain with --operations sizeLess?: (%,%) -> Boolean ++ sizeLess?(x,y) tests whether x is strictly ++ smaller than y with respect to the \spadfunFrom{euclideanSize}{EuclideanDomain}. euclideanSize: % -> NonNegativeInteger ++ euclideanSize(x) returns the euclidean size of the element x. ++ Error: if x is zero. divide: (%,%) -> Record(quotient:%,remainder:%) ++ divide(x,y) divides x by y producing a record containing a ++ \spad{quotient} and \spad{remainder}, ++ where the remainder is smaller (see \spadfunFrom{sizeLess?}{EuclideanDomain}) ++ than the divisor y. quo : (%,%) -> % ++ x quo y is the same as \spad{divide(x,y).quotient}. ++ See \spadfunFrom{divide}{EuclideanDomain}. rem: (%,%) -> % ++ x rem y is the same as \spad{divide(x,y).remainder}. ++ See \spadfunFrom{divide}{EuclideanDomain}. extendedEuclidean: (%,%) -> Record(coef1:%,coef2:%,generator:%) -- formerly called princIdeal ++ extendedEuclidean(x,y) returns a record rec where ++ \spad{rec.coef1*x+rec.coef2*y = rec.generator} and ++ rec.generator is a gcd of x and y. ++ The gcd is unique only ++ up to associates if \spadatt{canonicalUnitNormal} is not asserted. ++ \spadfun{principalIdeal} provides a version of this operation ++ which accepts an arbitrary length list of arguments. extendedEuclidean: (%,%,%) -> Union(Record(coef1:%,coef2:%),"failed") -- formerly called expressIdealElt ++ extendedEuclidean(x,y,z) either returns a record rec ++ where \spad{rec.coef1*x+rec.coef2*y=z} or returns "failed" ++ if z cannot be expressed as a linear combination of x and y. multiEuclidean: (List %,%) -> Union(List %,"failed") ++ multiEuclidean([f1,...,fn],z) returns a list of coefficients ++ \spad{[a1, ..., an]} such that ++ \spad{ z / prod fi = sum aj/fj}. ++ If no such list of coefficients exists, "failed" is returned. add -- declarations x,y,z: % l: List % -- definitions sizeLess?(x:%,y:%):Boolean == zero? y => false zero? x => true euclideanSize(x) "failed" qr:=divide(x,y) zero?(qr.remainder) => qr.quotient "failed" gcd(x:%, y:%):% == --Euclidean Algorithm x:=unitCanonical x y:=unitCanonical y while not zero? y repeat (x,y):= (y,x rem y) y:=unitCanonical y -- this doesn't affect the -- correctness of Euclid's algorithm, -- but -- a) may improve performance -- b) ensures gcd(x,y)=gcd(y,x) -- if canonicalUnitNormal x IdealElt ==> Record(coef1:%,coef2:%,generator:%) unitNormalizeIdealElt(s:IdealElt):IdealElt == (u,c,a):=unitNormal(s.generator) one? a => s [a*s.coef1,a*s.coef2,c]$IdealElt extendedEuclidean(x:%,y:%):IdealElt == --Extended Euclidean Algorithm s1:=unitNormalizeIdealElt([1$%,0$%,x]$IdealElt) s2:=unitNormalizeIdealElt([0$%,1$%,y]$IdealElt) zero? y => s1 zero? x => s2 while not zero?(s2.generator) repeat qr:= divide(s1.generator, s2.generator) s3:=[s1.coef1 - qr.quotient * s2.coef1, s1.coef2 - qr.quotient * s2.coef2, qr.remainder]$IdealElt s1:=s2 s2:=unitNormalizeIdealElt s3 if not(zero?(s1.coef1)) and not sizeLess?(s1.coef1,y) then qr:= divide(s1.coef1,y) s1.coef1:= qr.remainder s1.coef2:= s1.coef2 + qr.quotient * x s1 := unitNormalizeIdealElt s1 s1 TwoCoefs ==> Record(coef1:%,coef2:%) extendedEuclidean(x:%,y:%,z:%):TwoCoefs == zero? z => [0,0]$TwoCoefs s:= extendedEuclidean(x,y) (w:= exquo(z, s.generator)) case "failed" => "failed" zero? y => [s.coef1 * w, s.coef2 * w]$TwoCoefs qr:= divide((s.coef1 * w), y) [qr.remainder, s.coef2 * w + qr.quotient * x]$TwoCoefs principalIdeal(l:List %):List % == l = [] => error "empty list passed to principalIdeal" rest l = [] => uca:=unitNormal(first l) [[uca.unit],uca.canonical] rest rest l = [] => u:= extendedEuclidean(first l,second l) [[u.coef1, u.coef2], u.generator] v:=principalIdeal rest l u:= extendedEuclidean(first l,v.generator) [cons(u.coef1,[u.coef2*vv for vv in v.coef]),u.generator] expressIdealMember(l:List %, z:%):List % == z = 0 => [0 for v in l] pid := principalIdeal l (q := exquo(z, pid.generator)) case "failed" => "failed" [q*v for v in pid.coef] multiEuclidean(l:List %,z:%):List % == empty? l => error "empty list passed to multiEuclidean" empty? rest l => expressIdealMember(l,z) u:= extendedEuclidean(first l,_*/rest l,z) u case "failed" => "failed" rest rest l = [] => [u.coef2,u.coef1] v:=multiEuclidean(rest l,u.coef1) v case "failed" => "failed" cons(u.coef2,v) --% DivisionRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A division ring (sometimes called a skew field), +++ i.e. a not necessarily commutative ring where +++ all non-zero elements have multiplicative inverses. DivisionRing(): Category == Join(EntireRing, Algebra Fraction Integer) with ^: (%,Integer) -> % ++ x^n returns x raised to the integer power n. inv : % -> % ++ inv x returns the multiplicative inverse of x. ++ Error: if x is 0. -- Q-algebra is a lie, should be conditional on characteristic 0, -- but knownInfo cannot handle the following commented -- if % has CharacteristicZero then Algebra Fraction Integer add n: Integer x: % import RepeatedSquaring(%) (x:% ^ n: Integer):% == zero? n => 1 zero? x => n<0 => error "division by zero" x n<0 => expt(recip(x) pretend %,(-n) pretend PositiveInteger) expt(x,n pretend PositiveInteger) -- if % has CharacteristicZero() then (q:Fraction(Integer) * x:%):% == numer(q) * inv(denom(q)::%) * x --% Field +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of commutative fields, i.e. commutative rings +++ where all non-zero elements have multiplicative inverses. +++ The \spadfun{factor} operation while trivial is useful to have defined. +++ +++ Axioms: +++ \spad{a*(b/a) = b} +++ \spad{inv(a) = 1/a} Field(): Category == Join(EuclideanDomain,UniqueFactorizationDomain, DivisionRing) with --operations /: (%,%) -> % ++ x/y divides the element x by the element y. ++ Error: if y is 0. canonicalUnitNormal ++ either 0 or 1. canonicalsClosed ++ since \spad{0*0=0}, \spad{1*1=1} add --declarations x,y: % n: Integer -- definitions UCA ==> Record(unit:%,canonical:%,associate:%) unitNormal(x:%):UCA == if zero? x then [1$%,0$%,1$%]$UCA else [x,1$%,inv(x)]$UCA unitCanonical(x:%):% == if zero? x then x else 1 associates?(x:%,y:%):Boolean == if zero? x then zero? y else not(zero? y) inv(x:%):% ==((u:=recip x) case "failed" => error "not invertible"; u) exquo(x:%, y:%):Union(%,"failed") == (y=0 => "failed"; x / y) gcd(x:%,y:%):% == 1 euclideanSize(x:%):NonNegativeInteger == 0 prime?(x:%):Boolean == false squareFree(x:%):Factored(%) == x::Factored(%) factor(x:%):Factored(%) == x::Factored(%) (x:% / y:%):% == (zero? y => error "catdef: division by zero"; x * inv(y)) divide(x:%,y:%):Record(quotient:%,remainder:%) == [x / y,0] --% Finite +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of domains composed of a finite set of elements. +++ We include the functions \spadfun{lookup} and \spadfun{index} to give a bijection +++ between the finite set and an initial segment of positive integers. +++ +++ Axioms: +++ \spad{lookup(index(n)) = n} +++ \spad{index(lookup(s)) = s} Finite(): Category == SetCategory with --operations size: () -> NonNegativeInteger ++ size() returns the number of elements in the set. index: PositiveInteger -> % ++ index(i) takes a positive integer i less than or equal ++ to \spad{size()} and ++ returns the \spad{i}-th element of the set. This operation establishs a bijection ++ between the elements of the finite set and \spad{1..size()}. lookup: % -> PositiveInteger ++ lookup(x) returns a positive integer such that ++ \spad{x = index lookup x}. random: () -> % ++ random() returns a random element from the set. --++ A Field which happens to be finite --FiniteFieldCategory(): Category == -- Join(Field,Finite,StepThrough,CharacteristicNonZero) with -- charthRoot: % -> % -- ++ Takes the Characteristic'th root of something. -- ++ Such a root is always defined in finite fields, i.e. the operation -- ++ cannot fail. -- conditionP: Matrix % -> Union(Vector %,"failed") -- ++ given a matrix representing a homogeneous system of equations, -- ++ returns a vector whose characteristic'th powers is a non-trivial -- ++ solution. -- ++ If no such no-trivial solution exists, "failed" is returned. -- add -- mat: Matrix % -- conditionP mat == -- l:=nullSpace mat -- empty? l or every?(zero?, first l) => "failed" -- map(charthRoot,first l) -- charthRoot x == x^(size() quo characteristic()) -- --FinitePrimeField():Category == -- Join(FiniteFieldCategory,ConvertibleTo Integer) -- add -- charthRoot(x) == x -- Not used elsewhere, and it's not clear what "coeffField" does --SimpleFieldExtension(): Category == Field with -- --operations -- coefField: -> Field -- generator: -> % --% VectorSpace +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Vector Spaces (not necessarily finite dimensional) over a field. VectorSpace(S:Field): Category == Module(S) with / : (%, S) -> % ++ x/y divides the vector x by the scalar y. dimension: () -> CardinalNumber ++ dimension() returns the dimensionality of the vector space. --% OrderedSet +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The class of totally ordered sets, that is, sets such that for each pair of elements \spad{(a,b)} +++ exactly one of the following relations holds \spad{a a Boolean ++ x < y is a strict total ordering on the elements of the set. max: (%,%) -> % ++ max(x,y) returns the maximum of x and y relative to <. min: (%,%) -> % ++ min(x,y) returns the minimum of x and y relative to <. add --declarations x,y: % --definitions -- These really ought to become some sort of macro max(x:%,y:%):% == x > y => x y min(x:%,y:%):% == x > y => y x --% OrderedFinite +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered finite sets. OrderedFinite(): Category == Join(OrderedSet, Finite) --% OrderedMonoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also monoids, such that multiplication +++ preserves the ordering. +++ +++ Axioms: +++ \spad{x < y => x*z < y*z} +++ \spad{x < y => z*x < z*y} OrderedMonoid(): Category == Join(OrderedSet, Monoid) --% OrderedAbelianSemiGroup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also abelian semigroups, such that the addition +++ preserves the ordering. +++ \spad{ x < y => x+z < y+z} OrderedAbelianSemiGroup(): Category == Join(OrderedSet, AbelianMonoid) --% OrderedAbelianMonoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also abelian monoids, such that the addition +++ preserves the ordering. OrderedAbelianMonoid(): Category == Join(OrderedAbelianSemiGroup, AbelianMonoid) --% OrderedCancellationAbelianMonoid +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also abelian cancellation monoids, such that the addition +++ preserves the ordering. OrderedCancellationAbelianMonoid(): Category == Join(OrderedAbelianMonoid, CancellationAbelianMonoid) --% OrderedAbelianGroup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also abelian groups, such that the addition preserves +++ the ordering. OrderedAbelianGroup(): Category == Join(OrderedCancellationAbelianMonoid, AbelianGroup) --% OrderedRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Ordered sets which are also rings, that is, domains where the ring +++ operations are compatible with the ordering. +++ +++ Axiom: +++ \spad{0 ab< ac} OrderedRing(): Category == Join(OrderedAbelianGroup,Ring,Monoid) with positive?: % -> Boolean ++ positive?(x) tests whether x is strictly greater than 0. negative?: % -> Boolean ++ negative?(x) tests whether x is strictly less than 0. sign : % -> Integer ++ sign(x) is 1 if x is positive, -1 if x is negative, 0 if x equals 0. abs : % -> % ++ abs(x) returns the absolute value of x. add positive?(x:%):Boolean == x>0 negative?(x:%):Boolean == x<0 sign(x:%):Integer == positive? x => 1 negative? x => -1 zero? x => 0 error "x satisfies neither positive?, negative? or zero?" abs(x:%):% == positive? x => x negative? x => -x zero? x => 0 error "x satisfies neither positive?, negative? or zero?" --% OrderedAbelianMonoidSup +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ This domain is an OrderedAbelianMonoid with a \spadfun{sup} operation added. +++ The purpose of the \spadfun{sup} operator in this domain is to act as a supremum +++ with respect to the partial order imposed by \spadop{-}, rather than with respect to +++ the total \spad{>} order (since that is "max"). +++ +++ Axioms: +++ \spad{sup(a,b)-a ~= "failed"} +++ \spad{sup(a,b)-b ~= "failed"} +++ \spad{x-a ~= "failed" and x-b ~= "failed" => x >= sup(a,b)} OrderedAbelianMonoidSup(): Category == OrderedCancellationAbelianMonoid with --operation sup: (%,%) -> % ++ sup(x,y) returns the least element from which both ++ x and y can be subtracted. --% DifferentialRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ An ordinary differential ring, that is, a ring with an operation +++ \spadfun{differentiate}. +++ +++ Axioms: +++ \spad{differentiate(x+y) = differentiate(x)+differentiate(y)} +++ \spad{differentiate(x*y) = x*differentiate(y) + differentiate(x)*y} DifferentialRing(): Category == Ring with differentiate: % -> % ++ differentiate(x) returns the derivative of x. ++ This function is a simple differential operator ++ where no variable needs to be specified. D: % -> % ++ D(x) returns the derivative of x. ++ This function is a simple differential operator ++ where no variable needs to be specified. differentiate: (%, NonNegativeInteger) -> % ++ differentiate(x, n) returns the n-th derivative of x. D: (%, NonNegativeInteger) -> % ++ D(x, n) returns the n-th derivative of x. add D(r:%):% == differentiate r differentiate(r:%, n:NonNegativeInteger):% == for i in 1..n repeat r := differentiate r r D(r:%,n:NonNegativeInteger):% == differentiate(r,n) --% PartialDifferentialRing +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ A partial differential ring with differentiations indexed by a parameter type S. +++ +++ Axioms: +++ \spad{differentiate(x+y,e) = differentiate(x,e)+differentiate(y,e)} +++ \spad{differentiate(x*y,e) = x*differentiate(y,e) + differentiate(x,e)*y} PartialDifferentialRing(S:SetCategory): Category == Ring with differentiate: (%, S) -> % ++ differentiate(x,v) computes the partial derivative of x ++ with respect to s. differentiate: (%, List S) -> % ++ differentiate(x,[s1,...sn]) computes successive partial derivatives, ++ i.e. \spad{differentiate(...differentiate(x, s1)..., sn)}. differentiate: (%, S, NonNegativeInteger) -> % ++ differentiate(x, s, n) computes multiple partial derivatives, i.e. ++ n-th derivative of x with respect to s. differentiate: (%, List S, List NonNegativeInteger) -> % ++ differentiate(x, [s1,...,sn], [n1,...,nn]) computes ++ multiple partial derivatives, i.e. D: (%, S) -> % ++ D(x,v) computes the partial derivative of x ++ with respect to s. D: (%, List S) -> % ++ D(x,[s1,...sn]) computes successive partial derivatives, ++ i.e. \spad{D(...D(x, s1)..., sn)}. D: (%, S, NonNegativeInteger) -> % ++ D(x, s, n) computes multiple partial derivatives, i.e. ++ n-th derivative of x with respect to s. D: (%, List S, List NonNegativeInteger) -> % ++ D(x, [s1,...,sn], [n1,...,nn]) computes ++ multiple partial derivatives, i.e. ++ \spad{D(...D(x, s1, n1)..., sn, nn)}. add differentiate(r:%, l:List S):% == for s in l repeat r := differentiate(r, s) r differentiate(r:%, s:S, n:NonNegativeInteger):% == for i in 1..n repeat r := differentiate(r, s) r differentiate(r:%, ls:List S, ln:List NonNegativeInteger):% == for s in ls for n in ln repeat r := differentiate(r, s, n) r D(r:%, v:S):% == differentiate(r,v) D(r:%, lv:List S):% == differentiate(r,lv) D(r:%, v:S, n:NonNegativeInteger):% == differentiate(r,v,n) D(r:%, lv:List S, ln:List NonNegativeInteger):% == differentiate(r, lv, ln) --% DifferentialExtension +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ Differential extensions of a ring R. +++ Given a differentiation on R, extend it to a differentiation on %. DifferentialExtension(R:Ring): Category == Ring with --operations differentiate: (%, R -> R) -> % ++ differentiate(x, deriv) differentiates x extending ++ the derivation deriv on R. differentiate: (%, R -> R, NonNegativeInteger) -> % ++ differentiate(x, deriv, n) differentiate x n times ++ using a derivation which extends deriv on R. D: (%, R -> R) -> % ++ D(x, deriv) differentiates x extending ++ the derivation deriv on R. D: (%, R -> R, NonNegativeInteger) -> % ++ D(x, deriv, n) differentiate x n times ++ using a derivation which extends deriv on R. -- if R has DifferentialRing then DifferentialRing -- if R has PartialDifferentialRing(Symbol) then -- PartialDifferentialRing(Symbol) add differentiate(x:%, derivation: R -> R, n:NonNegativeInteger):% == for i in 1..n repeat x := differentiate(x, derivation) x D(x:%, derivation: R -> R):% == differentiate(x, derivation) D(x:%, derivation: R -> R, n:NonNegativeInteger):% == differentiate(x, derivation, n) if R has DifferentialRing then differentiate(x:%):% == differentiate(x, differentiate$R) if R has PartialDifferentialRing Symbol then differentiate(x:%, v:Symbol):% == differentiate(x, differentiate(#1, v)$R) --% RealConstant +++ Author: +++ Date Created: +++ Date Last Updated: +++ Basic Functions: +++ Related Constructors: +++ Also See: +++ AMS Classifications: +++ Keywords: +++ References: +++ Description: +++ The category of real numeric domains, i.e. convertible to floats. RealConstant(): Category == Join(ConvertibleTo SmallFloat, ConvertibleTo Float)