constructive-algebra 0.1 → 0.1.1

raw patch · 15 files changed

+632/−19 lines, 15 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.hs +70/−0
• constructive-algebra.cabal +19/−5
• examples/Z_Examples.hs +27/−0
• src/Algebra/Ideal.hs +9/−4
• src/Algebra/Q.hs +37/−0
• src/Algebra/Structures/BezoutDomain.hs +200/−0
• src/Algebra/Structures/CommutativeRing.hs +1/−1
• src/Algebra/Structures/EuclideanDomain.hs +105/−0
• src/Algebra/Structures/Field.hs +1/−1
• src/Algebra/Structures/FieldOfFractions.hs +88/−0
• src/Algebra/Structures/GCDDomain.hs +50/−0
• src/Algebra/Structures/IntegralDomain.hs +3/−3
• src/Algebra/Structures/Ring.hs +2/−3
• src/Algebra/Structures/StronglyDiscrete.hs +1/−1
• src/Algebra/Z.hs +19/−1

@@ -0,0 +1,70 @@+-------------------------------------------------------------------------------+-- | Constructive Algebra Library +-- +-- Anders Mortberg    <mortberg@student.chalmers.se>+-- Bassel Mannaa      <mannaa@student.chalmers.se>+--+-- Abstract:+-- This is a library written as part of our master theses. It focuses mainly+-- on the theory of commutative rings from a constructive point of view. +--+-------------------------------------------------------------------------------++module README where+++--------------------------------------------------------------------------------+-- Structures++-- Rings with basic operations. +import Algebra.Structures.Ring++-- Commutative rings.+import Algebra.Structures.CommutativeRing++-- Integral domains.+import Algebra.Structures.IntegralDomain++-- Fields.+import Algebra.Structures.Field++-- Strongly discrete rings - Rings with decidable ideal membership.+import Algebra.Structures.StronglyDiscrete++-- EuclideanDomains - Integral domains with decidable division and and Euclidean+-- function. Contains lots of functions that are possible at the level of +-- Euclidean domain like the Euclidean algorithm and extended Euclidean +-- algorithm.+import Algebra.Structures.EuclideanDomain++-- Bezout domains - Non-Noetherian analogues of principal ideal domains. All +-- finitely generated ideals are principal.+import Algebra.Structures.BezoutDomain++-- GCD domains - Non-Noetherian analogues of unique factorization domains. +-- All pairs of nonzero elements have a greatest common divisor.+import Algebra.Structures.GCDDomain++-- Field of fractions of a GCD domain.+import Algebra.Structures.FieldOfFractions+++-------------------------------------------------------------------------------+-- Special constructions.++-- Finitely generated ideals over commutative rings. +import Algebra.Ideal+++-------------------------------------------------------------------------------+-- Instances.++-- The integers.+import Algebra.Z++-- The rational numbers as the field of fractions of Z. +import Algebra.Q+++-------------------------------------------------------------------------------+-- The end.

@@ -7,10 +7,19 @@ -- 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+Version:             0.1.1  Synopsis:            A library of constructive algebra.-Description:         A library of constructive algebra.+Description:         +        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 get +        Bezout domains which are integral domains in which all finitely +        generated ideals are principal (and not necessarily that all ideals are+        principal).  License:             BSD3 License-file:        LICENSE@@ -31,7 +40,7 @@  -- Extra files to be distributed with the package, such as examples or -- a README.--- Extra-source-files:  +Extra-source-files:  README.hs, examples/Z_Examples.hs  -- Constraint on the version of Cabal needed to build this package. Cabal-version:       >=1.2@@ -43,11 +52,16 @@                        Algebra.Structures.CommutativeRing,                        Algebra.Structures.IntegralDomain,                         Algebra.Structures.Field,+                       Algebra.Structures.BezoutDomain,+                       Algebra.Structures.EuclideanDomain,                        Algebra.Structures.StronglyDiscrete,+                       Algebra.Structures.FieldOfFractions,+                       Algebra.Structures.GCDDomain,                                 Algebra.Ideal,-                       Algebra.Z+                       Algebra.Z,+                       Algebra.Q+                        -     -- Packages needed in order to build this package.   Build-depends:       base >= 3 && <= 4, QuickCheck >= 2    

