formal_lp/old/formal_interval/interval_1d/types.hl

   1
   2
   3 exception Unstable;;  (* generally thrown when there is a divide by zero *)
   4
   5 exception Fatal;;  (* generally indicates an uncorrected bug *)
   6
   7 (* represents a closed interval [lo,hi] of the real line *)
   8
   9 type interval = {
  10   lo : float;
  11   hi : float;
  12 };;
  13
  14 (* represents a function u:real->real, its derivative du, and 2nd derivative *)
  15
  16 type univariate = {
  17   u : interval -> interval;
  18   du : interval -> interval;
  19   ddu : interval -> interval;
  20 };;
  21
  22 (* represents the value f of a function and its derivative at some point y *)
  23
  24 type line = {
  25   f : interval;
  26   df : interval;
  27 };;
  28
  29 (*
  30   represents approximation data for a function f on a rectangular domain [x,z].
  31   l gives the value and the derivative of f at some point y in the domain.
  32   dd gives interval bounds on the second derivative over the entire domain.
  33   w i is an upper bound on widths (z - y) and (y - x).
  34 *)
  35
  36 type taylor_interval = {
  37   l : line;
  38   w : float;
  39   dd : interval;
  40 };;
  41
  42
  43