On Mon, May 8, 2017 at 3:05 AM, Matthias Felleisen <matth...@ccs.neu.edu>
wrote:
>
> Measure with outer contract and remove the inner define/tight. If you
> wrote this algorithm with a loop in Eiffel, instead of a tail-recursive
> function, you wouldn’t check the invariant for every loop iteration either
>
>
Fair comment.
[In Eiffel I'd need to use a check condition in my loop. Below I explore
the moral equivalent of raising an error in Racket, which seems to work
well enough.]
I've removed the offending post-condition and redone the timings. (Code at
end)
*No contracts*
cpu time: 13 real time: 13 gc time: 0
*Outer contract only*
cpu time: 48 real time: 48 gc time: 0
*Outer contract + inner exception check*
cpu time: 63 real time: 73 gc time: 15
*Outer + tight inner contract*
cpu time: 1251 real time: 1268 gc time: 27
The virtue of the inner contract is that it catches non-terminating cases
during development.
E.g. In the recursive call (S (* 0.5 (+ estimate (/ x estimate)))) if we
replace / with * the "tight" contract catches it by imposing a bounds
check.
*Note*: I haven't reintroduced the more stringent requirement that the
error reduces with every iteration (monotonic convergence).
*Take-away*
The timings suggest that applying the contract system is a particularly
expensive way to achieve this level of safety. The outer contract + inner
exception check is a much more affordable alternative.
This example isn't enough to really explore the question of whether it
makes sense to later turn off the inner checks, once confidence has been
achieved. Personally, I'd say "it depends" on how slow we're going and
whether it makes a difference and what cheaper checks are available.
YMMV
Dan
#lang racket
(define-syntax-rule (define/tight (fn args ...)
ctc
body ...)
(begin
(define (fn args ...) (fn/impl args ...))
(with-contract fn
([fn/impl ctc])
#:freevar fn ctc
(define (fn/impl args ...)
body ...))))
(define-syntax-rule (implies a b)
(or (not a) b))
(define (default-eps) 1e-14)
(define (sqrt-error x estimate)
(-> (>/c 0) (>/c 0) (>=/c 0))
(abs (- 1 (/ (sqr estimate) x))))
(define/contract (real-sqrt x [eps (default-eps)])
(->i ([x (>=/c 0)])
([eps (>/c 0)])
[result (>=/c 0)]
#:post (x result)
(implies (= x 0) (= result 0))
#:post (x eps result)
(let ([EPS (if (unsupplied-arg? eps)
(default-eps)
eps)])
(implies (> x 0) (< (sqrt-error x result) EPS))))
(define/tight (S estimate)
(->i ([estimate (and (>/c 0) (<=/c (max 1 x)))])
[result (>/c 0)])
(if (< (sqrt-error x estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))
(if (zero? x)
0
(S (* 0.5 (+ 1 x)))))
(define/contract (real-sqrt-moderate x [eps (default-eps)])
(->i ([x (>=/c 0)])
([eps (>/c 0)])
[result (>=/c 0)]
#:post (x result)
(implies (= x 0) (= result 0))
#:post (x eps result)
(let ([EPS (if (unsupplied-arg? eps)
(default-eps)
eps)])
(implies (> x 0) (< (sqrt-error x result) EPS))))
(define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x))))
(define (S estimate)
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))
(if (zero? x)
0
(S (* 0.5 (+ 1 x)))))
(define/contract (real-sqrt-modified x [eps (default-eps)])
(->i ([x (>=/c 0)])
([eps (>/c 0)])
[result (>=/c 0)]
#:post (x result)
(implies (= x 0) (= result 0))
#:post (x eps result)
(let ([EPS (if (unsupplied-arg? eps)
(default-eps)
eps)])
(implies (> x 0) (< (sqrt-error x result) EPS))))
(define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x))))
(define (S estimate)
(unless (<= 0 estimate (max 1 x))
(raise-arguments-error 'real-sqrt-modified "Broken bounds"
"estimate" estimate
"x" x))
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))
(if (zero? x)
0
(S (* 0.5 (+ 1 x)))))
(define (real-sqrt-fast x [eps (default-eps)])
(define (sqrt-error estimate)
(abs (- 1 (/ (sqr estimate) x))))
(define (S estimate)
(if (< (sqrt-error estimate) eps)
estimate
(S (* 0.5 (+ estimate (/ x estimate))))))
(if (zero? x)
0
(S (* 0.5 (+ 1 x)))))
(displayln "No contracts")
(time
(for ([i (in-range 5000)])
(real-sqrt-fast i)))
(newline)
(displayln "Outer contract only")
(time
(for ([i (in-range 5000)])
(real-sqrt-moderate i)))
(newline)
(displayln "Outer contract + inner exception check")
(time
(for ([i (in-range 5000)])
(real-sqrt-modified i)))
(newline)
(displayln "Outer contract + tight inner contract")
(time
(for ([i (in-range 5000)])
(real-sqrt i)))
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
