-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A library of constructive algebra. -- -- A library of algebra focusing mainly on commutative ring theory from a -- constructive point of view. -- -- Classical structures are implemented without Noetherian assumptions. -- This means that it is not assumed that all ideals are finitely -- generated. For example, instead of principal ideal domains one gets -- Bezout domains which are integral domains in which all finitely -- generated ideals are principal (and not necessarily that all ideals -- are principal). @package constructive-algebra @version 0.1.3 -- | Type level characters. Used for representing the variable name in -- univariate polynomials. module Algebra.TypeChar.Char data A_ data B_ data C_ data D_ data E_ data F_ data G_ data H_ data I_ data J_ data K_ data L_ data M_ data N_ data O_ data P_ data Q_ data R_ data S_ data T_ data U_ data V_ data W_ data X_ data Y_ data Z_ data A data B data C data D data E data F data G data H data I data J data K data L data M data N data O data P data Q data R data S data T data U data V data W data X data Y data Z instance Show Z instance Show Y instance Show X instance Show W instance Show V instance Show U instance Show T instance Show S instance Show R instance Show Q instance Show P instance Show O instance Show N instance Show M instance Show L instance Show K instance Show J instance Show I instance Show H instance Show G instance Show F instance Show E instance Show D instance Show C instance Show B instance Show A instance Show Z_ instance Show Y_ instance Show X_ instance Show W_ instance Show V_ instance Show U_ instance Show T_ instance Show S_ instance Show R_ instance Show Q_ instance Show P_ instance Show O_ instance Show N_ instance Show M_ instance Show L_ instance Show K_ instance Show J_ instance Show I_ instance Show H_ instance Show G_ instance Show F_ instance Show E_ instance Show D_ instance Show C_ instance Show B_ instance Show A_ -- | The representation of the ring structure. module Algebra.Structures.Ring -- | Definition of rings. class Ring a (<+>) :: (Ring a) => a -> a -> a (<*>) :: (Ring a) => a -> a -> a neg :: (Ring a) => a -> a zero :: (Ring a) => a one :: (Ring a) => a -- | Specification of rings. Test that the arguments satisfy the ring -- axioms. propRing :: (Ring a, Eq a) => a -> a -> a -> Property -- | Subtraction (<->) :: (Ring a) => a -> a -> a -- | Exponentiation (<^>) :: (Ring a) => a -> Integer -> a -- | Multiply from left with an integer; n *> x means x + x + ... + x, n -- times. (*>) :: (Ring a) => Int -> a -> a -- | Summation sumRing :: (Ring a) => [a] -> a -- | Product productRing :: (Ring a) => [a] -> a module Algebra.Structures.CommutativeRing -- | Definition of commutative rings. class (Ring a) => CommutativeRing a -- | Specification of commutative rings. Test that multiplication is -- commutative and that it satisfies the ring axioms. propCommutativeRing :: (CommutativeRing a, Eq a) => a -> a -> a -> Property -- | Finitely generated ideals in commutative rings. module Algebra.Ideal -- | Ideals characterized by their list of generators. data (CommutativeRing a) => Ideal a Id :: [a] -> Ideal a -- | The zero ideal. zeroIdeal :: (CommutativeRing a) => Ideal a -- | Test if an ideal is principal. isPrincipal :: (CommutativeRing a) => Ideal a -> Bool fromId :: (CommutativeRing a) => Ideal a -> [a] -- | Evaluate the ideal at a certain point. eval :: (CommutativeRing a) => a -> Ideal a -> a -- | Addition of ideals. addId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a -- | Multiplication of ideals. mulId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a -- | Test if an operations compute the correct ideal. The operation should -- give a witness that the comuted ideal contains the same elements. -- -- If [ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ] -- -- Then the witness should give that -- -- z_k = a_k1 * x_1 + ... + a_kn * x_n = b_k1 * y_1 + ... + b_km * y_m -- -- This is used to check that the intersection computed is correct. isSameIdeal :: (CommutativeRing a, Eq a) => (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Ideal a -> Ideal a -> Bool -- | Compute witnesses for two lists for the zero ideal. This is used when -- computing the intersection of two ideals. zeroIdealWitnesses :: (CommutativeRing a) => [a] -> [a] -> (Ideal a, [[a]], [[a]]) instance (CommutativeRing a, Arbitrary a, Eq a) => Arbitrary (Ideal a) instance (CommutativeRing a, Show a) => Show (Ideal a) module Algebra.Structures.StronglyDiscrete -- | Strongly discrete rings -- -- A ring is called strongly discrete if ideal membership is decidable. -- Nothing correspond to that x is not in the ideal and Just is the -- witness. Examples include all Bezout domains and polynomial rings. class (Ring a) => StronglyDiscrete a member :: (StronglyDiscrete a) => a -> Ideal a -> Maybe [a] -- | Test that the witness is actually a witness that the element is in the -- ideal. propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool module Algebra.Structures.IntegralDomain -- | Definition of integral domains. class (CommutativeRing a) => IntegralDomain a -- | Specification of integral domains. Test that there are no -- zero-divisors and that it satisfies the axioms of commutative rings. propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property -- | Representation of Euclidean domains. That is integral domains with an -- Euclidean functions and decidable division. module Algebra.Structures.EuclideanDomain -- | Euclidean domains -- -- Given a and b compute (q,r) such that a = bq + r and r = 0 || d r < -- d b. Where d is the Euclidean function. class (IntegralDomain a) => EuclideanDomain a d :: (EuclideanDomain a) => a -> Integer quotientRemainder :: (EuclideanDomain a) => a -> a -> (a, a) propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property modulo :: (EuclideanDomain a) => a -> a -> a quotient :: (EuclideanDomain a) => a -> a -> a divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool -- | The Euclidean algorithm for calculating the GCD of a and b. euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a -- | Generalized Euclidean algorithm to compute GCD of a list of elements. genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a -- | Lowest common multiple, (a*b)/gcd(a,b). lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a -- | Generalized lowest common multiple to compute lcm of a list of -- elements. genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a -- | The extended Euclidean algorithm. -- -- Computes x and y in ax + by = gcd(a,b). extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a, a) -- | Generalized extended Euclidean algorithm. -- -- Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n) genExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> [a] -- | A small simple matrix library. module Algebra.Matrix -- | Row vectors newtype Vector r Vec :: [r] -> Vector r unVec :: Vector r -> [r] lengthVec :: Vector r -> Int -- | Matrices newtype Matrix r M :: [Vector r] -> Matrix r -- | Construct a mxn matrix. matrix :: [[r]] -> Matrix r matrixToVector :: Matrix r -> Vector r vectorToMatrix :: Vector r -> Matrix r unMVec :: Matrix r -> [[r]] unM :: Matrix r -> [Vector r] -- | Construct a nxn identity matrix. identity :: (IntegralDomain r) => Int -> Matrix r -- | Matrix multiplication. mulM :: (Ring r) => Matrix r -> Matrix r -> Matrix r -- | Matrix addition. addM :: (Ring r) => Matrix r -> Matrix r -> Matrix r -- | Transpose a matrix. transpose :: Matrix r -> Matrix r isSquareMatrix :: Matrix r -> Bool -- | Compute the dimension of a matrix. dimension :: Matrix r -> (Int, Int) instance (Eq r) => Eq (Matrix r) instance (Eq r) => Eq (Vector r) instance (Eq r, Arbitrary r, Ring r) => Arbitrary (Matrix r) instance (Show r) => Show (Matrix r) instance (Ring r, Arbitrary r, Eq r) => Arbitrary (Vector r) instance (Show r) => Show (Vector r) -- | Representation of coherent rings. Traditionally a ring is coherent if -- every finitely generated ideal is finitely presented. This means that -- it is possible to solve homogenous linear equations in them. module Algebra.Structures.Coherent -- | Definition of coherent rings. -- -- We say that R is coherent iff for any M, we can find L such that ML=0 -- and -- -- MX=0 <-> exists Y. X=LY -- -- that is, iff we can generate the solutions of any linear homogeous -- system of equations. -- -- The main point here is that ML=0, it is not clear how to represent the -- equivalence in Haskell. This would probably be possible in type -- theory. class (IntegralDomain a) => Coherent a solve :: (Coherent a) => Vector a -> Matrix a propCoherent :: (Coherent a, Eq a) => Vector a -> Bool -- | Solves a system of equations. solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a -- | Test that the solution of an MxN system is in fact a solution of the -- system propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool -- | Intersection computable -> Coherence. -- -- Proof that if there is an algorithm to compute a f.g. set of -- generators for the intersection of two f.g. ideals then the ring is -- coherent. -- -- Takes the vector to solve, [x1,...,xn], and a function (int) that -- computes the intersection of two ideals. -- -- If -- -- [ x_1, ..., x_n ] `int` [ y_1, ..., y_m ] = [ z_1, ..., z_l ] -- -- then int should give witnesses us and vs such that: -- -- z_k = n_k1 * x_1 + ... + u_kn * x_n -- -- = u_k1 * y_1 + ... + n_km * y_m solveWithIntersection :: (IntegralDomain a, Eq a) => Vector a -> (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Matrix a -- | Strongly discrete coherent rings. -- -- If the ring is strongly discrete and coherent then we can solve -- arbitrary equations of the type AX=b. solveGeneralEquation :: (Coherent a, StronglyDiscrete a) => Vector a -> a -> Maybe (Matrix a) propSolveGeneralEquation :: (Coherent a, StronglyDiscrete a, Eq a) => Vector a -> a -> Bool -- | Solves general linear systems of the kind AX = B. -- -- A is given as a matrix and B is given as a row vector (it should be -- column vector). solveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Maybe (Matrix a, Matrix a) propSolveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Property -- | Representation of Bezout domains. That is non-Noetherian analogues of -- principal ideal domains. This means that all finitely generated ideals -- are principal. module Algebra.Structures.BezoutDomain -- | Bezout domains -- -- Compute a principal ideal from another ideal. Also give witness that -- the principal ideal is equal to the first ideal. -- -- toPrincipal <a_1,...,a_n> = (<a>,u_i,v_i) where -- -- sum (u_i * a_i) = a -- -- a_i = v_i * a class (IntegralDomain a) => BezoutDomain a toPrincipal :: (BezoutDomain a) => Ideal a -> (Ideal a, [a], [a]) propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property dividesB :: (BezoutDomain a, Eq a) => a -> a -> Bool -- | Intersection without witness. intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a -- | Intersection of ideals with witness. -- -- If one of the ideals is the zero ideal then the intersection is the -- zero ideal. intersectionBWitness :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]]) -- | Coherence of Bezout domains. solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a instance (BezoutDomain a, Eq a) => StronglyDiscrete a instance (EuclideanDomain a, Eq a) => BezoutDomain a -- | Specification of principal localization matrices used in the coherence -- proof of Prufer domains. module Algebra.PLM -- | A principal localization matrix for an ideal (x1,...,xn) is a matrix -- such that: -- -- propPLM :: (CommutativeRing a, Eq a) => Ideal a -> Matrix a -> Bool -- | Principal localization matrices for ideals are computable in Bezout -- domains. computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a -- | Greatest common divisor (GCD) domains. -- -- GCD domains are integral domains in which every pair of nonzero -- elements have a greatest common divisor. They can also be -- characterized as non-Noetherian analogues of unique factorization -- domains. module Algebra.Structures.GCDDomain -- | GCD domains class (IntegralDomain a) => GCDDomain a gcd' :: (GCDDomain a) => a -> a -> (a, a, a) -- | Specification of GCD domains. They are integral domains in which every -- pair of nonzero elements have a greatest common divisor. propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property instance (BezoutDomain a) => GCDDomain a module Algebra.Z -- | Type synonym for integers. type Z = Integer -- | Definition of rings. class Ring a (<+>) :: (Ring a) => a -> a -> a (<*>) :: (Ring a) => a -> a -> a neg :: (Ring a) => a -> a zero :: (Ring a) => a one :: (Ring a) => a instance Coherent Z instance EuclideanDomain Z instance IntegralDomain Z instance CommutativeRing Z instance Ring Z module Algebra.Structures.Field -- | Definition of fields. class (IntegralDomain a) => Field a inv :: (Field a) => a -> a -- | Specification of fields. Test that the multiplicative inverses behave -- as expected and that it satisfies the axioms of integral domains. propField :: (Field a, Eq a) => a -> a -> a -> Property -- | Division () :: (Field a) => a -> a -> a -- | The field of fractions over a GCD domain. The reason that it is an GCD -- domain is that we only want to work over reduced quotients. module Algebra.Structures.FieldOfFractions -- | Field of fractions newtype (GCDDomain a) => FieldOfFractions a F :: (a, a) -> FieldOfFractions a -- | Embed a value in the field of fractions. toFieldOfFractions :: (GCDDomain a) => a -> FieldOfFractions a -- | Extract a value from the field of fractions. This is only possible if -- the divisor is one. fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a -- | Reduce an element. reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a instance (GCDDomain a, Eq a) => Field (FieldOfFractions a) instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a) instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a) instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a) instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a) instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a) instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a) -- | Representation of rational numbers as the field of fractions of Z. module Algebra.Q -- | Q is the field of fractions of Z. type Q = FieldOfFractions Z toQ :: Z -> Q toZ :: Q -> Z instance Fractional Q instance Num Q module Algebra.UPoly -- | Polynomials over a commutative ring, indexed by a phantom type x that -- denote the name of the variable that the polynomial is over. For -- example UPoly Q X_ is Q[x] and UPoly Q T_ is Q[t]. newtype (CommutativeRing r) => UPoly r x UP :: [r] -> UPoly r x -- | The degree of the polynomial. deg :: (CommutativeRing r) => UPoly r x -> Integer -- | Useful shorthand for Q[x]. type Qx = UPoly Q X_ -- | The variable x in Q[x]. x :: Qx -- | Take a list and construct a polynomial by removing all zeroes in the -- end. toUPoly :: (CommutativeRing r, Eq r) => [r] -> UPoly r x -- | Take an element of the ring and the degree of the desired monomial, -- for example: monomial 3 7 = 3x^7 monomial :: (CommutativeRing r) => r -> Integer -> UPoly r x -- | Compute the leading term of a polynomial. lt :: (CommutativeRing r) => UPoly r x -> r -- | Formal derivative of polynomials in k[x]. deriv :: (CommutativeRing r) => UPoly r x -> UPoly r x -- | Square free decomposition of a polynomial. sqfr :: (Num k, Field k) => UPoly k x -> UPoly k x -- | Distinct power factorization, aka square free decomposition sqfrDec :: (Num k, Field k) => UPoly k x -> [UPoly k x] instance (Eq r) => Eq (UPoly r x) instance (Ord r) => Ord (UPoly r x) instance (Field k, Eq k) => EuclideanDomain (UPoly k x) instance (CommutativeRing r, Eq r) => IntegralDomain (UPoly r x) instance (CommutativeRing r, Eq r) => CommutativeRing (UPoly r x) instance (Show r, Field r, Num r, Show x) => Num (UPoly r x) instance (CommutativeRing r, Eq r) => Ring (UPoly r x) instance (CommutativeRing r, Eq r, Arbitrary r) => Arbitrary (UPoly r x) instance (CommutativeRing r, Eq r, Show r, Show x) => Show (UPoly r x)