@@ -0,0 +1,27 @@+module Z_Examples where++import Test.QuickCheck++import Algebra.Structures.BezoutDomain+import Algebra.Structures.StronglyDiscrete+import Algebra.Ideal+import Algebra.Z+++-------------------------------------------------------------------------------+-- Bezout domain examples++ex1, ex2 :: (Ideal Z, [Z], [Z])+ex1 = toPrincipal (Id [4,6])+ex2 = toPrincipal (Id [2,3])++ex3, ex4 :: Ideal Z+ex3 = Id [2] `intersectionB` Id [3]+ex4 = Id [2,3] `intersectionB` Id [3]+++-------------------------------------------------------------------------------+-- Strong discreteness++ex5 :: Maybe [Z]+ex5 = member 2 ex3

@@ -1,7 +1,9 @@ -- | Finitely generated ideals in commutative rings. module Algebra.Ideal   ( Ideal(Id)-  , zeroIdeal, isPrincipal, eval, addId, mulId +  , zeroIdeal, isPrincipal, fromId+  , eval, addId, mulId+  , isSameIdeal, zeroIdealWitnesses   ) where  import Data.List (intersperse,nub)@@ -47,15 +49,18 @@ mulId (Id xs) (Id ys) = if zs == [] then zeroIdeal else Id zs   where zs = nub [ f <*> g | f <- xs, g <- ys, f <*> g /= zero ] -{-| Test if an operations compute the correct ideal. +{- | Test if an operations compute the correct ideal.  The operation should give a witness that the comuted ideal contains the same elements. -I `op` J = K-[ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]+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) 

@@ -0,0 +1,37 @@+{-# LANGUAGE TypeSynonymInstances #-}+-- | Representation of rational numbers as the field of fractions of Z.+module Algebra.Q +  ( Q+  , toQ, toZ+  ) where++import Test.QuickCheck+-- import qualified Math.Algebra.Field.Base as A (Q(..)) +-- import Data.Ratio ++import Algebra.Structures.Field+import Algebra.Structures.FieldOfFractions+import Algebra.Z++-------------------------------------------------------------------------------+-- | Q is the field of fractions of Z.++type Q = FieldOfFractions Z++instance Num Q where+  (+)              = (<+>)+  (*)              = (<*>)+  abs (F (a,b))    = F (abs a, b) +  signum (F (a,_)) = F (signum a,one)+  fromInteger      = toQ++instance Fractional Q where+  (/) = (</>)+  fromRational = undefined+--   fromRational (a :% b) = reduce $ F (a,b)++toQ :: Z -> Q+toQ = toFieldOfFractions++toZ :: Q -> Z+toZ = fromFieldOfFractions   

@@ -0,0 +1,200 @@+-- | Representation of Bezout domains. That is non-Noetherian analogues of +-- principal ideal domains. This means that all finitely generated ideals are+-- principal.+--+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}+module Algebra.Structures.BezoutDomain+  ( BezoutDomain(..)+  , propBezoutDomain+  , intersectionB, intersectionBWitness+  ) where++import Test.QuickCheck ++import Algebra.Structures.IntegralDomain+-- import Algebra.Structures.Coherent+import Algebra.Structures.EuclideanDomain+-- import Algebra.Structures.PruferDomain+import Algebra.Structures.StronglyDiscrete+-- import Algebra.PLM+-- import Algebra.Matrix+import Algebra.Ideal+++-------------------------------------------------------------------------------+-- | 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 where+  toPrincipal :: Ideal a -> (Ideal a,[a],[a])++propToPrincipal :: (BezoutDomain a, Eq a) => Ideal a -> Bool+propToPrincipal = isPrincipal . (\(a,_,_) -> a) . toPrincipal++propIsSameIdeal :: (BezoutDomain a, Eq a) => Ideal a -> Bool+propIsSameIdeal (Id as) =+  let (Id [a], us, vs) = toPrincipal (Id as) +  in a == foldr1 (<+>) (zipWith (<*>) as us) +  && and [ ai == a <*> vi | (ai,vi) <- zip as vs ]+  && length us == l_as && length vs == l_as+  where l_as = length as++propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property+propBezoutDomain id@(Id xs) a b c = zero `notElem` xs ==> +  if propToPrincipal id+     then if propIsSameIdeal id+             then propIntegralDomain a b c +             else whenFail (print "propIsSameIdeal") False+     else whenFail (print "propToPrincipal") False+++-------------------------------------------------------------------------------+-- Euclidean domain -> Bezout domain++instance (EuclideanDomain a, Eq a) => BezoutDomain a where+  toPrincipal (Id [x]) = (Id [x], [one], [one])+  toPrincipal (Id xs)  = (Id [a], as, [ quotient ai a | ai <- xs ])+    where+    a  = genEuclidAlg xs+    as = genExtendedEuclidAlg xs+++-------------------------------------------------------------------------------+-- | 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]])+intersectionBWitness (Id xs) (Id ys) +  | xs' == [] = zeroIdealWitnesses xs ys+  | ys' == [] = zeroIdealWitnesses xs ys+  | otherwise = (Id [l], [handleZero xs as], [handleZero ys bs])+  where+  xs'            = filter (/= zero) xs+  ys'            = filter (/= zero) ys++  (Id [a],us1,vs1) = toPrincipal (Id xs') +  (Id [b],us2,vs2) = toPrincipal (Id ys')++  (Id [g],[u1,u2],[v1,v2]) = toPrincipal (Id [a,b])++  l  = g <*> v1 <*> v2+  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"+++-- | Intersection without witness.+intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a+intersectionB a b = (\(x,_,_) -> x) $ intersectionBWitness a b+++-------------------------------------------------------------------------------+-- Coherence+-- +-- solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a+-- solveB x = solveWithIntersection x intersectionB++-- 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)+--+instance (BezoutDomain a, Eq a) => StronglyDiscrete a where+  member x (Id xs) | x == zero = Just (replicate (length xs) zero)+                   | otherwise = if a == g +                                    then Just witness +                                    else Nothing+    where+    -- (<g>, as, bs)   = <x1,...,xn>+    -- sum (a_i * x_i) = g+    -- x_i             = b_i * g+    (Id [g], as, bs) = toPrincipal (Id xs)+    (Id [a], _,[q1,q2]) = toPrincipal (Id [x,g])+    +    -- x = qg = q (sum (ai * xi)) = sum (q * ai * xi)+    witness = map (q1 <*>) as++--------------------------------------------------------------------------------+-- | Bezout domain -> Prüfer domain+--+{-+Prufer: forall a b exists u v w t.  u+t = 1 &  ua = vb & wa = tb++We consider only domain.+We assume we have the Bezout condition: given a, b we can find g,a1,b1,c,d s.t.++a = g a1+b = g b1+1 = c a1 + d b1++We try then ++u = d b1+t = c a1++We should find v such that+a d b1 = b v+this simplifies to +g a1 d b1 = g b1 v+and we can take +v = a1 d+Similarly we can take +w = b1 c++We have shown that Bezout domain -> Prufer domain.+instance (BezoutDomain a, Eq a) => PruferDomain a where+  calcUVW a b | a == zero = (one,zero,zero)+              | b == zero = (zero,zero,zero)+              | otherwise = fromUVWTtoUVW (u,v,w,t)+    where+    -- Compute g, a1 and b1 such that:+    -- a = g*a1+    -- b = g*b1+    (g,[_,_],[a1,b1])  = toPrincipal (Id [a,b])+    +    -- Compute c and d such that:+    -- 1 = a1*c + a2*d+    (_,[c,d],_) = toPrincipal (Id [a1,b1])++    u = d <*> b1+    t = c <*> a1+    v = d <*> a1+    w = c <*> b1+-}

