--* From BMT%WATSON.vnet.ibm.com@yktvmh.watson.ibm.com Sat Jun 26 11:13:57 1993 --* Received: from yktvmh.watson.ibm.com by radical.watson.ibm.com (AIX 3.2/UCB 5.64/900524) --* id AA15688; Sat, 26 Jun 1993 11:13:57 -0400 --* Received: from watson.vnet.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3) --* with BSMTP id 0227; Sat, 26 Jun 93 11:14:47 EDT --* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0" --* id --* for asbugs@watson; Sat, 26 Jun 93 11:14:47 -0400 --* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0" --* id 4105; Sat, 26 Jun 1993 11:14:45 EDT --* Received: from cyst.watson.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3) --* with TCP; Sat, 26 Jun 93 11:14:44 EDT --* Received: from spadserv.watson.ibm.com by cyst.watson.ibm.com (AIX 3.2/UCB 5.64/900528) --* id AA42033; Sat, 26 Jun 1993 10:07:46 -0400 --* Received: by spadserv.watson.ibm.com (AIX 3.2/UCB 5.64/900524) --* id AA20227; Sat, 26 Jun 1993 10:10:17 -0400 --* Date: Sat, 26 Jun 1993 10:10:17 -0400 --* From: bmt@spadserv.watson.ibm.com --* X-External-Networks: yes --* Message-Id: <9306261410.AA20227@spadserv.watson.ibm.com> --* To: asbugs@watson.ibm.com --* Subject: both compiler errors seem wrong [catdef6.as][28.I (current)] --@ Fixed by: SSD Fri Jul 16 15:37:28 1993 --@ Tested by: none --@ Summary: v29.2 does not give any type errors for this file. --Copyright The Numerical Algorithms Group Limited 1991. #include "aslib.as" #library DemoLib "asdem" import DemoLib Boolean ==> Bit SmallInteger ==> SingleInteger Object ==> Type SetCategory ==> BasicType --% Basic AXIOM Categories --% 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: () -> % ++ init() chooses an initial object for stepping. nextItem: % -> Partial % ++ 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. --% 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 OldMonoid: Category == SemiGroup with --operations 1: % ++ 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: % -> Partial % ++ recip(x) tries to compute the multiplicative inverse for x ++ or "failed" if it cannot find the inverse (see unitsKnown). --% 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}. --% 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. --% 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 OldAbelianMonoid: Category == AbelianSemiGroup with --operations 0: % ++ 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 --% 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: (%,%) -> Partial(%) ++ 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 OldAbelianGroup: 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. --% 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. OldRing: Category == Join(Rng,Monoid,LeftModule(% pretend 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: % -> Partial(%) -- inherited from Monoid -- unitsKnown ++ recip truly yields ++ reciprocal or "failed" if not a unit. ++ Note: \spad{recip(0) = "failed"}. --% 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:Rng,S:Rng):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(% pretend Rng,% pretend Rng)) 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: % -> Partial(%) ++ 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(% pretend Rng,% pretend Rng)) 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 pretend Rng,R pretend Rng) --% 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. --% 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(% pretend CommutativeRing), EntireRing) with --operations exquo: (%,%) -> Partial(%) ++ 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. --% 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. OldGcdDomain: 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 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