diff --git a/Algebra/Algorithms/Groebner/Monomorphic.hs b/Algebra/Algorithms/Groebner/Monomorphic.hs --- a/Algebra/Algorithms/Groebner/Monomorphic.hs +++ b/Algebra/Algorithms/Groebner/Monomorphic.hs @@ -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 diff --git a/Algebra/Internal.hs b/Algebra/Internal.hs --- a/Algebra/Internal.hs +++ b/Algebra/Internal.hs @@ -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 diff --git a/Algebra/Ring/Polynomial/Monomorphic.hs b/Algebra/Ring/Polynomial/Monomorphic.hs --- a/Algebra/Ring/Polynomial/Monomorphic.hs +++ b/Algebra/Ring/Polynomial/Monomorphic.hs @@ -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 diff --git a/Algebra/Ring/Polynomial/Parser.hs b/Algebra/Ring/Polynomial/Parser.hs --- a/Algebra/Ring/Polynomial/Parser.hs +++ b/Algebra/Ring/Polynomial/Parser.hs @@ -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" diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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`. diff --git a/computational-algebra.cabal b/computational-algebra.cabal --- a/computational-algebra.cabal +++ b/computational-algebra.cabal @@ -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.*