656 in (order p', new_vals, steps) end |
656 in (order p', new_vals, steps) end |
657 *} |
657 *} |
658 |
658 |
659 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
659 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
660 ML {* |
660 ML {* |
|
661 fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) |
|
662 |
661 (* naming of n, M, m, r, ... follows Winkler p. 95 |
663 (* naming of n, M, m, r, ... follows Winkler p. 95 |
662 n: amount of variables |
664 assumes: n = length es1 = length es2 |
663 r: *) |
665 r: *) |
664 fun gcd_poly' [(c1, es1)] [(c2, es2)] _ _ = [(Integer.gcd c1 c2, map2 Integer.min es1 es2)] |
666 fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] |
|
667 | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] |
665 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = |
668 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = |
666 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else |
669 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else |
667 if n > 1 |
670 if n > 1 |
668 then |
671 then |
669 let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); |
672 let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); |
675 uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* |
678 uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* |
676 (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b')))) |
679 (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b')))) |
677 end |
680 end |
678 |
681 |
679 (* fn: poly -> poly -> int -> |
682 (* fn: poly -> poly -> int -> |
680 int -> int -> int list -> poly list -> poly*) |
683 int -> int -> int list -> poly list -> poly |
|
684 assumes length a > 1 \<and> length b > 1 |
|
685 yields TODO |
|
686 *) |
681 and try_new_r a b n M r r_list steps = |
687 and try_new_r a b n M r r_list steps = |
682 let |
688 let |
683 val r = find_new_r a b r; |
689 val r = find_new_r a b r; |
684 val r_list = r_list @ [r]; |
690 val r_list = r_list @ [r]; |
685 val g_r = gcd_poly' (order (eval a (n - 2) r)) |
691 val g_r = gcd_poly' (order (eval a (n - 2) r)) |
686 (order (eval b (n - 2) r)) (n - 1) 0 |
692 (order (eval b (n - 2) r)) (n - 1) 0 |
687 val steps = steps @ [g_r]; |
693 val steps = steps @ [g_r]; |
688 in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end |
694 in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end |
689 (* fn: poly -> poly -> int -> |
695 (* fn: poly -> poly -> int -> |
690 int -> int -> int -> int list -> poly list -> |
696 int -> int -> int -> int list -> poly list -> |
691 | poly -> poly -> int list -> poly*) |
697 | poly -> poly -> int list -> poly |
|
698 assumes length a > 1 \<and> length b > 1 |
|
699 yields TODO |
|
700 *) |
692 and HENSEL_lifting a b n M m r r_list steps g g_n mult = |
701 and HENSEL_lifting a b n M m r r_list steps g g_n mult = |
693 if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else |
702 if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else |
694 try_new_r a b n M r r_list steps |
703 try_new_r a b n M r r_list steps |
695 else |
704 else |
696 let |
705 let |