2 needs "../formal_lp/arith/informal/informal_arith.hl";;
3 needs "../formal_lp/arith/informal/informal_eval_interval.hl";;
6 module Informal_taylor = struct
8 open Informal_interval;;
11 open Informal_eval_interval;;
23 type m_taylor_interval =
26 domain : m_cell_domain;
29 ddf : interval list list;
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;;
37 let float_inv2 = div_float_lo 1 float_1 float_2;;
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
48 (* mk_m_center_domain *)
49 let mk_m_center_domain pp x_list z_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
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)"
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};;
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
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};;
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
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
105 (* error_mul_f2_hi *)
106 let error_mul_f2_hi pp a int = mul_float_hi pp a (abs_interval int);;
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
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;;
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
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
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
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
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
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
156 mk_interval (lo, hi);;
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)
165 List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
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;;
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)
178 List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
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;;
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)
191 List.nth (List.nth ti.ddf (j - 1)) (i - 1)) (1--ti.n) in
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);;
201 let eval_m_taylor_add p_lin p_second taylor1 taylor2 =
202 let ( + ), ( ++ ) = add_interval p_lin, add_interval p_second in
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
213 let eval_m_taylor_sub p_lin p_second taylor1 taylor2 =
214 let ( - ), ( -- ) = sub_interval p_lin, sub_interval p_second in
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
225 let eval_m_taylor_mul p_lin p_second ti1 ti2 =
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
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
256 let eval_m_taylor_inv p_lin p_second ti =
259 let f1_bound = eval_m_taylor_bound p_second ti in
260 let bounds = inv_interval p_lin ti.f in
262 let neg, inv, ( * ) = neg_interval, inv_interval p_lin, mul_interval p_lin in
263 neg (inv (ti.f * ti.f)) in
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
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
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
287 let eval_m_taylor_sqrt p_lin p_second ti =
290 let f1_bound = eval_m_taylor_bound p_second ti in
291 let bounds = sqrt_interval p_lin ti.f in
293 let inv, ( * ) = inv_interval p_lin, mul_interval p_lin in
294 inv (two_interval * bounds) in
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
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
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
319 let eval_m_taylor_atn =
320 let neg_two_interval = neg_interval two_interval in
321 fun p_lin p_second ti ->
324 let f1_bound = eval_m_taylor_bound p_second ti in
325 let bounds = atn_interval p_lin ti.f in
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
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
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
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
354 let eval_m_taylor_acs p_lin p_second ti =
357 let f1_bound = eval_m_taylor_bound p_second ti in
358 let bounds = acs_interval p_lin ti.f in
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
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
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
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
393 open Informal_taylor;;
396 let f1, f2 = Informal_interval.dest_interval int in
397 Informal_float.dest_float f1, Informal_float.dest_float f2;;
400 dest_int ti.f, map dest_int ti.df, map (map dest_int) ti.ddf;;
402 let dest_f = Informal_float.dest_float;;
405 needs "../formal_lp/formal_interval/m_taylor_arith2.hl";;
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);;
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;;
419 let xx = `[#1.1; &2; -- sqrt(&2)]` and
420 zz = `[&3; &3; &1 + sqrt(&3)]`;;
422 let xx1 = convert_to_float_list pp true xx and
423 zz1 = convert_to_float_list pp false zz;;
425 let xx0 = Informal_taylor.convert_to_float_list pp true xx and
426 zz0 = Informal_taylor.convert_to_float_list pp false zz;;
428 let dom_th = mk_m_center_domain n pp xx1 zz1;;
429 let dom = Informal_taylor.mk_m_center_domain pp xx0 zz0;;
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);;
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;;
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;;
448 let ti_th = eval_taylor pp pp dom_th;;
449 let ti = taylor pp pp dom;;
452 eval_m_taylor_bound n pp ti_th;;
453 dest_int (Informal_taylor.eval_m_taylor_bound pp ti);;
455 eval_m_taylor_partial_upper n pp 3 ti_th;;
456 dest_f (Informal_taylor.eval_m_taylor_partial_upper pp 3 ti);;
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;;
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);;
465 let xx = `[#0.0; &0; sqrt(&0)]` and
466 zz = `[#0.2; #0.1; sqrt(&0) + #0.1]`;;
468 let xx1 = convert_to_float_list pp true xx and
469 zz1 = convert_to_float_list pp false zz;;
471 let xx0 = Informal_taylor.convert_to_float_list pp true xx and
472 zz0 = Informal_taylor.convert_to_float_list pp false zz;;
474 let dom_th = mk_m_center_domain n pp xx1 zz1;;
475 let dom = Informal_taylor.mk_m_center_domain pp xx0 zz0;;
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;;
484 eval_m_taylor_bound n 20 th;;
485 dest_int (Informal_taylor.eval_m_taylor_bound 20 t);;
487 eval_m_taylor_partial_bound n 20 2 th;;
488 dest_int (Informal_taylor.eval_m_taylor_partial_bound 20 2 t);;
490 eval_m_taylor_mul n pp pp ti_th th;;
491 dest_ti (Informal_taylor.eval_m_taylor_mul pp pp ti t);;
495 test 100 eval_taylor dom_th;;
497 test 100 taylor dom;;
500 eval_m_taylor_bound n pp ti_th;;
501 dest_int (Informal_taylor.eval_m_taylor_bound pp ti);;
503 eval_m_taylor_upper_bound n pp ti_th;;
504 dest_f (Informal_taylor.eval_m_taylor_upper_bound pp ti);;
506 eval_m_taylor_lower_bound n pp ti_th;;
507 dest_f (Informal_taylor.eval_m_taylor_lower_bound pp ti);;
511 test 100 (eval_m_taylor_bound n pp) ti_th;;
513 test 100 (Informal_taylor.eval_m_taylor_bound pp) ti;;
519 eval_m_taylor_upper_partial n pp 1 ti_th;;
520 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 1 ti);;
522 eval_m_taylor_upper_partial n pp 2 ti_th;;
523 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 2 ti);;
525 eval_m_taylor_upper_partial n pp 3 ti_th;;
526 dest_f (Informal_taylor.eval_m_taylor_upper_partial pp 3 ti);;
529 eval_m_taylor_lower_partial n pp 1 ti_th;;
530 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 1 ti);;
532 eval_m_taylor_lower_partial n pp 2 ti_th;;
533 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 2 ti);;
535 eval_m_taylor_lower_partial n pp 3 ti_th;;
536 dest_f (Informal_taylor.eval_m_taylor_lower_partial pp 3 ti);;
538 eval_m_taylor_interval_partial n pp 1 ti_th;;
539 dest_int (Informal_taylor.eval_m_taylor_interval_partial pp 1 ti);;