Number.Peano.Inf.Functions

Documentation

minimum :: [Nat] -> Nat

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

maximum :: [Nat] -> Nat

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

length :: [a] -> Nat

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

 length [1..] > 100

 length undefined >= 0

 length (undefined: undefined) >= 1

nodeRank

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 any null (dependence n) then nodeRank n == 0.
• Otherwise nodeRank n == 1 + minimum [maximum (map nodeRank l1), maximum (map nodeRank l2), ..] where [l1, l2, ..] == dependence n if this is computable.
• Otherwise the rank is infinity. (These cases are observable.)

nodeRankMemo

Arguments

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

nodeRankMemoIntegral

Arguments

:: Integral a

=> (a -> [[a]])

dependence function

-> a

node number

-> Nat

rank of the node

nodeRankMemo specialised for integral types.