formal_lp/old/arith/informal/informal_m_taylor.hl

   1 (* Dependencies *)
   2 needs "../formal_lp/arith/informal/informal_arith.hl";;
   3 needs "../formal_lp/arith/informal/informal_eval_interval.hl";;
   4
   5
   6 module Informal_taylor = struct
   7
   8 open Informal_interval;;
   9 open Informal_float;;
  10 open Informal_atn;;
  11 open Informal_eval_interval;;
  12
  13
  14 type m_cell_domain =
  15 {
  16   lo : ifloat list;
  17   hi : ifloat list;
  18   y : ifloat list;
  19   w : ifloat list;
  20 };;
  21
  22
  23 type m_taylor_interval =
  24 {
  25   n : int;
  26   domain : m_cell_domain;
  27   f : interval;
  28   df : interval list;
  29   ddf : interval list list;
  30 };;
  31
  32
  33 let float_0 = mk_small_num_float 0 and
  34     float_1 = mk_small_num_float 1 and
  35     float_2 = mk_small_num_float 2;;
  36
  37 let float_inv2 = div_float_lo 1 float_1 float_2;;
  38
  39 (* convert_to_float_list *)
  40 let convert_to_float_list pp lo_flag list_tm =
  41   let tms = dest_list list_tm in
  42   let i_funs = map build_interval_fun tms in
  43   let ints = map (fun f -> eval_interval_fun pp f [] []) i_funs in
  44   let extract = (if lo_flag then fst else snd) o dest_interval in
  45     map extract ints;;
  46
  47
  48 (* mk_m_center_domain *)
  49 let mk_m_center_domain pp x_list z_list =
  50   let y_list =
  51     let ( * ), (+) = mul_float_eq, add_float_hi pp in
  52       map2 (fun x z -> if eq_float x z then x else float_inv2 * (x + z)) x_list z_list in
  53
  54   (* test: x <= y <= z *)
  55   let flag1 = itlist2 (fun x y a -> le_float x y && a) x_list y_list true and
  56       flag2 = itlist2 (fun y z a -> le_float y z && a) y_list z_list true in
  57     if not flag1 or not flag2 then
  58       failwith "mk_m_center_domain: ~(x <= y <= z)"
  59     else
  60       let w_list =
  61         let (-) = sub_float_hi pp in
  62         let w1 = map2 (-) y_list x_list in
  63         let w2 = map2 (-) z_list y_list in
  64           map2 max_float w1 w2 in
  65         {lo = x_list; hi = z_list; y = y_list; w = w_list};;
  66
  67
  68 (* eval_m_taylor (pp0 for initial evaluation of constants) *)
  69 let eval_m_taylor pp0 f_tm partials partials2 =
  70   let build = eval_constants pp0 o build_interval_fun o snd o dest_abs in
  71   let f = build f_tm in
  72   let n = length partials in
  73   (* Verify that the list of second partial derivatives is correct *)
  74   let _ =  map2 (fun i list -> if length list <> i then
  75                    failwith "eval_m_taylor: incorrect partials2" else ()) (1--n) partials2 in
  76   let dfs = map (build o rand o concl) partials in
  77   let d2fs = map (build o rand o concl) (List.flatten partials2) in
  78   let f_dfs_list = find_and_replace_all (f :: dfs) [] in
  79   let rec shape_list dd i =
  80     if i >= n then [dd] else
  81       let l1, l2 = chop_list i dd in
  82         l1 :: shape_list l2 (i + 1) in
  83   let d2fs_list = find_and_replace_all d2fs [] in
  84     fun p_lin p_second domain ->
  85       let y_ints = map (fun y -> mk_interval (y, y)) domain.y in
  86       let xz_ints = map mk_interval (zip domain.lo domain.hi) in
  87       let f_dfs_vals = eval_interval_fun_list p_lin f_dfs_list y_ints in
  88       let d2fs_vals = eval_interval_fun_list p_second d2fs_list xz_ints in
  89         {n = n; domain = domain;
  90          f = hd f_dfs_vals; df = tl f_dfs_vals;
  91         ddf = shape_list d2fs_vals 1};;
  92
  93
  94 (* mk_eval_functionq *)
  95 let mk_eval_function pp0 f_tm =
  96   let build = eval_constants pp0 o build_interval_fun o snd o dest_abs in
  97   let f = build f_tm in
  98   let f_list = find_and_replace_all [f] [] in
  99     fun pp x_list z_list ->
 100       let xz_ints = map mk_interval (zip x_list z_list) in
 101       let f_val = eval_interval_fun_list pp f_list xz_ints in
 102         hd f_val;;
 103
 104
 105 (* error_mul_f2_hi *)
 106 let error_mul_f2_hi pp a int = mul_float_hi pp a (abs_interval int);;
 107
 108
 109 (* eval_m_taylor_error *)
 110 (* sum_{i = 1}^n (w_i * (f_ii * w_i + 2 * sum_{j = 1}^{i - 1} w_j * f_ij)) *)
 111 let eval_m_taylor_error pp ti =
 112   let w = ti.domain.w in
 113   let ns = 1--ti.n in
 114   let ( * ), ( + ) = mul_float_hi pp, add_float_hi pp in
 115   let mul_wdd = map2 (fun list i -> Arith_misc.my_map2 (error_mul_f2_hi pp) w list) ti.ddf ns in
 116   let sums1 = map (end_itlist ( + ) o butlast) (tl mul_wdd) in
 117   let sums2 = (hd o hd) mul_wdd :: map2 (fun list t1 -> last list + float_2 * t1) (tl mul_wdd) sums1 in
 118   let sums = map2 ( * ) w sums2 in
 119     end_itlist ( + ) sums;;
 120
 121
 122 (* eval_m_taylor_upper_bound *)
 123 let eval_m_taylor_upper_bound pp ti =
 124   let f_hi = (snd o dest_interval) ti.f in
 125   let error = eval_m_taylor_error pp ti in
 126   let ( * ), ( + ) = mul_float_hi pp, add_float_hi pp in
 127   let sum2 =
 128     let mul_wd = map2 (error_mul_f2_hi pp) ti.domain.w ti.df in
 129       end_itlist ( + ) mul_wd in
 130   let a = sum2 + float_inv2 * error in
 131     f_hi + a;;
 132
 133 (* eval_m_taylor_lower_bound *)
 134 let eval_m_taylor_lower_bound pp ti =
 135   let f_lo = (fst o dest_interval) ti.f in
 136   let error = eval_m_taylor_error pp ti in
 137   let ( * ), ( + ), ( - ) = mul_float_hi pp, add_float_hi pp, sub_float_lo pp in
 138   let sum2 =
 139     let mul_wd = map2 (error_mul_f2_hi pp) ti.domain.w ti.df in
 140       end_itlist ( + ) mul_wd in
 141   let a = sum2 + float_inv2 * error in
 142     f_lo - a;;
 143
 144
 145 (* eval_m_taylor_bound *)
 146 let eval_m_taylor_bound pp ti =
 147   let f_lo, f_hi = dest_interval ti.f in
 148   let error = eval_m_taylor_error pp ti in
 149   let ( * ), ( + ), ( - ) = mul_float_hi pp, add_float_hi pp, sub_float_lo pp in
 150   let sum2 =
 151     let mul_wd = map2 (error_mul_f2_hi pp) ti.domain.w ti.df in
 152       end_itlist ( + ) mul_wd in
 153   let a = sum2 + float_inv2 * error in
 154   let hi = f_hi + a in
 155   let lo = f_lo - a in
 156     mk_interval (lo, hi);;
 157
 158
 159 (* eval_m_taylor_partial_upper *)
 160 let eval_m_taylor_partial_upper pp i ti =
 161   let df_hi = (snd o dest_interval o List.nth ti.df) (i - 1) in
 162   let dd_list = map (fun j -> if j <= i then
 163                        List.nth (List.nth ti.ddf (i - 1)) (j - 1)
 164                      else
 165                        List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
 166   let sum2 =
 167     let mul_dd = map2 (error_mul_f2_hi pp) ti.domain.w dd_list in
 168       end_itlist (add_float_hi pp) mul_dd in
 169     add_float_hi pp df_hi sum2;;
 170
 171
 172 (* eval_m_taylor_partial_lower *)
 173 let eval_m_taylor_partial_lower pp i ti =
 174   let df_lo = (fst o dest_interval o List.nth ti.df) (i - 1) in
 175   let dd_list = map (fun j -> if j <= i then
 176                        List.nth (List.nth ti.ddf (i - 1)) (j - 1)
 177                      else
 178                        List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
 179   let sum2 =
 180     let mul_dd = map2 (error_mul_f2_hi pp) ti.domain.w dd_list in
 181       end_itlist (add_float_hi pp) mul_dd in
 182     sub_float_lo pp df_lo sum2;;
 183
 184
 185 (* eval_m_taylor_partial_bound *)
 186 let eval_m_taylor_partial_bound pp i ti =
 187   let df_lo, df_hi = (dest_interval o List.nth ti.df) (i - 1) in
 188   let dd_list = map (fun j -> if j <= i then
 189                        List.nth (List.nth ti.ddf (i - 1)) (j - 1)
 190                      else
 191                        List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
 192   let sum2 =
 193     let mul_dd = map2 (error_mul_f2_hi pp) ti.domain.w dd_list in
 194       end_itlist (add_float_hi pp) mul_dd in
 195   let lo = sub_float_lo pp df_lo sum2 in
 196   let hi = add_float_hi pp df_hi sum2 in
 197     mk_interval (lo, hi);;
 198
 199
 200 (* add *)
 201 let eval_m_taylor_add p_lin p_second taylor1 taylor2 =
 202   let ( + ), ( ++ ) = add_interval p_lin, add_interval p_second in
 203     {
 204       n = taylor1.n;
 205       domain = taylor1.domain;
 206       f = taylor1.f + taylor2.f;
 207       df = map2 (+) taylor1.df taylor2.df;
 208       ddf = map2 (map2 (++)) taylor1.ddf taylor2.ddf
 209     };;
 210
 211
 212 (* sub *)
 213 let eval_m_taylor_sub p_lin p_second taylor1 taylor2 =
 214   let ( - ), ( -- ) = sub_interval p_lin, sub_interval p_second in
 215     {
 216       n = taylor1.n;
 217       domain = taylor1.domain;
 218       f = taylor1.f - taylor2.f;
 219       df = map2 (-) taylor1.df taylor2.df;
 220       ddf = map2 (map2 (--)) taylor1.ddf taylor2.ddf
 221     };;
 222
 223
 224 (* mul *)
 225 let eval_m_taylor_mul p_lin p_second ti1 ti2 =
 226   let n = ti1.n in
 227   let ns = 1--n in
 228   let bounds = mul_interval p_lin ti1.f ti2.f in
 229   let df = map2 (fun d1 d2 ->
 230                    let ( * ), ( + ) = mul_interval p_lin, add_interval p_lin in
 231                      d1 * ti2.f + ti1.f * d2) ti1.df ti2.df in
 232   let d1_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti1) ns in
 233   let d2_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti2) ns in
 234   let f1_bound = eval_m_taylor_bound p_second ti1 in
 235   let f2_bound = eval_m_taylor_bound p_second ti2 in
 236   let ddf =
 237     let ( * ), ( + ) = mul_interval p_second, add_interval p_second in
 238       map2 (fun (list1, list2) i ->
 239               let di1 = List.nth d1_bounds (i - 1) in
 240               let di2 = List.nth d2_bounds (i - 1) in
 241                 map2 (fun (dd1, dd2) j ->
 242                         let dj1 = List.nth d1_bounds (j - 1) in
 243                         let dj2 = List.nth d2_bounds (j - 1) in
 244                           (dd1 * f2_bound + di1 * dj2) + (dj1 * di2 + f1_bound * dd2))
 245                   (zip list1 list2) (1--i)) (zip ti1.ddf ti2.ddf) ns in
 246     {
 247       n = n;
 248       domain = ti1.domain;
 249       f = bounds;
 250       df = df;
 251       ddf = ddf;
 252     };;
 253
 254
 255 (* inv *)
 256 let eval_m_taylor_inv p_lin p_second ti =
 257   let n = ti.n in
 258   let ns = 1--n in
 259   let f1_bound = eval_m_taylor_bound p_second ti in
 260   let bounds = inv_interval p_lin ti.f in
 261   let u_bounds =
 262     let neg, inv, ( * ) = neg_interval, inv_interval p_lin, mul_interval p_lin in
 263       neg (inv (ti.f * ti.f)) in
 264   let df =
 265     let ( * ) = mul_interval p_lin in
 266       map (fun d -> u_bounds * d) ti.df in
 267   let d1_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti) ns in
 268   let d1, d2 =
 269     let inv, ( * ) = inv_interval p_second, mul_interval p_second in
 270     let ff = f1_bound * f1_bound in
 271       inv ff, two_interval * inv (f1_bound * ff) in
 272   let ddf =
 273     let ( * ), ( - ) = mul_interval p_second, sub_interval p_second in
 274       map2 (fun dd_list di1 ->
 275               Arith_misc.my_map2 (fun dd dj1 ->
 276                                     (d2 * dj1) * di1 - d1 * dd) dd_list d1_bounds) ti.ddf d1_bounds in
 277     {
 278       n = n;
 279       domain = ti.domain;
 280       f = bounds;
 281       df = df;
 282       ddf = ddf;
 283     };;
 284
 285
 286 (* sqrt *)
 287 let eval_m_taylor_sqrt p_lin p_second ti =
 288   let n = ti.n in
 289   let ns = 1--n in
 290   let f1_bound = eval_m_taylor_bound p_second ti in
 291   let bounds = sqrt_interval p_lin ti.f in
 292   let u_bounds =
 293     let inv, ( * ) = inv_interval p_lin, mul_interval p_lin in
 294       inv (two_interval * bounds) in
 295   let df =
 296     let ( * ) = mul_interval p_lin in
 297       map (fun d -> u_bounds * d) ti.df in
 298   let d1_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti) ns in
 299   let d1, d2 =
 300     let neg, sqrt, inv, ( * ) = neg_interval, sqrt_interval p_second,
 301       inv_interval p_second, mul_interval p_second in
 302     let two_sqrt_f = two_interval * sqrt f1_bound in
 303       inv two_sqrt_f, neg (inv (two_sqrt_f * (two_interval * f1_bound))) in
 304   let ddf =
 305     let ( * ), ( + ) = mul_interval p_second, add_interval p_second in
 306       map2 (fun dd_list di1 ->
 307               Arith_misc.my_map2 (fun dd dj1 ->
 308                                     (d2 * dj1) * di1 + d1 * dd) dd_list d1_bounds) ti.ddf d1_bounds in
 309     {
 310       n = n;
 311       domain = ti.domain;
 312       f = bounds;
 313       df = df;
 314       ddf = ddf;
 315     };;
 316
 317
 318 (* atn *)
 319 let eval_m_taylor_atn =
 320   let neg_two_interval = neg_interval two_interval in
 321     fun p_lin p_second ti ->
 322       let n = ti.n in
 323       let ns = 1--n in
 324       let f1_bound = eval_m_taylor_bound p_second ti in
 325       let bounds = atn_interval p_lin ti.f in
 326       let u_bounds =
 327         let inv, ( + ), ( * ) = inv_interval p_lin, add_interval p_lin, mul_interval p_lin in
 328           inv (one_interval + ti.f * ti.f) in
 329       let df =
 330         let ( * ) = mul_interval p_lin in
 331           map (fun d -> u_bounds * d) ti.df in
 332       let d1_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti) ns in
 333       let d1, d2 =
 334         let neg, inv, ( + ), ( * ) = neg_interval, inv_interval p_second,
 335           add_interval p_second, mul_interval p_second in
 336         let pow2 = pow_interval p_second 2 in
 337         let inv_one_ff = inv (one_interval + f1_bound * f1_bound) in
 338           inv_one_ff, (neg_two_interval * f1_bound) * pow2 inv_one_ff in
 339       let ddf =
 340         let ( * ), ( + ) = mul_interval p_second, add_interval p_second in
 341           map2 (fun dd_list di1 ->
 342                   Arith_misc.my_map2 (fun dd dj1 ->
 343                                         (d2 * dj1) * di1 + d1 * dd) dd_list d1_bounds) ti.ddf d1_bounds in
 344         {
 345           n = n;
 346           domain = ti.domain;
 347           f = bounds;
 348           df = df;
 349           ddf = ddf;
 350         };;
 351
 352
 353 (* acs *)
 354 let eval_m_taylor_acs p_lin p_second ti =
 355   let n = ti.n in
 356   let ns = 1--n in
 357   let f1_bound = eval_m_taylor_bound p_second ti in
 358   let bounds = acs_interval p_lin ti.f in
 359   let u_bounds =
 360     let inv, sqrt, neg = inv_interval p_lin, sqrt_interval p_lin, neg_interval in
 361     let ( * ), ( - ) = mul_interval p_lin, sub_interval p_lin in
 362       neg (inv (sqrt (one_interval - ti.f * ti.f))) in
 363   let df =
 364     let ( * ) = mul_interval p_lin in
 365       map (fun d -> u_bounds * d) ti.df in
 366   let d1_bounds = map (fun i -> eval_m_taylor_partial_bound p_second i ti) ns in
 367   let d1, d2 =
 368     let neg, sqrt, inv = neg_interval, sqrt_interval p_second, inv_interval p_second in
 369     let ( - ), ( * ), ( / ) = sub_interval p_second, mul_interval p_second, div_interval p_second in
 370     let pow3 = pow_interval p_second 3 in
 371     let ff_1 = one_interval - f1_bound * f1_bound in
 372       inv (sqrt ff_1), neg (f1_bound / sqrt (pow3 ff_1)) in
 373   let ddf =
 374     let ( * ), ( - ) = mul_interval p_second, sub_interval p_second in
 375       map2 (fun dd_list di1 ->
 376               Arith_misc.my_map2 (fun dd dj1 ->
 377                                     (d2 * dj1) * di1 - d1 * dd) dd_list d1_bounds) ti.ddf d1_bounds in
 378     {
 379       n = n;
 380       domain = ti.domain;
 381       f = bounds;
 382       df = df;
 383       ddf = ddf;
 384     };;
 385
 386
 387 end;;
 388
 389
 390 (*
 391 (* Tests *)
 392
 393 open Informal_taylor;;
 394
 395 let dest_int int =
 396   let f1, f2 = Informal_interval.dest_interval int in
 397     Informal_float.dest_float f1, Informal_float.dest_float f2;;
 398
 399 let dest_ti ti =
 400   dest_int ti.f, map dest_int ti.df, map (map dest_int) ti.ddf;;
 401
 402 let dest_f = Informal_float.dest_float;;
 403
 404
 405 needs "../formal_lp/formal_interval/m_taylor_arith2.hl";;
 406
 407 let convert_to_float_list pp lo_flag list_tm =
 408   let tms = dest_list list_tm in
 409   let i_funs = map build_interval_fun tms in
 410   let ints = map (fun f -> eval_interval_fun pp f [] []) i_funs in
 411   let extract = (if lo_flag then fst else snd) o dest_pair o rand o concl in
 412     mk_list (map extract ints, real_ty);;
 413
 414
 415 let pp = 7;;
 416 let poly = expr_to_vector_fun `x1 + x2 * x3 + x3 * (x1 + x3 pow 2)`;;
 417 let n = (get_dim o fst o dest_abs) poly;;
 418
 419 let xx = `[#1.1; &2; -- sqrt(&2)]` and
 420     zz = `[&3; &3; &1 + sqrt(&3)]`;;
 421
 422 let xx1 = convert_to_float_list pp true xx and
 423     zz1 = convert_to_float_list pp false zz;;
 424
 425 let xx0 = Informal_taylor.convert_to_float_list pp true xx and
 426     zz0 = Informal_taylor.convert_to_float_list pp false zz;;
 427
 428 let dom_th = mk_m_center_domain n pp xx1 zz1;;
 429 let dom = Informal_taylor.mk_m_center_domain pp xx0 zz0;;
 430
 431 let partials = map (fun i -> gen_partial_poly i poly) (1--n);;
 432 let get_partial i eq_th =
 433   let partial_i = gen_partial_poly i (rand (concl eq_th)) in
 434   let pi = (rator o lhand o concl) partial_i in
 435     REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i);;
 436 let partials2 = map (fun j ->
 437                        let th = List.nth partials (j - 1) in
 438                          map (fun i -> get_partial i th) (1--j)) (1--n);;
 439
 440 let diff_th = gen_diff_poly poly;;
 441 let diff2_th = gen_diff2c_domain_poly poly;;
 442 let lin_th = gen_lin_approx_poly_thm poly diff_th partials;;
 443 let second_th = gen_second_bounded_poly_thm poly partials2;;
 444
 445 let eval_taylor = eval_m_taylor pp diff2_th lin_th second_th;;
 446 let taylor = Informal_taylor.eval_m_taylor pp poly partials partials2;;
 447
 448 let ti_th = eval_taylor pp pp dom_th;;
 449 let ti = taylor pp pp dom;;
 450 dest_ti ti;;
 451
 452 eval_m_taylor_bound n pp ti_th;;
 453 dest_int (Informal_taylor.eval_m_taylor_bound pp ti);;
 454
 455 eval_m_taylor_partial_upper n pp 3 ti_th;;
 456 dest_f (Informal_taylor.eval_m_taylor_partial_upper pp 3 ti);;
 457
 458 let t2_th = eval_m_taylor_sub n 2 5 ti_th ti_th;;
 459 let t2 = Informal_taylor.eval_m_taylor_sub 2 5 ti ti;;
 460 dest_ti t2;;
 461
 462 eval_m_taylor_sub n 8 8 ti_th t2_th;;
 463 dest_ti (Informal_taylor.eval_m_taylor_sub 8 8 ti t2);;
 464
 465 let xx = `[#0.0; &0; sqrt(&0)]` and
 466     zz = `[#0.2; #0.1; sqrt(&0) + #0.1]`;;
 467
 468 let xx1 = convert_to_float_list pp true xx and
 469     zz1 = convert_to_float_list pp false zz;;
 470
 471 let xx0 = Informal_taylor.convert_to_float_list pp true xx and
 472     zz0 = Informal_taylor.convert_to_float_list pp false zz;;
 473
 474 let dom_th = mk_m_center_domain n pp xx1 zz1;;
 475 let dom = Informal_taylor.mk_m_center_domain pp xx0 zz0;;
 476
 477
 478 let ti_th = eval_taylor pp pp dom_th;;
 479 let ti = taylor pp pp dom;;
 480 let th = eval_m_taylor_acs n pp pp ti_th;;
 481 let t = Informal_taylor.eval_m_taylor_acs pp pp ti;;
 482 dest_ti t;;
 483
 484 eval_m_taylor_bound n 20 th;;
 485 dest_int (Informal_taylor.eval_m_taylor_bound 20 t);;
 486
 487 eval_m_taylor_partial_bound n 20 2 th;;
 488 dest_int (Informal_taylor.eval_m_taylor_partial_bound 20 2 t);;
 489
 490 eval_m_taylor_mul n pp pp ti_th th;;
 491 dest_ti (Informal_taylor.eval_m_taylor_mul pp pp ti t);;
 492
 493
 494 (* 1.20 *)
 495 test 100 eval_taylor dom_th;;
 496 (* 0.04 *)
 497 test 100 taylor dom;;
 498
 499 (* bounds *)
 500 eval_m_taylor_bound n pp ti_th;;
 501 dest_int (Informal_taylor.eval_m_taylor_bound pp ti);;
 502
 503 eval_m_taylor_upper_bound n pp ti_th;;
 504 dest_f (Informal_taylor.eval_m_taylor_upper_bound pp ti);;
 505
 506 eval_m_taylor_lower_bound n pp ti_th;;
 507 dest_f (Informal_taylor.eval_m_taylor_lower_bound pp ti);;
 508
 509
 510 (* 1.288 *)
 511 test 100 (eval_m_taylor_bound n pp) ti_th;;
 512 (* 0.044 *)
 513 test 100 (Informal_taylor.eval_m_taylor_bound pp) ti;;
 514
 515
 516
 517 (* partials *)
 518
 519 eval_m_taylor_upper_partial n pp 1 ti_th;;
 520 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 1 ti);;
 521
 522 eval_m_taylor_upper_partial n pp 2 ti_th;;
 523 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 2 ti);;
 524
 525 eval_m_taylor_upper_partial n pp 3 ti_th;;
 526 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 3 ti);;
 527
 528
 529 eval_m_taylor_lower_partial n pp 1 ti_th;;
 530 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 1 ti);;
 531
 532 eval_m_taylor_lower_partial n pp 2 ti_th;;
 533 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 2 ti);;
 534
 535 eval_m_taylor_lower_partial n pp 3 ti_th;;
 536 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 3 ti);;
 537
 538 eval_m_taylor_interval_partial n pp 1 ti_th;;
 539 dest_int (Informal_taylor.eval_m_taylor_interval_partial pp 1 ti);;
 540 *)