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

Number.Peano.Inf.Functions

Synopsis

# Documentation

minimum :: [Nat] -> NatSource

Minimum of the list elements. Works also for empty lists.

maximum :: [Nat] -> NatSource

Maximum of the list elements. Works also for empty lists.

length :: [a] -> NatSource

Lazyness properties of `Nat` makes it ideal for lazy list length computation. Examples:

``` length [1..] > 100
```
``` length undefined >= 0
```
``` length (undefined: undefined) >= 1
```

Arguments

 :: Ord n => (n -> [[n]]) dependence function -> n node -> Nat rank of the node

Rank computation with lazy Peano numbers.

The dependence function represents a graph with multiedges (edges with multiple start nodes). `dependence n` is the list of the start nodes of all multiedges whose end node is `n`.

`nodeRank n` computes the length of the shortest path to `n`. Note that if `n` is an end point of a multiedge with no start point, then `nodeRank n == 0`.

• If `dependence n == []` then `nodeRank n == infinity`, because `n` is not accessable.
• If `any null (dependence n)` then `nodeRank n == 0`
• Otherwise if `dependence n == [l1, l2, ..]` then `nodeRank n == 1 + minimum [maximum (map nodeRank l1), maximum (map nodeRank l2), ..]`

If there is an inevitable cycle in the graph, the rank is `infinity`. One can observe these cases, due to the observable infinity value.