computational-algebra 0.0.2.0 → 0.0.3.0
raw patch · 6 files changed
+138/−89 lines, 6 filesdep +peggy
Dependencies added: peggy
Files
- Algebra/Algorithms/Groebner/Monomorphic.hs +2/−4
- Algebra/Internal.hs +81/−15
- Algebra/Ring/Polynomial/Monomorphic.hs +8/−0
- Algebra/Ring/Polynomial/Parser.hs +44/−68
- README.md +1/−1
- computational-algebra.cabal +2/−1
Algebra/Algorithms/Groebner/Monomorphic.hs view
@@ -67,8 +67,7 @@ let t = freshVar (g : j) in eliminate [t] $ (one - g * injectVar t) : j --- | Calculate saturation ideal. The saturation of an ideal I by an ideal J is defined as follows:--- I : J^∞ = { f ∈ k[X] | ∃ n > 0 s.t. f J^n ⊆ I }+-- | Calculate saturation ideal. saturationIdeal :: Groebnerable r => [Polynomial r] -> [Polynomial r] -> [Polynomial r] saturationIdeal i g = intersection $ map (i `saturationByPrincipalIdeal`) g @@ -77,8 +76,7 @@ quotByPrincipalIdeal i g = map (snd . head . flip (divPolynomialWith Lex) [g]) $ intersection [i, [g]] --- | Calculate the ideal quotient of I of J, defind as follows:--- I : J = { f ∈ k[X] | fJ ⊆ I }+-- | Calculate the ideal quotient of I of J. quotIdeal :: Groebnerable r => [Polynomial r] -> [Polynomial r] -> [Polynomial r] quotIdeal i g = intersection $ map (i `quotByPrincipalIdeal`) g
Algebra/Internal.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} {-# LANGUAGE MultiParamTypeClasses, PolyKinds, StandaloneDeriving #-} {-# LANGUAGE TypeFamilies, TypeOperators #-}+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Algebra.Internal ( toProxy, Nat(..), SNat(..), Vector(..), Sing(..) , SingInstance(..), singInstance, toInt , Min, Max, sMin, sMax, sZ, sS, (:+:), (%+), (:-:), (%-)@@ -17,9 +18,9 @@ , eqlTrans, plusZR, plusZL, eqPreservesS, plusAssociative , sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent , eqSuccMinus, plusMinusEqL, plusMinusEqR, plusLeqL, plusLeqR- , zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR+ , zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR, plusSR , leqRhs, leqLhs, leqTrans, minComm, leqAnitsymmetric- , maxZL, maxComm, maxZR, maxLeqL, maxLeqR+ , maxZL, maxComm, maxZR, maxLeqL, maxLeqR, plusMonotone , module Monomorphic ) where import Data.Proxy@@ -253,6 +254,41 @@ case singInstance n of SingInstance -> SingInstance +data Reason x y where+ Because :: SNat y -> Eql x y -> Reason x y++because :: SNat y -> Eql x y -> Reason x y+because = Because++infixl 4 ===, =~=+infix 5 `Because`+infix 5 `because`+++(===) :: Eql x y -> Reason y z -> Eql x z+eq === (_ `Because` eq') = eqlTrans eq eq'++(=~=) :: Eql x y -> SNat y -> Eql x y+eq =~= _ = eq++start :: SNat a -> Eql a a+start = eqlRefl++definition, byDefinition :: Sing a => Eql a a+byDefinition = eqlRefl sing+definition = eqlRefl sing++admitted :: Reason x y+admitted = undefined+{-# WARNING admitted "There are some goals left yet unproven." #-}++infix 4 :=:+type a :=: b = Eql a b++cong' :: (SNat m -> SNat (f m)) -> a :=: b -> f a :=: f b+cong' _ Eql = Eql++ leqRefl :: SNat n -> Leq n n leqRefl SZ = ZeroLeq sZ leqRefl (SS n) = SuccLeqSucc $ leqRefl n@@ -276,8 +312,9 @@ plusZR :: SNat n -> Eql (n :+: Z) n plusZR SZ = Eql plusZR (SS n) =- case plusZR n of- Eql -> Eql+ start (sS n %+ sZ)+ =~= sS (n %+ sZ)+ === sS n `because` cong' sS (plusZR n) plusZL :: SNat n -> Eql (Z :+: n) n plusZL _ = Eql@@ -289,26 +326,39 @@ -> Eql (n :+: (m :+: l)) ((n :+: m) :+: l) plusAssociative SZ _ _ = Eql plusAssociative (SS n) m l =- case plusAssociative n m l of- Eql -> Eql+ start (sS n %+ (m %+ l))+ =~= sS (n %+ (m %+ l))+ === sS ((n %+ m) %+ l) `because` cong' sS (plusAssociative n m l)+ =~= sS (n %+ m) %+ l+ =~= (sS n %+ m) %+ l sAndPlusOne :: SNat n -> Eql (S n) (n :+: One) sAndPlusOne SZ = Eql sAndPlusOne (SS n) =- case sAndPlusOne n of- Eql -> Eql+ start (sS (sS n))+ === sS (n %+ sOne) `because` cong' sS (sAndPlusOne n)+ =~= sS n %+ sOne +plusCongL :: SNat n -> m :=: m' -> n :+: m :=: n :+: m'+plusCongL _ Eql = Eql++plusCongR :: SNat n -> m :=: m' -> m :+: n :=: m' :+: n+plusCongR _ Eql = Eql+ plusCommutative :: SNat n -> SNat m -> Eql (n :+: m) (m :+: n) plusCommutative SZ SZ = Eql plusCommutative SZ (SS m) =- case plusZR (SS m) of- Eql -> Eql+ start (sZ %+ sS m)+ =~= sS m+ === sS (m %+ sZ) `because` cong' sS (plusCommutative SZ m)+ =~= sS m %+ sZ plusCommutative (SS n) m =- case plusCommutative n m of- Eql -> case sAndPlusOne (m %+ n) of- Eql -> case plusAssociative m n sOne of- Eql -> case sAndPlusOne n of- Eql -> Eql+ start (sS n %+ m)+ =~= sS (n %+ m)+ === sS (m %+ n) `because` cong' sS (plusCommutative n m)+ === (m %+ n) %+ sOne `because` sAndPlusOne (m %+ n)+ === m %+ (n %+ sOne) `because` eqlSymm (plusAssociative m n sOne)+ === m %+ sS n `because` plusCongL m (eqlSymm $ sAndPlusOne n) minusCongEq :: Eql n m -> SNat l -> Eql (n :-: l) (m :-: l) minusCongEq Eql _ = Eql@@ -384,6 +434,7 @@ leqTrans :: Leq n m -> Leq m l -> Leq n l leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql+leqTrans _ _ = error "impossible!" minComm :: SNat n -> SNat m -> Eql (Min n m) (Min m n) minComm SZ SZ = Eql@@ -418,4 +469,19 @@ maxLeqR :: SNat n -> SNat m -> Leq m (Max n m) maxLeqR n m = case maxComm n m of Eql -> maxLeqL m n++plusSR :: SNat n -> SNat m -> Eql (S (n :+: m)) (n :+: S m)+plusSR n m =+ start (sS (n %+ m))+ === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m)+ === n %+ (m %+ sOne) `because` eqlSymm (plusAssociative n m sOne)+ === n %+ sS m `because` plusCongL n (eqlSymm $ sAndPlusOne m)++plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)+plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)+plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =+ case plusSR m (leqRhs leq) of+ Eql -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq+plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'+ -- (m + S n) - m = S (m + n) - m
Algebra/Ring/Polynomial/Monomorphic.hs view
@@ -41,6 +41,12 @@ normalizeMonom :: Monomial -> Monomial normalizeMonom = M.filter (/= 0) +instance (Eq r, NoetherianRing r) => NA.LeftModule r (Polynomial r) where+ c .* Polynomial d = normalize $ Polynomial $ fmap (c NA.*) d++instance (Eq r, NoetherianRing r) => NA.RightModule r (Polynomial r) where+ (*.) = flip (NA..*)+ instance (Eq r, NoetherianRing r) => NoetherianRing (Polynomial r) instance (Eq r, NoetherianRing r) => NA.Commutative (Polynomial r) instance (Eq r, NoetherianRing r) => NA.Multiplicative (Polynomial r) where@@ -183,3 +189,5 @@ injectVar :: NA.Unital r => Variable -> Polynomial r injectVar var = Polynomial $ M.singleton (M.singleton var 1) NA.one +injectCoeff :: r -> Polynomial r+injectCoeff c = Polynomial $ M.singleton M.empty c
Algebra/Ring/Polynomial/Parser.hs view
@@ -1,89 +1,65 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE QuasiQuotes #-} module Algebra.Ring.Polynomial.Parser where import Algebra.Ring.Polynomial.Monomorphic import Control.Applicative hiding (many)-import Control.Arrow-import Data.Char import qualified Data.Map as M-import Data.Maybe import Data.Ratio-import qualified Numeric.Algebra as NA-import Text.Parsec hiding (optional, (<|>))-import Text.Parsec.String--variable :: Parser Variable-variable = Variable <$> letter <*> optional (char '_' *> index)--variableWithPower :: Parser (Variable, Integer)-variableWithPower = (,) <$> lexeme variable <*> option 1 power- where- power = symbol '^' *> parseInt--index :: Parser Int-index = digitToInt <$> digit- <|> read <$ symbol '{' <*> lexeme (many1 digit) <* symbol '}'+import qualified Numeric.Algebra as NA+import Text.Peggy -monomial :: Parser Monomial-monomial = M.fromList <$> many variableWithPower+[peggy|+expression :: Polynomial Rational+ = expr !. -term :: Parser (Monomial, Rational)-term = signed' $ try $ flip (,) <$> option 1 coefficient- <*> monomial- <|> flip (,) <$> number <*> pure M.empty+letter :: Char+ = [a-zA-Z] -signed' p = do- s <- optional sign- (n, c) <- p- return (n, fromMaybe 1 s * c)- where- sign = lexeme $ char '-' *> return (negate 1)- <|> char '+' *> return 1+variable :: Variable+ = letter ('_' integer)? { Variable $1 (fromInteger <$> $2) } +variableWithPower :: (Variable, Integer)+ = variable "^" natural { ($1, $2) }+ / variable { ($1, 1) } -symbol :: Char -> Parser Char-symbol = lexeme . char+expr :: Polynomial Rational+ = expr "+" term { $1 + $2 }+ / expr "-" term { $1 - $2 }+ / term -lexeme :: Parser a -> Parser a-lexeme p = p <* spaces+term :: Polynomial Rational+ = number space* monoms { $1 NA..* $3 }+ / number { injectCoeff $1 }+ / monoms -toPolyn = normalize . Polynomial . M.fromList+monoms :: Polynomial Rational+ = monoms space * fact { $1 * $3 }+ / fact -polyOp :: Parser (Polynomial Rational -> Polynomial Rational -> Polynomial Rational)-polyOp = (NA.-) <$ symbol '-'- <|> (NA.+) <$ symbol '+'+fact :: Polynomial Rational+ = fact "^" natural { $1 ^ $2 }+ / "(" expr ")"+ / monomial { toPolyn [($1, 1)] } -expression :: Parser (Polynomial Rational)-expression = (spaces *> (toPolyn <$> count 1 term) `chainl1` polyOp <* eof)+monomial :: Monomial+ = variableWithPower+ { M.fromListWith (+) $1 } -coefficient :: Parser Rational-coefficient = char '(' *> number <* char ')'- <|> number+number :: Rational+ = integer "/" integer { $1 % $2 }+ / integer '.' [0-9]+ { realToFrac (read (show $1 ++ '.' : $2) :: Double) }+ / integer { fromInteger $1 } -number :: Parser Rational-number = signed $- try (toRational <$> parseDouble)- <|> try (lexeme $ (%) <$> parseInt- <* symbol '/'- <*> parseInt)- <|> toRational <$> parseInt+integer :: Integer+ = "-" natural { negate $1 }+ / natural -parseInt :: Parser Integer-parseInt = lexeme $ read <$> many1 digit+natural :: Integer+ = [1-9] [0-9]* { read ($1 : $2) } -signed :: Num b => Parser b -> Parser b-signed p = do- s <- optional sign- n <- p- return $ fromMaybe 1 s * n- where- sign = lexeme $ char '-' *> return (negate 1)- <|> char '+' *> return 1+|] -parseDouble :: Parser Double-parseDouble = lexeme $ do- int <- many1 digit- _ <- char '.'- float <- many1 digit- return $ read $ int ++ '.':float+toPolyn :: [(Monomial, Ratio Integer)] -> Polynomial (Ratio Integer)+toPolyn = normalize . Polynomial . M.fromList parsePolyn :: String -> Either ParseError (Polynomial Rational)-parsePolyn = parse expression "polynomial"+parsePolyn = parseString expression "polynomial"
README.md view
@@ -38,7 +38,7 @@ ------------ Due to GHC 7.4.*'s bug, this library contains extra modules and functionalities as follows: -* `Monomorphic` data-type and his frieds+* `Monomorphic` data-type and his friends * This is completely separeted as [`monomorphic`](http://hackage.haskell.org/package/monomorphic) package. But due to GHC 7.4.1, which is shipped with latest Haskell Platform, I include the functionality from this library for a while. * Singleton types and functions * Because the [`singletons`](http://hackage.haskell.org/package/singletons) package is not available in GHC 7.4.1, I provide limited version of the functionalities of that package in `Algebra.Internal` module. After new HP released, I will entirely rewrite all source codes using `singletons`.
computational-algebra.cabal view
@@ -2,7 +2,7 @@ -- further documentation, see http://haskell.org/cabal/users-guide/ name: computational-algebra-version: 0.0.2.0+version: 0.0.3.0 synopsis: Well-kinded computational algebra library, currently supporting Groebner basis. description: Dependently-typed computational algebra libray for Groebner basis. homepage: https://github.com/konn/computational-algebra@@ -34,5 +34,6 @@ , lens == 3.* , containers >= 0.4 && < 0.6 , parsec == 3.*+ , peggy == 0.3.* if impl(ghc >= 7.6.1) build-depends: monomorphic == 0.0.*