1018 trace_rewrite:=false; |
1018 trace_rewrite:=false; |
1019 |
1019 |
1020 (*WN.17.3.03 =========================================================^^^---*) |
1020 (*WN.17.3.03 =========================================================^^^---*) |
1021 |
1021 |
1022 |
1022 |
|
1023 "----- SK060904-2a non-termination of add_fraction_p_"; |
1023 (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*) |
1024 (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*) |
1024 (*... takes uncredible much time:*) |
1025 (*... takes uncredible much time:*) |
1025 (* |
1026 (* |
1026 WN060831???SK6 |
1027 WN060831???SK6 |
|
1028 "----- SK060904-2a non-termination of add_fraction_p_"; |
1027 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)"; |
1029 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)"; |
1028 val None = rewrite_set_ thy false common_nominator_p t; |
1030 val None = rewrite_set_ thy false common_nominator_p t; |
1029 writeln |
1031 writeln |
1030 "----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\ |
1032 "----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\ |
1031 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\ |
1033 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\ |
1330 (*SK loops .. WN060420???MG5 not canceled to "1 / (4*c + 3*e)"*) |
1332 (*SK loops .. WN060420???MG5 not canceled to "1 / (4*c + 3*e)"*) |
1331 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1333 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1332 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1334 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1333 term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"; |
1335 term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"; |
1334 (*..WN060831 _with_ parentheses ...*) |
1336 (*..WN060831 _with_ parentheses ...*) |
|
1337 "----- SK060904-1b non-termination of cancel_p_"; |
1335 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
1338 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
1336 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
1339 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
1337 (* WN060831???SK8 |
1340 (* WN060831???SK8 |
1338 val Some (t',_) = rewrite_set_ thy false cancel_p t''; |
1341 val Some (t',_) = rewrite_set_ thy false cancel_p t''; |
1339 term2str t'; |
1342 term2str t'; |
1389 |
1392 |
1390 (*Schalk I, p.68 Nr. 440b *) |
1393 (*Schalk I, p.68 Nr. 440b *) |
1391 (* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831???SK11 |
1394 (* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831???SK11 |
1392 val t = str2term |
1395 val t = str2term |
1393 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)"; |
1396 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)"; |
1394 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1397 trace_rewrite := true; |
1395 term2str t; |
1398 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1396 if (term2str t) = |
1399 ### rls: cancel_p on: |
1397 |
1400 (-9 * (a ^ 3 * b) + -9 * (a ^ 2 * b ^ 2) + a ^ 5 * b + a ^ 4 * b ^ 2) / |
|
1401 (3 * (a ^ 3 * b) + -3 * (a * b ^ 3) + a ^ 4 * b + -1 * (a ^ 2 * b ^ 3)) |
|
1402 trace_rewrite := false; |
|
1403 term2str t; |
|
1404 if (term2str t) = |
1398 then () |
1405 then () |
1399 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27"; |
1406 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27"; |
1400 |
1407 |
1401 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))"; |
1408 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))"; |
1402 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1409 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1514 if (term2str t) = |
1521 if (term2str t) = |
1515 |
1522 |
1516 then () |
1523 then () |
1517 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37"; |
1524 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37"; |
1518 |
1525 |
1519 |
1526 "----- SK060904-1a non-termination of cancel_p_"; |
1520 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))"; |
1527 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))"; |
1521 val Some (t,_) = rewrite_set_ thy false make_polynomial t; |
1528 val Some (t,_) = rewrite_set_ thy false make_polynomial t; |
1522 term2str t; |
1529 term2str t; |
1523 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) / |
1530 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) / |
1524 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" |
1531 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" |
2092 |
2099 |
2093 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))"; |
2100 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))"; |
2094 val Some (t', _) = cancel_p_ thy t; term2str t'; |
2101 val Some (t', _) = cancel_p_ thy t; term2str t'; |
2095 (*???SK order ???*) |
2102 (*???SK order ???*) |
2096 |
2103 |
2097 "----- non-termination of cancel_p_ S"; |
2104 "----- SK060904-1a non-termination of cancel_p_"; |
2098 (*cancel_p_ does not terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) |
2105 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))"; |
2099 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))"; |
|
2100 val Some (t',_) = rewrite_set_ thy false norm_Poly t; |
2106 val Some (t',_) = rewrite_set_ thy false norm_Poly t; |
2101 term2str t' = |
2107 term2str t' = |
2102 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true*); |
2108 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true*); |
2103 (* cancel_p_ thy t'; |
2109 (* cancel_p_ thy t'; |
2104 *) |
2110 Warning - Increasing stack from 147456 to 294912 bytes |
2105 |
2111 Warning - Increasing stack from 294912 to 589824 bytes |
2106 val mmm = (3,[2,1,1]); |
2112 Warning - Increasing stack from 589824 to 1179648 bytes*) |
2107 mv_monom2str mmm; |
2113 |
2108 |
2114 "----- SK060904-1b non-termination of cancel_p_"; |
2109 val xxx = [(1,[1,0,0]),(2,[1,1,0]),(3,[2,1,1])]; |
2115 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
2110 mv_poly2str xxx; |
2116 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
|
2117 (* cancel_p_ thy t; |
|
2118 Warning - Increasing stack from 147456 to 294912 bytes |
|
2119 Warning - Increasing stack from 294912 to 589824 bytes |
|
2120 Warning - Increasing stack from 589824 to 1179648 bytes) |
|
2121 |
|
2122 |
|
2123 "----- SK060904-2a non-termination of add_fraction_p_"; |
|
2124 val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \ |
|
2125 \ (-1 * a + b * x) / (a + b * x) "; |
|
2126 (* |
|
2127 rewrite_set_ thy false common_nominator_p t; |
|
2128 |
|
2129 common_nominator_p_ thy t; |
|
2130 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \ |
|
2131 \ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) "; |
|
2132 |
|
2133 add_fraction_p_ thy t; |
|
2134 " ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\ |
|
2135 \ ((a + b * x)*(-1 * a + b * x)) "; |
|
2136 *) |