peano-inf-0.6: Lazy Peano numbers including observable infinity value.

Portability portable experimental divip@aszt.inf.elte.hu

Number.Peano.Inf

Description

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`.

Synopsis

# Documentation

data Nat Source

Natural numbers and infinity.

Instances

 Bounded Nat Enum Nat Eq Nat Integral Nat Num Nat Ord Nat Real Nat Show Nat Serial Nat

Observable infinity value.

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`.

Arguments

 :: Nat n -> Nat m -> Either Nat Nat n >= m: Left (n-m), n < m: Right (m-n)

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`

Arguments

 :: Nat n -> Nat m -> Either Nat Nat n >= m: Left (n-m), n < m: Right (m-n)

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`.

Arguments

 :: Nat n -> Nat m -> Either Nat Nat n >= m: Left (n-m), n < m: Right (m-n)

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`.

(-|) :: Nat -> Nat -> NatSource

Non-negative subtraction. For example, `(5 -| 8 == 0)`.