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




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



:: Ord n 
=> (n -> [[n]])

dependence function

-> n


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