Functions.hs

module Number.Peano.Inf.Functions 
    ( minimum
    , maximum
    , length
    , nodeRank
    ) where

import Number.Peano.Inf

import qualified Data.Set as Set

import qualified Prelude
import Prelude hiding (minimum, maximum, length)

{- |
Minimum of the list elements.
Works also for empty lists.
-}
minimum :: [Nat] -> Nat
minimum = foldr min infinity


{- |
Maximum of the list elements.
Works also for empty lists.
-}
maximum :: [Nat] -> Nat
maximum = foldr max 0

{- | 
Lazyness properties of @Nat@ makes it ideal for lazy list length computation. 
Examples:

> length [1..] > 100

> length undefined >= 0

> length (undefined: undefined) >= 1
-}
length :: [a] -> Nat
length [] = 0
length (_:t) = succ (length t)

{- | 
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.
-}
nodeRank 
    :: Ord n                
    => (n -> [[n]])         -- ^ dependence function
    -> n                    -- ^ node
    -> Nat                  -- ^ rank of the node
nodeRank dependence node = rank Set.empty node  where

    rank visited node
        | Set.member node visited   = infinity
        | otherwise                 = minimum $ map f $ dependence node
     where
        visited' = Set.insert node visited

        f = maximum . map (succ . rank visited')