@@ -293,7 +293,7 @@ rewrites =
293293
294294 -- How can the binomial theorem be represented?
295295 -- Is it really only available for one integer at a time?
296- -- ++ [ powP ("a" + "b") (NonVariablePattern . Const $ fromIntegral n) := sum [(fromInteger $ n `_choose ` k) * powP "a" (fromInteger k) * powP "b" (fromInteger $ n - k) | k <- [0..n]] | n <- [2..1000]]
296+ -- ++ [ powP ("a" + "b") (NonVariablePattern . Const $ fromIntegral n) := sum [(fromInteger $ n `choose ` k) * powP "a" (fromInteger k) * powP "b" (fromInteger $ n - k) | k <- [0..n]] | n <- [2..1000]]
297297 ++
298298
299299 -- It's a bit unclear to me how to determine that high powers
@@ -306,6 +306,7 @@ rewrites =
306306
307307 , sinP 0 := 0
308308 , cosP 0 := 1
309+ , sinhP 0 := 0
309310 , coshP 0 := 1
310311 , snP 0 " k" := 0
311312 , cnP 0 " k" := 1
@@ -377,13 +378,15 @@ rewrites =
377378 -- Additional ad-hoc: because of negate representations?
378379 , " a" - (fromInteger (- 1 )* " b" ) := " a" + " b"
379380
380- ] where
381- n `_choose` k
382- | k < 0 || k > n = 0
383- | k == 0 || k == n = 1
384- | k == 1 || k == n - 1 = n
385- | 2 * k > n = n `_choose` (n - k)
386- | otherwise = (n - 1 ) `_choose` (k - 1 ) * n `div` k
381+ ]
382+
383+ choose :: Integral i => i -> i -> i
384+ n `choose` k
385+ | k < 0 || k > n = 0
386+ | k == 0 || k == n = 1
387+ | k == 1 || k == n - 1 = n
388+ | 2 * k > n = n `choose` (n - k)
389+ | otherwise = (n - 1 ) `choose` (k - 1 ) * n `div` k
387390
388391rewrite :: Fix Expr -> Fix Expr
389392rewrite e = fst $ equalitySaturation e rewrites symCost
@@ -481,11 +484,15 @@ symTests = testGroup "Jacobi"
481484 rewrite (_sin(" a" + " b" )) @?= _sin " a" * _cos " b" + _cos " a" * _sin " b"
482485
483486 -- TODO: More elliptic function identities may be worthwhile.
487+ -- This is just this expanded via the binomial theorem:
488+ -- _pow ((1 - _pow (_sn "x" "k") 2) / _pow "k" 2) 5 * _dn "x" "k"
484489 , testCase " reduce (dn(x,k))^11 in terms of sn(x,k)" $
485- fst (equalitySaturation' (defaultBackoffScheduler { banLength = 100 }) (_pow (_dn " x" " k" ) 11 ) rewrites depthCost ) @?= _pow (( 1 - _pow ( _sn " x" " k" ) 2 ) / _pow " k " 2 ) 5 * _dn " x" " k" -- this should actually not be equal
490+ fst (equalitySaturation' (defaultBackoffScheduler { banLength = 100 }) (_pow (_dn " x" " k" ) 11 ) rewrites symCost ) @?= _pow " k " ( - 10 ) * _dn " x " " k " - 5 * _pow " k " ( - 10 ) * _pow ( _sn " x" " k" ) 2 * _dn " x " " k " + 10 * _pow " k " ( - 10 ) * _pow (_sn " x " " k " ) 4 * _dn " x " " k " - 10 * _pow " k " ( - 10 ) * _pow (_sn " x " " k " ) 6 * _dn " x " " k " + 5 * _pow " k " ( - 10 ) * _pow (_sn " x " " k " ) 8 * _dn " x" " k" - _pow " k " 10 * _pow (_sn " x " " k " ) 10 * _dn " x " " k "
486491
492+ -- This is also expanded via the binomial theorem, programmatically.
493+ -- _pow ((1 - _pow (_sn "x" "k") 2) / _pow "k" 2) 500 * _dn "x" "k"
487494 , testCase " reduce (dn(x,k))^1001 in terms of sn(x,k)" $
488- rewrite (_pow (_dn " x" " k" ) 1001 ) @?= _pow (( 1 - _pow (_sn " x " " k " ) 2 ) / _pow " k" 2 ) 500 * _dn " x" " k"
495+ rewrite (_pow (_dn " x" " k" ) 1001 ) @?= sum [( fromInteger $ 500 `choose` m) * ( - 1 ) ^ m * _pow " k" ( - 1000 ) * _pow ( _dn " x" " k" ) ( 2 * fromInteger m) | m <- [ 0 .. 50 ]]
489496
490497 , testCase " cubic binomial (a+b)^3 = a^3 + 3*a^2*b + 3*a*b^2 + b^3" $
491498 rewrite (_pow (" a" + " b" ) 3 ) @?= _pow " a" 3 + fromInteger 3 * _pow " a" 2 * " b" + fromInteger 3 * " a" * _pow " b" 2 + _pow " b" 3
0 commit comments