Documentation
Lazyness properties of Nat
makes it ideal for lazy list length computation.
Examples:
length [1..] > 100
length undefined >= 0
length (undefined: undefined) >= 1
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
any null (dependence n)
thennodeRank n == 0
. - Otherwise
nodeRank n == 1 + minimum [maximum (map nodeRank l1), maximum (map nodeRank l2), ..] where
[l1, l2, ..] == dependence nif this is computable.
- Otherwise the rank is
infinity
. (These cases are observable.)
:: (n -> [[n]]) | dependence function |
-> (n -> Nat) | memoised version of the result function |
-> n -> Nat | rank of a node |
Memoising version of nodeRank
.
The rank of inaccessable nodes are inductive_infinity
.
These cases are observable with the predicate (> n)
where n
is an upper bound for the number of nodes in the graph.
nodeRankMemo
specialised for integral types.