diff --git a/ChangeLog b/ChangeLog new file mode 100644 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,8 @@ +2010-07-08 Ahn, Ki Yung + * second release 0.0.0.2 + * no changes to the library itself + * few more QuickCheck properties + * slightliy improved documentation + +2010-07-08 Ahn, Ki Yung + * first release 0.0.0.1 diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -0,0 +1,45 @@ +import Math.Ordinals.MultiSet +import Test.QuickCheck +import Control.Monad +import Data.List + +sortwf (O os) = O $ sortBy (\ a b -> case compare a b of + { GT -> LT; LT -> GT; EQ -> EQ }) os + +instance Arbitrary Ordinal where + arbitrary = liftM sortwf $ oneof [ return 0 + , liftM2 (.:) arbitrary arbitrary ] + +prop_wf o = wf o -- sanity check for arbitrary definition for Ordinal + +-- http://planetmath.org/encyclopedia/PropertiesOfOrdinalArithmetic.html +prop_add_identity_l o = 0 + o == o where types = o :: Ordinal +prop_add_identity_r o = o + 0 == o where types = o :: Ordinal +prop_add_assoc a b c = a + (b + c) == (a + b) + c where types = a :: Ordinal +prop_sub_def a b | a <= b = a + (b - a) == b + | otherwise = prop_sub_def b a + where types = a :: Ordinal +prop_mult_identity_l o = 1 * o == o where types = o :: Ordinal +prop_mult_identity_r o = o * 1 == o where types = o :: Ordinal +prop_mult_zero_l o = 0 * o == 0 where types = o :: Ordinal +prop_mult_zero_r o = o * 0 == 0 where types = o :: Ordinal +prop_mult_assoc a b c = a * (b * c) == (a * b) * c where types = a :: Ordinal +prop_mult_dist_l a b c = a * (b + c) == a*b + a*c where types = a :: Ordinal +-- TODO division ??? div not yet defined +-- http://planetmath.org/encyclopedia/OrdinalExponentiation.html +-- TODO exponentiation +prop_power_zero o = o > 0 ==> 0 ^: o == 0 where types = o :: Ordinal +prop_power_one o = 1 ^: o == 1 where types = o :: Ordinal -- fails TODO +prop_power_of_one o = o ^: 1 == o where types = o :: Ordinal +prop_power_mult a b c = a^:b * a^:c == a^:(b+c) where types = a :: Ordinal -- fails TODO + +a :: Ordinal +a = 2 -- O [O [],O []] +b :: Ordinal +b = 1 -- O [O []] +c :: Ordinal +c = w (w 1 + 1) + 1 -- [O [O [O []],O []],O []] + +prop_power_power a b c = (a^:b)^:c == a^:(b*c) where types = a :: Ordinal -- fails TODO + +main = print $ O [] diff --git a/Math/Ordinals/MultiSet.hs b/Math/Ordinals/MultiSet.hs --- a/Math/Ordinals/MultiSet.hs +++ b/Math/Ordinals/MultiSet.hs @@ -1,32 +1,64 @@ --- Encoding of ordinals up to epsilon_0 as an iterated multiset: --- definition in Basic Proof Theory by Troelstra and Schwichenberg. --- Note, this is not the most efficient way to calculate ordinals. --- This library is better than having none. --- I think CNF representation would be more efficent, --- planning to add in the next version of this library. +{- | +Encoding of ordinals up to epsilon_0 as an iterated multiset: +definition in Basic Proof Theory by Troelstra and Schwichenberg. +Note, this is not the most efficient way to calculate ordinals. +This library is better than having none. +I think CNF representation would be more efficent, +planning to add in the next version of this library. --- For further analysis on efficiency of implementations on ordinals see --- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.8089 --- FYI, An ordinal calculator that covers wider range beyond epsion_0 --- can be found at http://www.mtnmath.com/ord/ which is written C++. --- However, I found a serious errors in this calculator: --- the property a^b * a^c == a^(b+c) doesn't hold. --- (e.g., --- ordCalc> 3 ^(w^w + w + 1) * 3^(w^w) == 3 ^ (w^w + w + 1 + w^w) --- FALSE ) --- This calculator didn't seem to run QuickCeck style tests --- although it does have large tests cases some of them seg faults sometimes --- depending on the machine I built this ord calcualtor. +For further analysis on efficiency of implementations on ordinals see + +FYI, an ordinal calculator that covers wider range beyond epsion_0 +can be found at which is written C++. +However, I found a serious error in this calculator (ver 0.2): +the property a^b * a^c == a^(b+c) does not hold. For example, -module Math.Ordinals.MultiSet where +@ + ordCalc> 3 ^(w^w + w + 1) * 3^(w^w) == 3 ^ (w^w + w + 1 + w^w) + FALSE +@ +This calculator didn't seem to run QuickCeck style automatic +testing, although it does have hundreds (or maybe more than a thousand) +tests cases but some of them even causes segmentation faults +depending on the machine I built this ordCalc. +-} +module Math.Ordinals.MultiSet ( + -- * Types + Ordinal(..) + + -- * Operators + , (^:) + -- | There are more operators such as + -- '+' (addition), '*' (multiplication), '-', (left addtion) + -- defined in the 'Num' class instance declaration for 'Ordinal'. + -- Although ordinals are not really 'Num' we decided to make it + -- as a 'Num' instance for convenience; We can use functions such + -- as 'sum' and 'product' over list of ordinals and they behave well. + -- We also plan to implement division and remainder operations + -- in the 'Integral' class instance for similar reason. For further + -- information on class instances see the source code. + + -- * Auxiliary functions + , w, wf + + -- * Auxiliary operators + -- | These operators can manipulate the 'Ordinal' newtype data structure + -- internally. Use with care since it can break the well-formedness ('wf') + -- of ordinal representation. + , (.:), (++.), (.++.) + ) where + import Data.List (groupBy, intersperse) newtype Ordinal = O [Ordinal] deriving Eq +-- | convenience function that takes an argument as the power of omega +-- (the first limit ordinal). +w :: Ordinal -> Ordinal w o = O [o] instance Show Ordinal where @@ -47,7 +79,8 @@ EQ -> compare as bs r -> r --- well formedness of ordinals +-- | well formedness of ordinals +wf :: Ordinal -> Bool wf (O []) = True wf (O [o]) = wf o wf (O (o:os@(o':_))) = o >= o' && wf (O os) @@ -64,12 +97,16 @@ toInteger o@(O as) | all (0 ==) as = fromIntegral (toInt o) toInteger _ = error "ordinal not less than omega" + -- | Left division. not yet defined div a b = fst (divMod a b) + -- | not yet defined mod a b = snd (divMod a b) - divMod = quotRem -- TODO -- somebody help figure this out + -- | not yet defined + divMod = quotRem + -- | not yet defined -- TODO -- somebody help figure this out quotRem _ _ = error "Ordinal quotRem not yet defined" @@ -82,9 +119,11 @@ signum 0 = 0 signum (O(o:os)) = O[o] + -- | Addition. o + 0 = o O as + O bs@(b:_) = O (takeWhile (>=b) as ++ bs) + -- | Left subtraction -- for a <= b exists r = b - a such that a + r = b -- i.e., a + (b - a) = b for a <= b o - 0 = o @@ -94,8 +133,9 @@ EQ -> O as - O bs GT -> o1 - -- something similar to - -- http://www.volny.cz/behounek/logic/papers/ordcalc/index.html + -- | Multiplication. + -- Implemented as something similar to + -- 0 * _ = 0 o1@(O(a:as)) * O bs | null bs' = sum [o1 | _ <- zs] -- finite @@ -104,8 +144,11 @@ where (bs',zs) = span (>0) bs (as1,as2) = span (a==) (a:as) --- exponentiation : define new op since neither ^ nor ^^ will work +-- | Exponentiation. +-- Defined a new operator since neither '^' nor '^^' will work. +-- Note, @(w o)@ is same as @(w 1 :^ o)@ for any oridnal @o@. infixr 8 ^: +(^:) :: Ordinal -> Ordinal -> Ordinal _ ^: 0 = 1 0 ^: _ = 0 1 ^: _ = 1 diff --git a/Ordinals.cabal b/Ordinals.cabal --- a/Ordinals.cabal +++ b/Ordinals.cabal @@ -1,5 +1,5 @@ name: Ordinals -version: 0.0.0.1 +version: 0.0.0.2 synopsis: Ordinal arithmetic description: Ordinal arithmetic implementation up to epsilon_0. Currently based on interated multiset representation, @@ -9,9 +9,10 @@ license-file: LICENSE author: Ki Yung Ahn maintainer: kya@pdx.edu -homepage: https://patch-tag.com/r/kyagrd/Ordinals/ +homepage: http://patch-tag.com/r/kyagrd/Ordinals/ build-depends: base < 5 build-type: Simple ghc-options: -Wall exposed-modules: Math.Ordinals.MultiSet ghc-prof-options: -auto-all +extra-source-files: ChangeLog Main.hs