formal_ineqs/verifier/interval_m/univariate.ml

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