8 Conjectures
Say you have a language and you have defined some functions on the language:
(define-language Shapes (s (square x y r) (overlay s s)) ((x y r) number) ; for the results (t (rectangle x y x y)) ; determine the area of a shape (define-metafunction Shapes ; we leave off the optional contract because there is no specification for the domain [(area (rectangle x_min x_max y_min y_max)) ,(* (- (term x_max) (term x_min)) (- (term y_max) (term y_min)))] [(area (square x y r)) ,(* (term r) (term r))] [(area (overlay s_top s_bot)) ,(+ (term (area s_top)) (term (area s_bot)))]) ; compute the bounding rectangle of a shape (define-metafunction Shapes bb : s -> t [(bb (square x y r)) (rectangle x ,(+ (term x) (term r)) ,(- (term y) (term r)) y)] [(bb (overlay s_top s_bot)) (bb-aux (bb s_top) (bb s_bot))]) ; auxiliary function: (define-metafunction Shapes bb-aux : t t -> t [(bb-aux (rectangle x_min1 x_max1 y_min1 y_max1) (rectangle x_min2 x_max2 y_min2 y_max2)) (rectangle ,(min (term x_min1) (term x_min2)) ,(max (term x_max1) (term x_max2)) ,(min (term y_min1) (term y_min2)) ,(max (term y_max1) (term y_max2)))]))
You can experiment with these functions:
> (term (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3)))) '(rectangle -7.2 4.1 -5.0 2.7)
> (term (area (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3))))) 87.01
> (term (area (square 1.1 2.7 3))) 9
> (term (area (square -7.2 -2.0 3))) 9
From experiments such as these and/or inspiration, you may come up with
conjectures such as
the area of the bounding area of some shape s is always larger than the area of the s
in English or, with Redex,
(> (area (bb s)) (area s))
It turns out that Redex comes with a random testing tool that can
help you check such conjectures:
> (redex-check Shapes s (> (term (area (bb s))) (term (area s))))
redex-check: counterexample found after 1 attempt:
(square 0 0 0)
The redex-check facility generates examples of s with
respect to language Shapes and checks whether the
conjecture—
> (redex-check Shapes s (>= (term (area (bb s))) (term (area s))))
redex-check: counterexample found after 7 attempts:
(square 0 0+inf.0i 0+inf.0i)
But again, redex-check finds a counter-example. This time, the
counter-example consists of a combination of two squares that
overlap. While the area of the bounding box is just the area of the
surrounding rectangle, the area function computes the area of an
overlay construction as the sum of the two.
Draw the situation on a grid to figure out why the conjecture fails.
To fix the conjecture, we need to change the area
function. Specifically, we need to subtract the overlap between the two
shapes:
meaning we also need to define the intersection function.
In short, before you try to prove conjectures it is often helpful to have them checked so that minor typos or real misunderstandings are eliminated before you invest effort in a full-fledged proof.