-
Notifications
You must be signed in to change notification settings - Fork 32
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Adding Inverse Rules #1016
base: main
Are you sure you want to change the base?
Adding Inverse Rules #1016
Conversation
(when (flag-set? 'localize 'costs) | ||
#| (when (flag-set? 'localize 'costs) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why did you disable this?
(let loop ([prog prog] | ||
[loc loc]) | ||
(let loop ([prog prog] [loc loc]) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You gotta update your raco fmt
version. Run raco pkg update fmt
.
@@ -225,6 +235,13 @@ | |||
[difference-of-sqr--1 (+ (* a a) -1) (* (+ a 1) (- a 1))] | |||
[pow-sqr (* (pow a b) (pow a b)) (pow a (* 2 b))]) | |||
|
|||
(define-ruleset* difference-of-squares-canonicalize-revv |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(define-ruleset* difference-of-squares-canonicalize-revv | |
(define-ruleset* difference-of-squares-canonicalize-rev |
[difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)] | ||
[difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)] | ||
[difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))] | ||
[pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))]) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the pow-sqr-rev
rule true? Consider (pow -1 (* 2 1/2)) = (pow -1 1) = -1
but (* (pow -1 1/2) (pow -1 1/2))
is illegal because (pow -1 1/2)
does not exist.
; Specialized numerical functions | ||
; TODO: These are technically rules over impls | ||
; | ||
; (define-ruleset* special-numerical-reduce | ||
; (numerics simplify) | ||
; #:type ([x real] [y real] [z real]) | ||
; [log1p-expm1 (log1p (expm1 x)) x] | ||
; [hypot-1-def (sqrt (+ 1 (* y y))) (hypot 1 y)] | ||
; [fmm-def (- (* x y) z) (fma x y (neg z))] | ||
; [fmm-undef (fma x y (neg z)) (- (* x y) z)]) | ||
|
||
; (define-ruleset* special-numerical-expand | ||
; (numerics) | ||
; #:type ([x real] [y real]) | ||
; [log1p-expm1-u x (log1p (expm1 x))] | ||
; [expm1-log1p-u x (expm1 (log1p x))]) | ||
|
||
; (define-ruleset* numerics-papers | ||
; (numerics) | ||
; #:type ([a real] [b real] [c real] [d real]) | ||
; ; "Further Analysis of Kahan's Algorithm for | ||
; ; the Accurate Computation of 2x2 Determinants" | ||
; ; Jeannerod et al., Mathematics of Computation, 2013 | ||
; ; | ||
; ; a * b - c * d ===> fma(a, b, -(d * c)) + fma(-d, c, d * c) | ||
; [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))]) | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any reason to add this comment back?
(arithmetic sound) | ||
(arithmetic) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
?
(define-ruleset* log2-factor | ||
(exponents sound) | ||
#:type ([a real] [b real]) | ||
[log2-expand (log x 2) (/ (log x) (log 2))] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You want (log2 x)
not (log x 2)
.
[acos-cos-rev (fabs (remainder x (* 2 (PI)))) (acos (cos x))] | ||
[asin-sin-rev (- (fabs (remainder (+ x (/ (PI) 2)) (* 2 (PI)))) (/ (PI) 2)) (asin (sin x))] | ||
[atan-tan-rev (remainder x (PI)) (atan (tan x))]) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I really doubt that these rules help but I guess they probably don't hurt either.
[hang-m0-tan-rev (tan (/ (neg a) 2)) (/ (- 1 (cos a)) (neg (sin a)))] | ||
[hang-p0-tan-rev (tan (/ a 2)) (/ (- 1 (cos a)) (sin a))] | ||
[hang-0m-tan-rev (tan (/ (neg a) 2)) (/ (neg (sin a)) (+ 1 (cos a)))] | ||
[hang-0p-tan-rev (tan (/ a 2)) (/ (sin a) (+ 1 (cos a)))]) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suspect these aren't sound
|
||
(define-ruleset* trig-expand-sound | ||
(trigonometry sound) | ||
#:type ([x real] [y real] [a real] [b real]) | ||
[sin-sum (sin (+ x y)) (+ (* (sin x) (cos y)) (* (cos x) (sin y)))] | ||
[cos-sum (cos (+ x y)) (- (* (cos x) (cos y)) (* (sin x) (sin y)))] | ||
[cos-sum-rev (- (* (cos x) (cos y)) (* (sin x) (sin y))) (cos (+ x y))] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why isn't this in the block below?
Description:
This PR introduces the implementation of all inverse rules. The inverse rules allow the system to reverse operations in order to achieve a few goals. By adding inverse rules we hope to prove more expressions equal to one another so that they are in the same eclass. We also hope to further improve results as the quality of our rulesets improve with missing rules.
This pr has improved results overall but there are a few benchmarks that have gotten worse which is expected.