formal_lp/old/formal_interval/interval_m/univariate.hl

   1
   2 (* port of univariate.cc
   3    a univariate represents a function u:real->real.
   4    its first derivative du:real->real
   5    and its second derivative ddu;real->real.
   6
   7    For example, if the function is x |-> x,
   8    its derivative is x |-> 1,
   9    and second derivative is x |-> 0,
  10    which is implemented as ux1.
  11
  12    We give a few other examples, sqrt,  1/x, atan.
  13
  14  *)
  15
  16 module Univariate = struct
  17
  18 open Interval;;
  19
  20 let eval uni x  = function
  21   | 0 -> uni.u x
  22   | 1 -> uni.du x
  23   | _ -> uni.ddu x;;
  24
  25 let mk_univariate (u1,du1,ddu1) = { u = u1; du = du1; ddu = ddu1; };;
  26
  27 let raise_zero x = bounded_from_zero x or  raise Unstable ;;
  28
  29 (* here are a couple of examples *)
  30
  31 let ux1 =
  32   mk_univariate(
  33     (fun x -> x),
  34     (fun x -> one),
  35     (fun x-> zero)
  36   );;
  37
  38 let usqrt =
  39   let ( / ) = idiv in
  40   let ( * ) = imul in
  41     mk_univariate(
  42       isqrt,
  43
  44       (fun x ->
  45         let _ = raise_zero x in
  46           one / (two * isqrt x)),
  47
  48       (fun x ->
  49          let _ = raise_zero x in
  50            ineg (one / ((two * isqrt x) * (two * x))))
  51 );;
  52
  53 let uinv =
  54   let ( / ) = idiv in
  55   let ( * ) = imul in
  56     mk_univariate(
  57       (fun x ->
  58          let _ = raise_zero x in
  59            one / x),
  60
  61       (fun x ->
  62          let _ = raise_zero x in
  63            ineg (one / ( x * x))),
  64
  65       (fun x ->
  66          let _ = raise_zero x in
  67             two / ( x * (x * x)))
  68     );;
  69
  70 let uatan =
  71   let ( / ) = idiv in
  72   let ( * ) = imul in
  73   let ( + ) = iadd in
  74     mk_univariate(
  75       iatan,
  76
  77       (fun x ->
  78          one / (one + x * x)),
  79
  80       (fun x ->
  81          let t = one / (one + x * x) in
  82            (ineg two * x) * (t * t))
  83     );;
  84
  85
  86 let uacos =
  87   let ( / ) = idiv in
  88   let ( * ) = imul in
  89   let ( - ) = isub in
  90     mk_univariate(
  91       iacos,
  92       (fun x ->
  93          ineg (one / isqrt (one - x * x))),
  94       (fun x ->
  95          let t = one - x * x in
  96          ineg (x / isqrt (t * t * t)))
  97     );;
  98
  99 end;;