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