constructive-algebra 0.1.1 → 0.1.2

raw patch · 8 files changed

+457/−32 lines, 8 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.hs +10/−0
• constructive-algebra.cabal +6/−3
• examples/Z_Examples.hs +17/−0
• src/Algebra/Matrix.hs +156/−0
• src/Algebra/PLM.hs +49/−0
• src/Algebra/Structures/BezoutDomain.hs +18/−28
• src/Algebra/Structures/Coherent.hs +175/−0
• src/Algebra/Z.hs +26/−1

@@ -48,12 +48,22 @@ -- Field of fractions of a GCD domain. import Algebra.Structures.FieldOfFractions +-- Coherent rings. That is rings in which it is possible to solve homogenous+-- linear equations. +import Algebra.Structures.Coherent + ------------------------------------------------------------------------------- -- Special constructions.  -- Finitely generated ideals over commutative rings.  import Algebra.Ideal++-- Simple matrix library+import Algebra.Matrix++-- Principle localization matrices+import Algebra.PLM   -------------------------------------------------------------------------------

@@ -7,7 +7,7 @@ -- The package version. See the Haskell package versioning policy -- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for -- standards guiding when and how versions should be incremented.-Version:             0.1.1+Version:             0.1.2  Synopsis:            A library of constructive algebra. Description:         @@ -16,7 +16,7 @@         .         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 get +        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).@@ -56,8 +56,11 @@                        Algebra.Structures.EuclideanDomain,                        Algebra.Structures.StronglyDiscrete,                        Algebra.Structures.FieldOfFractions,-                       Algebra.Structures.GCDDomain,         +                       Algebra.Structures.GCDDomain, +                       Algebra.Structures.Coherent,                        Algebra.Ideal,+                       Algebra.Matrix,+                       Algebra.PLM,                        Algebra.Z,                        Algebra.Q                        