@@ -10,7 +10,7 @@   ---------------------------------------------------------------------------------- | Definition of commutative rings+-- | Definition of commutative rings.  class Ring a => CommutativeRing a 

@@ -0,0 +1,105 @@+-- | Representation of Euclidean domains. That is integral domains with an +-- Euclidean functions and decidable division.+--+module Algebra.Structures.EuclideanDomain +  ( EuclideanDomain(..)+  , propEuclideanDomain+  , modulo, quotient, divides +  , euclidAlg, genEuclidAlg+  , lcmE, genLcmE+  , extendedEuclidAlg, genExtendedEuclidAlg+  ) where++import Test.QuickCheck++import Algebra.Structures.IntegralDomain+-- import Algebra.Structures.Coherent+import Algebra.Ideal+++-------------------------------------------------------------------------------+-- | 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 where+  d :: a -> Integer+  quotientRemainder :: a -> a -> (a,a)++-- Check both that |a| <= |ab| and |a| >= 0 for all a,b+propD :: (EuclideanDomain a, Eq a) => a -> a -> Bool+propD a b = +  a == zero || b == zero || (d a <= d (a <*> b) && d a >= 0 && d b >= 0)++propQuotRem :: (EuclideanDomain a, Eq a) => a -> a -> Bool+propQuotRem a b = b == zero || (a == b <*> q <+> r && (r == zero || d r < d b))+  where (q,r) = quotientRemainder a b ++propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property+propEuclideanDomain a b c =+  if propD a b +     then if propQuotRem a b+             then propIntegralDomain a b c+             else whenFail (print "propQuotRem") False+     else whenFail (print "propD") False+++-------------------------------------------------------------------------------+-- Operations++modulo :: EuclideanDomain a => a -> a -> a+modulo a b = snd (quotientRemainder a b)++quotient :: EuclideanDomain a => a -> a -> a+quotient a b = fst (quotientRemainder a b)++divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool+divides a b = modulo b a == zero++-- | The Euclidean algorithm for calculating the GCD of a and b.+euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a+euclidAlg a b | a == zero && b == zero = error "GCD of 0 and 0 is undefined"+              | b == zero = a+              | otherwise = euclidAlg b (a `modulo` b)++-- | Generalized Euclidean algorithm to compute GCD of a list of elements.+genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a+genEuclidAlg = foldl euclidAlg zero++-- | Lowest common multiple, (a*b)/gcd(a,b).+lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a+lcmE a b = quotient (a <*> b) (euclidAlg a b)++-- | Generalized lowest common multiple to compute lcm of a list of elements.+genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a+genLcmE xs = quotient (foldr1 (<*>) xs) (genEuclidAlg xs)++-- | The extended Euclidean algorithm. +-- +-- Computes x and y in ax + by = gcd(a,b).+-- +extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a,a)+extendedEuclidAlg a b | modulo a b == zero = (zero,one)+                      | otherwise          = (y, x <-> y <*> (a `quotient` b))+  where (x,y) = extendedEuclidAlg b (a `modulo` b)++-- Specification of extended Euclidean algorithm.+propExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> Property+propExtendedEuclidAlg a b = a /= zero && b /= zero ==> +  let (x,y) = extendedEuclidAlg a b in a <*> x <+> b <*> y == euclidAlg a b++-- | 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]+genExtendedEuclidAlg [x,y] = let (a,b) = extendedEuclidAlg x y in [a,b]+genExtendedEuclidAlg xs    =+  let (x,y) = extendedEuclidAlg (genEuclidAlg (init xs)) (last xs)+  in map (x<*>) (genExtendedEuclidAlg (init xs)) ++ [y]++-- Specification of generalized extended Euclidean algorithm. +propGenExtEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> Property+propGenExtEuclidAlg xs = all (/= zero) xs && length xs >= 2 ==> +  foldr (<+>) zero (zipWith (<*>) (genExtendedEuclidAlg xs) xs) == genEuclidAlg xs

