Limits

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

> module Limes          (  Extended (..), mapE, limes
>                       )
> where

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

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

> import Ratio
>
> import CPS
> import Function       (  Function(..), Prim(..),
>                          minus, (***), zero, one, mone, two, mtwo  )

----------------------------------------------------------------------
Type definitions

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

> dontknow = zzero

> data Signum           =  Neg | Zero | Pos
>                       deriving (Eq, Show)

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

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

> instance Num Signum where
>     Zero * _          =  Zero
>     _    * Zero       =  Zero
>     Neg  * Neg        =  Pos
>     Neg  * Pos        =  Neg
>     Pos  * Neg        =  Neg
>     Pos  * Pos        =  Pos
>     _ + _    = error "Num Signum, not implemented"
>     abs _    = error "Num Signum, not implemented"
>     signum _ = error "Num Signum, not implemented"
>     fromInteger n
>         | n < 0       =  Neg
>         | n == 0      =  Zero
>         | n > 0       =  Pos

----------------------------------------------------------------------
Reprasentation eigentlicher und uneigentlicher Werte.
Representation to ghostwrite and unghostwrite values.
----------------------------------------------------------------------

> data Extended val     =  MInfty | Proper val | Infty deriving (Eq)
> type Value            =  Extended Function

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

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

> isProper MInfty       =  False
> isProper (Proper _)   =  True
> isProper Infty        =  False

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

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

> mapE f MInfty         =  MInfty
> mapE f (Proper v)     =  Proper (f v)
> mapE f Infty          =  Infty

----------------------------------------------------------------------
Sign
----------------------------------------------------------------------

> signOf MInfty         =  unit Neg
> signOf (Proper (Ratio n))
>     | n < 0           =  unit Neg
>     | n == 0          =  unit Zero
>     | n > 0           =  unit Pos
> signOf Infty          =  unit Pos
> signOf _              =  dontknow                     -- catch all

----------------------------------------------------------------------
Eigentliche und uneigentliche Grenzwerte
Ghostwrite and unghostwrite limit values
----------------------------------------------------------------------

> limes                 :: Value -> Function -> Maybe Value
> limes a f             =  firstSolution (lim a f) ()

----------------------------------------------------------------------
Grenzwerte primitiver Funktionen.
Limits on primitive functions
----------------------------------------------------------------------

> limPrim               :: Value -> Prim -> BT st Value res
> limPrim MInfty f      =  case f of
>     Exp               -> proper zero
>     Arctan            -> proper (mtwo *** (Prim Arctan :.: one))
>     Arccot            -> proper (Ratio (4 % 1) *** (Prim Arctan :.: one))
>     Sinh              -> minfty
>     Cosh              -> infty
>     Tanh              -> proper mone
>     Coth              -> proper mone
>     Abs               -> infty
>     _                 -> dontknow                     -- catch all
> limPrim v@(Proper a) f        =  case f of
>     Tan               -> dontknow
>     Cot               -> dontknow
>     Ln                -> signOf v &= \s -> case s of
>         Neg           -> dontknow
>         Zero          -> minfty
>         Pos           -> proper (Prim Ln :.: a)
>     Coth              -> signOf v &= \s -> case s of
>         Zero          -> dontknow
>         _             -> proper (Prim Coth :.: a)
>     _                 -> proper (Prim f :.: a)        -- catch all
> limPrim Infty f       =  case f of
>     Exp               -> infty
>     Ln                -> infty
>     Arctan            -> proper (two *** (Prim Arctan :.: one))
>     Arccot            -> proper zero
>     Sinh              -> infty
>     Cosh              -> infty
>     Tanh              -> proper zero
>     Coth              -> proper zero
>     Abs               -> infty
>     _                 -> dontknow                     -- catch all

----------------------------------------------------------------------
Grenzwerte von Funktionen.
Limit values for functions.
----------------------------------------------------------------------

> lim                   :: Value -> Function -> BT st Value res
> lim a n@(Ratio _)     =  proper n
> lim a n@(Const _)     =  proper n
> lim a (Prim f)        =  limPrim a f
> lim a (Fun f)         =  dontknow
> lim a (Derive n f)    =  dontknow
> lim a Id              =  unit a
> lim a (f :.: g)       =  lim a g                              &= \lg ->
>                          lim lg f
> lim a (Summ fs)       =  accumulat [ lim a f | f<-fs ]        &= \lfs ->
>                          if MInfty `elem` lfs then
>                              if Infty `elem` lfs then
>                                  hospital a n d
>                              else
>                                  minfty
>                          else
>                              if Infty `elem` lfs then
>                                  infty
>                              else
>                                  proper (Summ [ f | Proper f<-lfs ])
>     where n           =  Summ [ Prod gs :^: mone | gs<-remove fs ]
>           d           =  Prod fs :^: mone
> lim a (Prod fs)       =  accumulat [ lim a f | f<-fs ]        &= \lfs ->
>                          if all isProper lfs then
>                              proper (Prod [ f | Proper f<-lfs ])
>                          else
>                              accumulat [ signOf f | f<-lfs ]  &= \sfs ->
>                              if Zero `elem` sfs then
>                                  hospital a n d
>                              else
>                                  case product sfs of
>                                      Neg -> minfty
>                                      Pos -> infty
>     where n           =  Prod [] -- HACK: nur vorlaufig --only temporary
>           d           =  Prod [] -- HACK: nur vorlaufig
> lim a (f :^: g)       =  lim a (Prim Exp :.: g *** (Prim Ln :.: f))

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

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

> minfty                =  unit MInfty
> proper n              =  unit (Proper n)
> infty                 =  unit Infty

----------------------------------------------------------------------
Satz von de L'Hospital
L'Hospital's rule
----------------------------------------------------------------------

> hospital a f g        =  dontknow

----------------------------------------------------------------------
Hilfsfunktionen

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

> remove []             =  []
> remove (a:x)          =  x : [ a:x' | x'<-remove x ]

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