@@ -1,10 +1,13 @@+{-# LANGUAGE TypeSynonymInstances #-} module Z_Examples where  import Test.QuickCheck  import Algebra.Structures.BezoutDomain import Algebra.Structures.StronglyDiscrete+import Algebra.Structures.Coherent import Algebra.Ideal+import Algebra.Matrix import Algebra.Z  @@ -25,3 +28,17 @@  ex5 :: Maybe [Z] ex5 = member 2 ex3+++-------------------------------------------------------------------------------+-- Solving equations++ex6 :: Matrix Z+ex6 = solve (Vec [1,2,3])+++-------------------------------------------------------------------------------+-- PLM++ex7 :: Matrix Z+ex7 = computePLM_B (Id [2,3,4])

@@ -0,0 +1,156 @@+-- | A small simple matrix library.+module Algebra.Matrix+  ( Vector(Vec)+  , unVec, lengthVec+  , Matrix(M)+  , matrix+  , matrixToVector, vectorToMatrix, unMVec, unM +  , identity, mulM, addM, transpose, isSquareMatrix, dimension+  ) where++import qualified Data.List as L+import Control.Monad (liftM)+import Test.QuickCheck++import Algebra.Structures.IntegralDomain+++-------------------------------------------------------------------------------+-- | Row vectors++data Vector r = Vec [r] deriving (Eq)++instance Show r => Show (Vector r) where+  show (Vec vs) = show vs++instance (Ring r, Arbitrary r, Eq r) => Arbitrary (Vector r) where+  arbitrary = do n <- choose (1,10) :: Gen Int+                 liftM Vec $ gen n+    where+    gen 0 = return []+    gen n = do x <- arbitrary+               xs <- gen (n-1)+               if x == zero then return (one:xs) else return (x:xs)++{-+instance Ring r => Ring (Vector r) where+  (Vec xs) <+> (Vec ys) | length xs == length ys = Vec (zipWith (<+>) xs ys)+                        | otherwise = error "Bad dimensions in vector addition"+  (Vec xs) <*> (Vec ys) | length xs == length ys = Vec (zipWith (<*>) xs ys)+                        | otherwise = error "Bad dimensions in vector multiplication"+  -- In order to do these we need to know the length of the vector in advance...+  -- Give me dependent types!+  one  = ?+  zero = ?+-}++unVec :: Vector r -> [r]+unVec (Vec vs) = vs++lengthVec :: Vector r -> Int+lengthVec = length . unVec+++-------------------------------------------------------------------------------+-- | Matrices++data Matrix r = M [Vector r]+  deriving (Eq)++instance Show r => Show (Matrix r) where+  show (M xs) = case unlines $ map show xs of+    [] -> "[]"+    xs -> init xs++instance (Eq r, Arbitrary r, Ring r) => Arbitrary (Matrix r) where+  arbitrary = do n <- choose (1,10) :: Gen Int+                 m <- choose (1,10) :: Gen Int+                 xs <- sequence [ liftM Vec (gen n) | _ <- [1..m]]+                 return (M xs)+    where+    gen 0 = return []+    gen n = do x <- arbitrary+               xs <- gen (n-1)+               if x == zero then return (one:xs) else return (x:xs)+++-- | Construct a mxn matrix.+matrix :: [[r]] -> Matrix r+matrix xs = +  let m = fromIntegral $ length xs+      n = fromIntegral $ length (head xs)+  in if length (filter (\x -> fromIntegral (length x) == n) xs) == length xs +        then M (map Vec xs)+        else error "matrix: Bad dimensions"++unM :: Matrix r -> [Vector r]+unM (M xs) = xs++unMVec :: Matrix r -> [[r]]+unMVec = map unVec . unM++vectorToMatrix :: Vector r -> Matrix r+vectorToMatrix = matrix . (:[]) . unVec++matrixToVector :: Matrix r -> Vector r+matrixToVector m | fst (dimension m) == 1 = head (unM m)+                 | otherwise              = error "matrixToVector: Bad dimension"++-- | Compute the dimension of a matrix.+dimension :: Matrix r -> (Int, Int)+dimension (M xs) | null xs   = (0,0)+                 | otherwise = (length xs, length (unVec (head xs)))++isSquareMatrix :: Matrix r -> Bool+isSquareMatrix (M xs) = all (== length xs) (map lengthVec xs)++-- | Transpose a matrix.+transpose :: Matrix r -> Matrix r+transpose (M xs) = matrix (L.transpose (map unVec xs))++-- | Matrix addition.+addM :: Ring r => Matrix r -> Matrix r -> Matrix r+addM (M xs) (M ys) | dimension (M xs) == dimension (M ys) = m+                   | otherwise = error "Bad dimensions in matrix addition"+  where+  m = matrix (zipWith (zipWith (<+>)) (map unVec xs) (map unVec ys))++-- | Matrix multiplication.+mulM :: Ring r => Matrix r -> Matrix r -> Matrix r+mulM (M xs) (M ys) +  | snd (dimension (M xs)) == fst (dimension (M ys)) = m+  | otherwise = error "Bad dimensions in matrix multiplication"+    where+    m = matrix [ [ foldr1 (<+>) (zipWith (<*>) x y) +                 | y <- L.transpose (map unVec ys) ]+               | x <- map unVec xs ]++++{-+-- In order to do this the size of the matrix need to be encoded in the type+-- There is also a problem with the fact that it is not possible to add or +-- multiply matrices with bad dimensions, so the generation of matrices has to be better...+instance Ring r => Ring (Matrix r) where+  (<+>) = add+  (<*>) = mul+  neg (M xs d) = M [ map neg x | x <- xs ] d+  zero  = undefined +-}++-- | Construct a nxn identity matrix.+identity :: IntegralDomain r => Int -> Matrix r+identity n = matrix (xs 0)+  where+  xs x | x == n    = [] +       | otherwise = (replicate x zero ++ [one] ++ +                      replicate (n-x-1) zero) : xs (x+1)++-- Specification of identity.+propLeftIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool+propLeftIdentity a = a == identity n `mulM` a+  where n = fst (dimension a)++propRightIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool+propRightIdentity a = a == a `mulM` identity m+  where m = snd (dimension a)

@@ -0,0 +1,49 @@+-- | Specification of principal localization matrices used in the coherence +-- proof of Prufer domains. +module Algebra.PLM +  ( propPLM+  , computePLM_B+  ) where++import Algebra.Structures.CommutativeRing+import Algebra.Structures.BezoutDomain+import Algebra.Ideal+import Algebra.Matrix+++-------------------------------------------------------------------------------+{- | A principal localization matrix for an ideal (x1,...,xn) is a matrix such +that:++ - The sum of the diagonal should equal 1.++ - For all i, j, l in {1..n}: a_lj * x_i = a_li * x_j++-}+propPLM :: (CommutativeRing a, Eq a) => Ideal a -> Matrix a -> Bool+propPLM (Id xs) (M vs) +  | isSquareMatrix (M vs) = +    let as      = map unVec vs+        sumDiag = sumRing [ ai !! i | (ai,i) <- zip as [0..]]+        n       = length as - 1+        ijl     = and [ as !! l !! j <*> xs !! i == +                        as !! l !! i <*> xs !! j+                      | i <- [0..n]+                      , j <- [0..n]+                      , l <- [0..n]+                      ]+    in one == sumDiag && ijl+  | otherwise = error "isPLM: Not square matrix"++-- Maybe it would be nice to add some of the properties in Proposition 2.6 in:+-- http://hlombardi.free.fr/liens/salouThesis.pdf+++-------------------------------------------------------------------------------+-- | Principal localization matrices for ideals are computable in Bezout domains.++computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a+computePLM_B (Id xs) = +  let (Id [g],us,ys) = toPrincipal (Id xs)+      n              = length xs - 1+  in M [ Vec [ us !! i <*> ys !! j | j <- [0..n] ] | i <- [0..n] ]

@@ -7,17 +7,17 @@   ( BezoutDomain(..)   , propBezoutDomain   , intersectionB, intersectionBWitness+  , solveB   ) where  import Test.QuickCheck   import Algebra.Structures.IntegralDomain--- import Algebra.Structures.Coherent+import Algebra.Structures.Coherent import Algebra.Structures.EuclideanDomain -- import Algebra.Structures.PruferDomain import Algebra.Structures.StronglyDiscrete--- import Algebra.PLM--- import Algebra.Matrix+import Algebra.Matrix import Algebra.Ideal  @@ -95,15 +95,16 @@   as = map (v2 <*>) us1   bs = map (v1 <*>) us2   -  -- Handle the zeroes specially. If the first element in xs is a zero-  -- then the witness should be zero otherwise use the computed witness. -  handleZero xs [] -    | all (==zero) xs = xs-    | otherwise       = error "intersectionB: This should be impossible"-  handleZero (x:xs) (a:as) -    | x == zero = zero : handleZero xs (a:as)-    | otherwise = a    : handleZero xs as-  handleZero [] _  = error "intersectionB: This should be impossible"+-- Handle the zeroes specially. If the first element in xs is a zero+-- then the witness should be zero otherwise use the computed witness. +handleZero :: (Ring a, Eq a) => [a] -> [a] -> [a]+handleZero xs [] +  | all (==zero) xs = xs+  | otherwise       = error "intersectionB: This should be impossible"+handleZero (x:xs) (a:as) +  | x == zero = zero : handleZero xs (a:as)+  | otherwise = a    : handleZero xs as+handleZero [] _  = error "intersectionB: This should be impossible"   -- | Intersection without witness.@@ -112,26 +113,15 @@   ---------------------------------------------------------------------------------- Coherence--- --- solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a--- solveB x = solveWithIntersection x intersectionB+-- | Coherence of Bezout domains.+solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a+solveB x = solveWithIntersection x intersectionBWitness  -- instance (BezoutDomain r, Eq r) => Coherent r where --   solve x = solveWithIntersection x intersectionB   ---------------------------------------------------------------------------------- Principal localization matrix------ computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a--- computePLM_B (Id xs) = ---  let (Id [g],us,ys) = toPrincipal (Id xs)---      n              = length xs - 1---  in M [ Vec [ us !! i <*> ys !! j | j <- [0..n] ] | i <- [0..n] ]---------------------------------------------------------------------------------- -- | Strongly discreteness for Bezout domains --  -- Given x, compute as such that x = sum (a_i * x_i)@@ -145,11 +135,11 @@     -- (<g>, as, bs)   = <x1,...,xn>     -- sum (a_i * x_i) = g     -- x_i             = b_i * g-    (Id [g], as, bs) = toPrincipal (Id xs)+    (Id [g], as, bs) = toPrincipal (Id (filter (/= zero) xs))     (Id [a], _,[q1,q2]) = toPrincipal (Id [x,g])          -- x = qg = q (sum (ai * xi)) = sum (q * ai * xi)-    witness = map (q1 <*>) as+    witness = handleZero xs (map (q1 <*>) as)  -------------------------------------------------------------------------------- -- | Bezout domain -> Prüfer domain

@@ -0,0 +1,175 @@+-- | 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+  ( Coherent(solve)+  , propCoherent+  , solveMxN, propSolveMxN+  , solveWithIntersection+  , solveGeneralEquation, propSolveGeneralEquation+  , solveGeneral, propSolveGeneral+  ) where++import Test.QuickCheck++import Algebra.Structures.IntegralDomain+import Algebra.Structures.StronglyDiscrete+import Algebra.Matrix+import Algebra.Ideal+++-------------------------------------------------------------------------------+-- | 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 where+  solve :: Vector a -> Matrix a++isSolution :: (CommutativeRing a, Eq a) => Matrix a -> Matrix a -> Bool+isSolution m sol = all (==zero) (concat (unMVec (m `mulM` sol)))++propCoherent :: (Coherent a, Eq a) => Vector a -> Bool+propCoherent m = isSolution (vectorToMatrix m) (solve m)++-------------------------------------------------------------------------------+-- | Solves a system of equations.+solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a+solveMxN (M (l:ls)) = solveMxN' (solve l) ls+  where+  -- Inductively solve all subsystems. If the computed solution is in fact a +  -- solution to the next set of equations then don't do anything. +  -- This solves the problems with having many identical rows in the system,+  -- like [[1,1],[1,1]].+  solveMxN' :: (Coherent a, Eq a) => Matrix a -> [Vector a] -> Matrix a+  solveMxN' m []      = m+  solveMxN' m1 (x:xs) = if isSolution (vectorToMatrix x) m1 +                           then solveMxN' m1 xs +                           else solveMxN' (m1 `mulM` m2) xs+    where m2 = solve (matrixToVector (mulM (vectorToMatrix x) m1))+++-- | Test that the solution of an MxN system is in fact a solution of the system+propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool+propSolveMxN m = isSolution m (solveMxN m)+++-------------------------------------------------------------------------------+-- | 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+solveWithIntersection (Vec xs) int = transpose $ matrix $ solveInt xs +  where+  solveInt []     = error "solveInt: Can't solve an empty system"+  solveInt [x]    = [[zero]] -- Base case, could be [x,y] also...+                             -- That wouldn't give the trivial solution... +--  solveInt [x,y]  | x == zero || y == zero = [[zero,zero]]+--                  | otherwise = +--    let (Id ts,us,vs) = (Id [x]) `int` (Id [neg y])+--    in [ u ++ v | (u,v) <- zip us vs ]+  solveInt (x:xs)+    | x == zero             = map (zero:) $ solveInt xs +    | isSameIdeal int as bs = s ++ m'+    | otherwise             = error "solveInt: This does not compute the intersection"+      where+      as            = Id [x]+      bs            = Id (map neg xs)++      -- Compute the intersection of <x1> and <-x2,...,-xn>+      (Id ts,us,vs) = as `int` bs+      s             = [ u ++ v | (u,v) <- zip us vs ]+      +      -- Solve <0,x2,...,xn> recursively+      m             = solveInt xs+      m'            = map (zero:) m+++-------------------------------------------------------------------------------+-- | 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)+solveGeneralEquation v@(Vec xs) b = +  let sol = solve v+  in case b `member` (Id xs) of+    Just as -> Just $ transpose (M (replicate (length (head (unMVec sol))) (Vec as)))+                      `addM` sol+    Nothing -> Nothing+++propSolveGeneralEquation :: (Coherent a, StronglyDiscrete a, Eq a) +                         => Vector a +                         -> a +                         -> Bool+propSolveGeneralEquation v b = case solveGeneralEquation v b of+  Just sol -> all (==b) $ concat $ unMVec $ vectorToMatrix v `mulM` sol+  Nothing  -> True+++isSolutionB v sol b = all (==b) $ concat $ unMVec $ vectorToMatrix v `mulM` sol+++-- | 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   -- M+             -> Vector a   -- B+             -> Maybe (Matrix a, Matrix a)  -- (L,X0)+solveGeneral (M (l:ls)) (Vec (a:as)) = +  case solveGeneral' (solveGeneralEquation l a) ls as [(l,a)] of+    Just x0 -> Just (solveMxN (M (l:ls)), x0)+    Nothing -> Nothing+  where+  -- Compute a new solution inductively and check that the new solution +  -- satisfies all the previous equations.+  solveGeneral' Nothing _ _ _              = Nothing+  solveGeneral' (Just m) [] [] old         = Just m +  solveGeneral' (Just m) (l:ls) (a:as) old = +    if isSolutionB l m a +       then solveGeneral' (Just m) ls as old+       else case solveGeneralEquation (matrixToVector (vectorToMatrix l `mulM` m)) a of+         Just m' -> let m'' = m `mulM` m'+                    in if all (\(x,y) -> isSolutionB x m'' y) old+                          then solveGeneral' (Just m'') ls as ((l,a):old)+                          else Nothing+         Nothing -> Nothing+  solveGeneral' _ _ _ _ = error "solveGeneral: Bad input"      ++-- It would be great to only generate solvable systems...+-- propSolveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Property +propSolveGeneral m b = length (unM m) == length (unVec b) ==> case solveGeneral m b of+  Just (l,x) -> all (==b) (unM (transpose (m `mulM` x))) &&+                isSolution m l+  Nothing -> True

@@ -10,7 +10,10 @@ import Algebra.Structures.EuclideanDomain import Algebra.Structures.BezoutDomain import Algebra.Structures.StronglyDiscrete+import Algebra.Structures.Coherent import Algebra.Ideal+import Algebra.Matrix+import Algebra.PLM   -- | Type synonym for integers.@@ -34,12 +37,34 @@   d = abs   quotientRemainder = quotRem - propEuclideanDomainZ :: Z -> Z -> Z -> Property propEuclideanDomainZ = propEuclideanDomain +-- Euclidean domain -> Bezout domain propBezoutDomainZ :: Ideal Z -> Z -> Z -> Z -> Property propBezoutDomainZ = propBezoutDomain +-- Bezout domain -> Strongly discrete propStronglyDiscreteZ :: Z -> Ideal Z -> Bool propStronglyDiscreteZ = propStronglyDiscrete++-- Bezout domain -> Coherent+instance Coherent Z where+  solve = solveB++propCoherentZ :: Vector Z -> Bool+propCoherentZ = propCoherent++propSolveMxNZ :: Matrix Z -> Bool+propSolveMxNZ = propSolveMxN++propSolveGeneralEquationZ :: Vector Z -> Z -> Bool+propSolveGeneralEquationZ = propSolveGeneralEquation++-- Not working perfectly...+propSolveGeneralZ :: Matrix Z -> Vector Z -> Property+propSolveGeneralZ = propSolveGeneral++-- PLM+propPLMZ :: Ideal Z -> Bool+propPLMZ id = propPLM id (computePLM_B id)