@@ -14,7 +14,7 @@ infixl 7 </>  ---------------------------------------------------------------------------------- | Definition of fields+-- | Definition of fields.  class IntegralDomain a => Field a where   inv :: a -> a

@@ -0,0 +1,88 @@+-- | 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+  ( FieldOfFractions(..)+  , toFieldOfFractions, fromFieldOfFractions+  , reduce+  ) where++import Test.QuickCheck++import Algebra.Structures.Field+import Algebra.Structures.GCDDomain+++-------------------------------------------------------------------------------+-- | Field of fractions++newtype GCDDomain a => FieldOfFractions a = F (a,a)+++--------------------------------------------------------------------------------+-- Instances++instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a) where+  show (F (a,b)) | b == one  = show a+                 | otherwise = case show b of+                    ('-':xs) -> "-" ++ show a ++ "/" ++ xs+                    xs -> show a ++ "/" ++ xs++instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a) where+  arbitrary = do+    a <- arbitrary+    b <- arbitrary+    if b == zero +       then return $ F (a,one)+       else return $ F (a,b)++instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a) where+  f == g = a <*> d == b <*> c+    where+    F (a,b) = reduce f+    F (c,d) = reduce g++instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a) where+  (F (a,b)) <+> (F (c,d)) = reduce (F (a <*> d <+> c <*> b,b <*> d))+  (F (a,b)) <*> (F (c,d)) = reduce (F (a <*> c,b <*> d))+  neg (F (a,b))           = reduce (F (neg a,b))+  one                     = toFieldOfFractions one+  zero                    = toFieldOfFractions zero++instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)+instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)++instance (GCDDomain a, Eq a) => Field (FieldOfFractions a) where+  inv (F (a,b)) | b /= zero && a /= zero = reduce $ F (b,a)+                | otherwise = error "FieldOfFraction: Division by zero"+++--------------------------------------------------------------------------------+-- Operations++-- | Embed a value in the field of fractions.+toFieldOfFractions :: GCDDomain a => a -> FieldOfFractions a+toFieldOfFractions a = F (a,one)++-- | 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+fromFieldOfFractions (F (a,b)) +  | b == one  = a+  | otherwise = error "FieldOfFractions: Can't extract value"++-- | Reduce an element.+reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a+reduce (F (a,b)) | b == zero = error "FieldOfFractions: Division by zero"+                 | a == zero = F (zero,one)+                 | otherwise = if g == one+                                  then F (a,b)+                                  else F (x,y)+  where+  (g,x,y) = gcd' a b++-- Specification of reduce.+propReduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> Property+propReduce f@(F (a,b)) = a /= zero && b /= zero ==> g == one+  where+  F (c,d) = reduce f+  (g,_,_) = gcd' c d

