Functions.hs

module Number.Peano.Inf.Functions 
    ( minimum
    , maximum
    , length
    , nodeRank
--    , nodeRankSimple 
    , nodeRankMemo
    , nodeRankMemoIntegral
    ) 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)


nodeRankSimple 
    :: (n -> [[n]]) 
    -> n 
    -> Nat

nodeRankSimple dependence = rank where

    rank = minimum . map f . dependence

    f = maximum . map (succ . rank)


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

nodeRank dependence = rank Set.empty  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')


{- | 
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
    :: (n -> [[n]])         -- ^ dependence function
    -> (n -> Nat)           -- ^ memoised version of the result function
    -> (n -> Nat)           -- ^ rank of a node

nodeRankMemo dependence rank' = rank  where

    rank = minimum . map f . dependence

    f = maximum . map (succ . rank')

{- | 
@nodeRankMemo@ specialised for integral types.
-}
nodeRankMemoIntegral
    :: Integral a
    => (a -> [[a]])         -- ^ dependence function
    -> a                    -- ^ node number
    -> Nat                  -- ^ rank of the node

nodeRankMemoIntegral dep = f where 

    f = nodeRankMemo dep (memoise f)

----------------- memoisation for non-negative integrals

data T x = B x (T x) (T x)

memoise :: Integral a => (a -> x) -> (a -> x)
memoise = decode . code
 where
	code f = B (f 0) (code (\n -> f (2*n+1)))
		             (code (\n -> f (2*n+2)))

	decode (B x l r) n 
		| n == 0    = x
		| odd n     = decode l (n `div` 2)
		| otherwise = decode r ((n-2) `div` 2)

-----------------