EuclideanDomain.hs

-- | Representation of Euclidean domains. That is integral domains with an 
-- Euclidean functions and decidable division.
--
module Algebra.Structures.EuclideanDomain 
  ( EuclideanDomain(..)
  , propD, propQuotRem, 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