diff --git a/Number/Peano/Inf.hs b/Number/Peano/Inf.hs --- a/Number/Peano/Inf.hs +++ b/Number/Peano/Inf.hs @@ -6,10 +6,7 @@ Lazy Peano numbers including observable infinity value. -Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'. - -The lazy operations of @Num@ makes it ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@. - +Properties of @Nat@ can be found in the source of "Number.Peano.Inf.Test". -} module Number.Peano.Inf ( Nat @@ -67,26 +64,14 @@ {- | Traditional infinity value: @let n = Succ n in n@. -For every function @f :: Nat -> Bool@, @f infinity@ and @f inductive_infinity@ gives the same result, provided that -the results are not bottom. - -Use @infinity@ instead. Lots of the given properties of @infinity@ is not true for @inductive_infinity@. For example, - -* @inductive_infinity == inductive_infinity@ is an endless computation instead of @True@. - -However, the following values are @True@: - -* @n < inductive_infinity@, @n@ = 0, 1, 2,... - -Note also: - -* @inductive_infinity == infinity@ is an endless computation instead of @True@. +@infinity@ is equal to @inductive_infinity@ but @infinity@ is lazier. +In other words: +For every function @f :: Nat -> Bool@, either @f inductive_infinity@ is bottom or @f inductive_infinity@ is equal to @f infinity@. -} inductive_infinity :: Nat inductive_infinity = let n = Succ n in n - instance Eq Nat where Zero == Zero = True @@ -96,6 +81,7 @@ Inf == Succ m = Inf == m _ == _ = False + instance Ord Nat where Zero `compare` Zero = EQ @@ -145,15 +131,16 @@ Just i -> show i Nothing -> "infinity" + {- | Difference of two natural numbers: the result is either positive or negative. -implementation of @(-)@ is based on @diff@. - The following value is undefined: * @diff infinity infinity@ -} +infix 6 `diff` + diff :: Nat -- ^ n -> Nat -- ^ m @@ -171,13 +158,16 @@ Variant of @diff@: * @infDiff infinity infinity == Left infinity@. - +-} +{- Note that if the implementation of @(-)@ would be based on @infDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == infinity /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == infinity /= 5@. -} +infixl 6 `infDiff` + infDiff :: Nat -- ^ n -> Nat -- ^ m @@ -194,13 +184,16 @@ Variant of @diff@: * @zeroDiff infinity infinity == Left 0@. - +-} +{- Note that if the implementation of @(-)@ would be based on @zeroDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == 0 /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == 0 /= 5@. -} +infixl 6 `zeroDiff` + zeroDiff :: Nat -- ^ n -> Nat -- ^ m @@ -215,7 +208,7 @@ --- | Non-negative subtraction. For example, @(5 -| 8 == 0)@. +-- | Non-negative subtraction. For example, @5 -| 8 == 0@. infixl 6 -| (-|) :: Nat -> Nat -> Nat @@ -247,6 +240,7 @@ signum Zero = Zero signum _ = Succ Zero + instance Enum Nat where succ = Succ @@ -258,6 +252,12 @@ toEnum i | i < 0 = error "Number.Peano.Inf: toEnum on negative value." toEnum i = iterate Succ Zero !! i + fromEnum n = f 0 n where + + f i Zero = i + f i (Succ m) = i' `seq` f i' m where i' = i+1 + f _ Inf = error "Number.Peano.Inf: fromEnum infinity." + enumFrom n = enumFromTo n Inf {- | @@ -318,17 +318,11 @@ f (Left j) l = l: f (j `infDiff` d) (d + l) - fromEnum n = f 0 n where - - f i Zero = i - f i (Succ m) = i' `seq` f i' m where i' = i+1 - f _ Inf = error "Number.Peano.Inf: fromEnum infinity." - - instance Real Nat where toRational n = toRational (fromIntegral n :: Integer) + instance Integral Nat where toInteger n = case toInteger' n of @@ -336,6 +330,7 @@ Nothing -> error "Number.Peano.Inf: toInteger infinity." quotRem _ _ = error "Number.Peano.Inf: quotRem not implemented." + instance Bounded Nat where diff --git a/Number/Peano/Inf/Functions.hs b/Number/Peano/Inf/Functions.hs --- a/Number/Peano/Inf/Functions.hs +++ b/Number/Peano/Inf/Functions.hs @@ -24,6 +24,17 @@ maximum :: [Nat] -> Nat maximum = foldr max 0 +{- | +Lazyness properties of @Nat@ makes it ideal for lazy list length computation. +Examples: + +> length [1..] > 100 + +> length undefined >= 0 + +> length (undefined: undefined) >= 1 +-} + length :: [a] -> Nat length [] = 0 length (_:t) = succ (length t) diff --git a/Number/Peano/Inf/Test.hs b/Number/Peano/Inf/Test.hs --- a/Number/Peano/Inf/Test.hs +++ b/Number/Peano/Inf/Test.hs @@ -1,3 +1,6 @@ +{- | +You can find the properties in the source code. +-} {-# LANGUAGE ScopedTypeVariables #-} @@ -6,79 +9,246 @@ ) where import Number.Peano.Inf - import Test.LazySmallCheck hiding (test) +import Data.List default (Nat) +------ helper functions + +sm :: Testable a => a -> IO () +sm = smallCheck 10 + +(=~=) :: Eq a => [a] -> [a] -> Bool +as =~= bs = take 15 as == take 15 bs + +infix 1 <=> +(<=>) :: Bool -> Bool -> Bool +(<=>) = (==) + + +----------- Properties of Nat ------------ + +-- Note that (n::Nat) means that @n = 0, 1, 2..@ or @n = infinity@, but @inductive_infinity@ will not appear. + test :: IO () test = do --- Several lazyness properties +-- Eq - smallCheck 10 $ + sm $ \(n::Nat) -> n == n - undefined >= (0::Nat) + sm $ \(n::Nat) (m::Nat) -> n == m <=> m == n - smallCheck 10 $ \(n::Nat) -> and + sm $ \(n::Nat) (m::Nat) (k::Nat) -> n == m && m == k ==> n == k - [ n + undefined >= n -- but @undefined + n@ raises an error. - , n /= infinity ==> (1 + n + undefined) `compare` n == GT -- but @compare (n + undefined) n@ raises an error. +-- (<=) - , n `min` (n + undefined) == n + sm $ \(n::Nat) (m::Nat) (k::Nat) -> n <= m && m <= k ==> n <= k - , (1 + n + undefined) `min` n == n -- but @min (n + undefined) n@ raises an error. - ] + sm $ \(n::Nat) (m::Nat) -> n <= m && m <= n <=> n == m - smallCheck 10 $ \(m::Nat) (n::Nat) -> and + sm $ \(n::Nat) (m::Nat) -> n <= m || m <= n - [ (m + n) `min` (m + undefined) >= m +-- sm $ \(n::Nat) (m::Nat) -> xor [n < m, n == m, m < n] - , (m + undefined) `min` (m + n) >= m - , n `max` (m + undefined) >= m +-- (<), (>), (>=), compare - , (m + undefined) `max` n >= m + sm $ \(n::Nat) (m::Nat) -> n < m <=> n <= m && n /= m - ] + sm $ \(n::Nat) (m::Nat) -> n > m <=> m < n --- Properties of infinity + sm $ \(n::Nat) (m::Nat) -> n >= m <=> m <= n - smallCheck 10 $ and + sm $ \(n::Nat) (m::Nat) -> n `compare` m == case () of + _ | n < m -> LT + | n == m -> EQ + | n > m -> GT - [ infinity == infinity +-- min, max - , 0 * infinity == 0 + sm $ \(n::Nat) (m::Nat) -> (n `min` m, n `max` m) `elem` [(n, m), (m, n)] - , infinity * 0 == 0 + sm $ \(n::Nat) (m::Nat) -> n `min` m <= n && n `min` m <= m - ] + sm $ \(n::Nat) (m::Nat) -> n `max` m >= n && n `max` m >= m - smallCheck 10 $ \(n::Nat) -> and - [ n /= infinity ==> n < infinity +-- (+) - , n + infinity == infinity + sm $ \(n::Nat) (m::Nat) -> n + m == m + n - , infinity + n == infinity + sm $ \(n::Nat) (m::Nat) (k::Nat) -> n + (m + k) == (n + m) + k - , n /= 0 ==> n * infinity == infinity + sm $ \(n::Nat) -> 0 + n == n - , n /= 0 ==> infinity * n == infinity + sm $ \(n::Nat) -> infinity + n == infinity - , n /= infinity ==> infinity - n == infinity + sm $ \(n::Nat) -> n == infinity || n `elem` iterate (1+) 0 - ] + sm $ \(n::Nat) -> n /= infinity ==> n < 1 + n -{- -The following values raise error messages: +-- diff -* @infinity - infinity@, + sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> (d + n) `diff` n == Left d -* @fromEnum infinity@, + sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> n `diff` (1 + d + n) == Right (1 + d) -* @toInteger infinity@. --} + -- infinity `diff` infinity is undefined + + +-- zeroDiff, infDiff, (-), (-|) + + sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `zeroDiff` m == n `diff` m + + sm $ infinity `zeroDiff` infinity == Left 0 + + sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `infDiff` m == n `diff` m + + sm $ infinity `infDiff` infinity == Left infinity + + sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> Left (n - m) == n `diff` m + + sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> n -| m == n - m + + sm $ \(n::Nat) (m::Nat) -> n <= m && m /= infinity ==> n -| m == 0 + + +-- (*) + + sm $ \(n::Nat) -> 0 * n == 0 + + sm $ \(n::Nat) (m::Nat) -> (1 + n) * m == m + n * m + +-- sm $ \(n::Nat) -> n /= 0 ==> infinity * n == infinity + +-- sm $ \(n::Nat) (m::Nat) -> n * m == m * n + +-- sm $ \(n::Nat) (m::Nat) (k::Nat) -> n * (m * k) == (n * m) * k + + + +-- minBound, maxBound + + sm $ minBound == (0::Nat) && maxBound == infinity + + sm $ \(n::Nat) -> minBound <= n + + sm $ \(n::Nat) -> n <= maxBound + + +-- toInteger, fromInteger + + sm $ toInteger (0::Nat) == 0 + + sm $ \(n::Nat) -> n /= infinity ==> toInteger (1 + n) == 1 + toInteger n + + -- toInteger infinity is undefined + + sm $ \(n::Nat) -> n /= infinity ==> fromInteger (toInteger n) == n + + sm $ \(n::Integer) -> n >= 0 ==> toInteger (fromInteger n :: Nat) == n + + +-- toEnum, fromEnum + + sm $ \(n::Int) -> n >= 0 ==> (toEnum n :: Nat) == fromInteger (toInteger n) + + sm $ \(n::Nat) -> n /= infinity ==> toInteger (fromEnum n) == toInteger n + + +-- succ, pred + + sm $ \(n::Nat) -> succ n == 1 + n + + sm $ \(n::Nat) -> pred (1 + n) == n + + +-- enumFrom + + sm $ \(n::Nat) -> head [n.. ] == n + + sm $ \(n::Nat) -> tail [n.. ] =~= [1+n.. ] + +-- sm $ \(n::Nat) -> [n.. ] =~= [n, 1+n.. ] + + +-- enumFromTo + + sm $ \(n::Nat) (m::Nat) -> [n.. m] =~= takeWhile (<= m) [n..] + + +-- enumFromThen (non-decreasing) + + sm $ \(n::Nat) (m::Nat) -> take 2 [n, m.. ] == [n, m] + + sm $ \(n::Nat) (d::Nat) -> tail [n, d+n.. ] =~= [d+n, d+d+n.. ] + + +-- enumFromThen (non-increasing) + + sm $ \(n::Nat) (d::Nat) -> d /= infinity ==> tail [d+d+n, d+n.. ] =~= [d+n, n.. ] + +-- sm $ \(n::Nat) (d::Nat) -> tail [d+d+d+n, d+d+n.. ] =~= [d+d+n, d+n.. ] + + sm $ \(n::Nat) (d::Nat) -> n < d ==> tail [d+n, n.. ] == [n] + + +-- enumFromThenTo + + sm $ \(n::Nat) (m::Nat) (k::Nat) -> [n, m.. k] =~= case n `compare` m of + + LT -> takeWhile (<= k) [n, m..] + EQ -> [n, m..] + GT -> takeWhile (>= k) [n, m..] + + +-- inductive_infininty + + sm $ \(n::Nat) -> n /= infinity ==> n < inductive_infinity + + + +------- Lazyness properties of Nat ---------- + + + + sm $ (0::Nat) <= undefined + + + sm $ infinity + undefined == infinity + + sm $ \(n::Nat) -> n /= infinity ==> inductive_infinity + undefined > n + + sm $ \(n::Nat) -> n + undefined >= n + +-- sm $ \(n::Nat) -> undefined + n >= n -- raises an error + + sm $ \(n::Nat) -> n /= infinity ==> 1 + n + undefined > n + + + sm $ \(n::Nat) -> n `min` (n + undefined) == n + + sm $ \(n::Nat) -> (1 + n + undefined) `min` n == n + +-- sm $ \(n::Nat) -> (n + undefined) `min` n == n -- raises an error + + sm $ \(n::Nat) (m::Nat) -> (n + undefined) `min` (m + undefined) >= n `min` m + + + sm $ \(n::Nat) (m::Nat) -> n `max` (m + undefined) >= m + + sm $ \(n::Nat) (m::Nat) -> (m + undefined) `max` n >= m + + sm $ \(n::Nat) (m::Nat) -> (n + undefined) `max` (m + undefined) >= n `min` m + + + sm $ \(n::Nat) -> (1 + undefined) * n >= n + + sm $ \(n::Nat) -> n /= infinity ==> (1 + undefined) * inductive_infinity > n + + diff --git a/peano-inf.cabal b/peano-inf.cabal --- a/peano-inf.cabal +++ b/peano-inf.cabal @@ -1,10 +1,8 @@ name: peano-inf -version: 0.6 +version: 0.6.1 synopsis: Lazy Peano numbers including observable infinity value. description: Lazy Peano numbers including observable infinity value. - . - This data type was needed in a graph traversing algorithm. . This data type is ideal for lazy list length computation (the infinite value is not needed in this case). For a comparison with other Peano number implementation, see