diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Anders Mörtberg 2010 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Anders Mörtberg nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +import Distribution.Simple +main = defaultMain diff --git a/constructive-algebra.cabal b/constructive-algebra.cabal new file mode 100644 --- /dev/null +++ b/constructive-algebra.cabal @@ -0,0 +1,54 @@ +-- constructive-algebra.cabal auto-generated by cabal init. For +-- additional options, see +-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr. + +Name: constructive-algebra + +-- 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.0.0 + +Synopsis: A library for constructive algebra. +Description: A library for constructive algebra. + +License: BSD3 +License-file: LICENSE + +Author: Anders Mortberg, Bassel Mannaa + +Maintainer: mortberg@student.chalmers.se + +-- A copyright notice. +-- Copyright: + +-- Stability of the pakcage (experimental, provisional, stable...) +Stability: Experimental + +Category: Math, Algebra + +Build-type: Simple + +-- Extra files to be distributed with the package, such as examples or +-- a README. +-- Extra-source-files: + +-- Constraint on the version of Cabal needed to build this package. +Cabal-version: >=1.2 + + +Library + -- Modules exported by the library. + Exposed-modules: Algebra.Structures.Ring + + -- Packages needed in order to build this package. + Build-depends: base >= 3 && <= 4, QuickCheck >= 2 + + -- Modules not exported by this package. + -- Other-modules: + + -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source. + -- Build-tools: + + -- Source directories + hs-source-dirs: src, . diff --git a/src/Algebra/Structures/Ring.hs b/src/Algebra/Structures/Ring.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Structures/Ring.hs @@ -0,0 +1,110 @@ +-- | The representation of the ring structure. +module Algebra.Structures.Ring + ( Ring(..) + , propRing + , (<->), (<^>) + , sumRing, productRing + ) where + +import Test.QuickCheck + + +infixl 8 <^> +infixl 7 <*> +infixl 6 <+> +infixl 6 <-> + + +------------------------------------------------------------------------------- +-- | Definition of rings + +class Ring a where + -- | Addition + (<+>) :: a -> a -> a + + -- | Multiplication + (<*>) :: a -> a -> a + + -- | Compute additive inverse + neg :: a -> a + + -- | The additive identity + zero :: a + + -- | The multiplicative identity + one :: a + + +------------------------------------------------------------------------------- +-- Properties + +-- Addition satisfy the same properties as a commutative group +propAddAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) +propAddAssoc a b c = ((a <+> b) <+> c == a <+> (b <+> c), "propAddAssoc") + +-- Zero is the additive identity +propAddIdentity :: (Ring a, Eq a) => a -> (Bool,String) +propAddIdentity a = (a <+> zero == a && zero <+> a == a, "propAddIdentity") + +-- Negation is the additive inverse +propAddInv :: (Ring a, Eq a) => a -> (Bool,String) +propAddInv a = (neg a <+> a == zero && a <+> neg a == zero, "propAddInv") + +-- Addition is commutative +propAddComm :: (Ring a, Eq a) => a -> a -> (Bool,String) +propAddComm x y = (x <+> y == y <+> x, "propAddComm") + +-- Multiplication is associative +propMulAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) +propMulAssoc a b c = ((a <*> b) <*> c == a <*> (b <*> c), "propMulAssoc") + +-- Multiplication is right-distributive over addition +propRightDist :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) +propRightDist a b c = + ((a <+> b) <*> c == (a <*> c) <+> (b <*> c), "propRightDist") + +-- Multiplication is left-ditributive over addition +propLeftDist :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) +propLeftDist a b c = + (a <*> (b <+> c) == (a <*> b) <+> (a <*> c), "propLeftDist") + +-- One is multiplicative identity +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. +propRing :: (Ring a, Eq a) => a -> a -> a -> Property +propRing a b c = whenFail (print errorMsg) cond + where + (cond,errorMsg) = + propAddAssoc a b c &&& propAddIdentity a &&& propAddInv a &&& + propAddComm a b &&& propMulAssoc a b c &&& propRightDist a b c &&& + propLeftDist a b c &&& propMulIdentity a + + (False,x) &&& _ = (False,x) + _ &&& (False,x) = (False,x) + _ &&& _ = (True,"") + + +------------------------------------------------------------------------------- +-- Operations + +-- | Subtraction +(<->) :: Ring a => a -> a -> a +a <-> b = a <+> neg b + +-- | Summation +sumRing :: Ring a => [a] -> a +sumRing = foldr (<+>) zero + +-- | Product +productRing :: Ring a => [a] -> a +productRing = foldr (<*>) one + +-- | Exponentiation +(<^>) :: Ring a => a -> Integer -> a +x <^> 0 = one +x <^> y = if y < 0 + then error "<^>: Input should be positive" + else x <*> x <^> (y-1)