@@ -0,0 +1,50 @@+-- | 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.+--+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}+module Algebra.Structures.GCDDomain +  ( GCDDomain(gcd')+  , propGCDDomain+  ) where++import Test.QuickCheck++import Algebra.Structures.IntegralDomain+import Algebra.Structures.BezoutDomain+import Algebra.Ideal+++-------------------------------------------------------------------------------+-- | GCD domains++class IntegralDomain a => GCDDomain a where+  -- | Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and+  --   a = gx+  --   b = gy+  -- and a, b /= 0+  gcd' :: a -> a -> (a,a,a)+++propGCD :: (GCDDomain a, Eq a) => a -> a -> Bool+propGCD a b = a == zero || b == zero || a == g <*> x && b == g <*> y+  where+  (g,x,y) = gcd' a b+++-- | 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+propGCDDomain a b c = if propGCD a b +                         then propIntegralDomain a b c+                         else whenFail (print "propGCD") False++-- This can be used to compute gcd of a list of non-zero elements+-- genGCD :: ?+-- genGCD = ?++instance BezoutDomain a => GCDDomain a where+  gcd' a b = (g,x,y)+    where (Id [g],_,[x,y]) = toPrincipal (Id [a,b])

@@ -11,7 +11,7 @@   ---------------------------------------------------------------------------------- | Definition of integral domains+-- | Definition of integral domains.  class CommutativeRing a => IntegralDomain a @@ -20,8 +20,8 @@ propZeroDivisors a b = if a <*> b == zero then a == zero || b == zero else True  --- | Specification of commutative rings. Test that there are no zero-divisors--- commutative and that it satisfies the axioms of commutative rings.+-- | 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 propIntegralDomain a b c = if propZeroDivisors a b                               then propCommutativeRing a b c 

@@ -16,7 +16,7 @@   ---------------------------------------------------------------------------------- | Definition of rings+-- | Definition of rings.  class Ring a where   -- | Addition@@ -72,8 +72,7 @@ propMulIdentity :: (Ring a, Eq a) => a -> (Bool,String) propMulIdentity a = (one <*> a == a && a <*> one == a, "propMulIdentity") --- | Specification of rings.--- Test that the arguments satisfy the ring axioms.+-- | Specification of rings. Test that the arguments satisfy the ring axioms. propRing :: (Ring a, Eq a) => a -> a -> a -> Property propRing a b c = whenFail (print errorMsg) cond   where

@@ -12,7 +12,7 @@ -- -- 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 euclidean domains and the polynomial ring.+-- Examples include all Bezout domains and polynomial rings. -- class Ring a => StronglyDiscrete a where   member :: a -> Ideal a -> Maybe [a]

@@ -1,12 +1,16 @@ {-# LANGUAGE TypeSynonymInstances #-} module Algebra.Z    ( Z-  , module Algebra.Structures.IntegralDomain+  , Ring(..)   ) where  import Test.QuickCheck  import Algebra.Structures.IntegralDomain+import Algebra.Structures.EuclideanDomain+import Algebra.Structures.BezoutDomain+import Algebra.Structures.StronglyDiscrete+import Algebra.Ideal   -- | Type synonym for integers.@@ -25,3 +29,17 @@  propIntegralDomainZ :: Z -> Z -> Z -> Property propIntegralDomainZ = propIntegralDomain++instance EuclideanDomain Z where+  d = abs+  quotientRemainder = quotRem+++propEuclideanDomainZ :: Z -> Z -> Z -> Property+propEuclideanDomainZ = propEuclideanDomain++propBezoutDomainZ :: Ideal Z -> Z -> Z -> Z -> Property+propBezoutDomainZ = propBezoutDomain++propStronglyDiscreteZ :: Z -> Ideal Z -> Bool+propStronglyDiscreteZ = propStronglyDiscrete