Ordinals 0.0.0.1 → 0.0.0.2

raw patch · 4 files changed

+123/−26 lines, 4 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• ChangeLog +8/−0
• Main.hs +45/−0
• Math/Ordinals/MultiSet.hs +67/−24
• Ordinals.cabal +3/−2

@@ -0,0 +1,8 @@+2010-07-08  Ahn, Ki Yung <kya@pdx.edu>+	* 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 <kya@pdx.edu>+	* first release 0.0.0.1

@@ -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 []

@@ -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+<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 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+  -- <http://www.volny.cz/behounek/logic/papers/ordcalc/index.html>   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

@@ -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