diff --git a/Number/Peano/Inf.hs b/Number/Peano/Inf.hs --- a/Number/Peano/Inf.hs +++ b/Number/Peano/Inf.hs @@ -6,34 +6,41 @@ Lazy Peano numbers including observable infinity value. -Note that the following equation does /not/ hold for this number type: +Several lazyness properties: -* @1 + a > a@, because @1 + infinity == infinity@. +* @n + undefined >= n@, if @n@ = 0, 1, 2, ... -The following operation is undefined: +but @undefined + n >= n@ raises an error. -* @infinity - infinity@ +* @compare (n + undefined) (n-1) == GT@, if @n@ = 0, 1, 2, ... -There are variants of @(-)@ with different behaviour regarding this, see below. +but @compare (n + undefined) n@ raises an error. -The following operations are naturally undefined: +* @min n (n + undefined)@ results @n@, if @n@ = 0, 1, 2, ... -* @fromEnum infinity@ +* @min (n + undefined) (n - 1)@ results @n - 1@, if @n@ = 0, 1, 2, ... -* @toInteger infinity@ +but @min (n + undefined) n@ raises an error. -* @0 - n@, if @n > 0@ +* @min n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @min 10 (5 + undefined) >= 5@. -* @fromInteger n@, if @n < 0@ +* @min (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ... -* @toEnum n@, if @n < 0@ +* @max n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @max 10 (5 + undefined) >= 5@. -* @pred 0@ +* @max (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ... +These properties makes the @Num@ data type ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@. + +Note that the following equation does /not/ hold for this number type: + +* @1 + a > a@, because @1 + infinity == infinity@. + -} module Number.Peano.Inf ( Nat , infinity + , inductive_infinity , diff , zeroDiff , infDiff @@ -41,19 +48,90 @@ ) where import Data.Ratio ((%)) +{- +Implementation Notes +The observable infinity value has many representatives: + +> Inf +> Succ Inf +> Succ (Succ Inf) +> ... + +Multiple representatives need extra caretaking: Every function on @Nat@ must be well defined. + +A function @f :: Nat -> Nat@ is well defined if for all @n@ and @m@ which are representatives of +the observable infinity, both @f n@ and @f m@ should be + +* either @0@, @1@, @2@, ..., @bottom@, @Succ bottom@, @Succ (Succ bottom)@, ... + +* or (maybe different) representatives of the observable infinity + +The functions in this module obey this rule. +The abstract @Nat@ data type ensures that the users should not take care of this rule. +-} + -- | Natural numbers and infinity. data Nat = Zero | Succ Nat | Inf --- | Observable infinity value. +{- | +Observable infinity value. +The following values are @True@: + +* @infinity == infinity@ + +* @0 < infinity@, @1 < infinity@, @2 < infinity@, ... + +* @n + infinity == infinity@, if @n@ is not the inductive infinity. + +* @infinity + n == infinity@ + +* @n * infinity == infinity@, if @n@ is not the inductive infinity. + +* @infinity * n == infinity@ + +* @n - infinity == 0@, if @n@ is not the inductive infinity. + +* @infinity - n == infinity@, if @n@ is not the inductive infinity and if @n /= infinity@. + +The following values rais error messages: + +* @infinity - infinity@ + +* @fromEnum infinity@ + +* @toInteger infinity@ +-} infinity :: Nat infinity = Inf +{- | +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@: + +* @0 < inductive_infinity@, @1 < inductive_infinity@, @2 < inductive_infinity@, ... + +Note also: + +* @inductive_infinity == infinity@ is an endless computation instead of @True@. +-} +inductive_infinity :: Nat +inductive_infinity = let n = Succ n in n + + + instance Eq Nat where Zero == Zero = True @@ -112,7 +190,15 @@ Just i -> show i Nothing -> "infinity" --- | Difference of two natural numbers: the result is either positive or negative. +{- | +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@ +-} diff :: Nat -- ^ n -> Nat -- ^ m @@ -126,7 +212,17 @@ Succ n `diff` Inf = n `diff` Inf --- | Variant of @diff@: @infDiff infinity infinity == Left infinity@. +{- | +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@. +-} infDiff :: Nat -- ^ n -> Nat -- ^ m @@ -139,7 +235,17 @@ Zero `infDiff` m = Right m --- | Variant of @diff@: @zeroDiff infinity infinity == Left 0@. +{- | +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@. +-} zeroDiff :: Nat -- ^ n -> Nat -- ^ m @@ -198,6 +304,15 @@ enumFrom n = enumFromTo n Inf + {- | + @[inf.. inf] == [inf, inf, inf, ..@ + + instead of + + @[inf.. inf] == [inf]@ + + Both are reasonable but the second solution would make @enumfrom@ much more eager. + -} enumFromTo n m = case m `infDiff` n of Right _ -> [] diff --git a/peano-inf.cabal b/peano-inf.cabal --- a/peano-inf.cabal +++ b/peano-inf.cabal @@ -1,5 +1,5 @@ name: peano-inf -version: 0.3 +version: 0.4 synopsis: Lazy Peano numbers including observable infinity value. description: Lazy Peano numbers including observable infinity value.