vd: termination arguments.

.gitignore

@@ -1,4 +1,5 @@
 # Let's ignore some junk, backup and temporary test files.
+*.rkt~
 \#devel.dr.rkt#2#
 \#devel.rkt#
 .#devel.rkt

09a-fractals/vd02-termination-args.rkt

@@ -0,0 +1,96 @@
+#lang htdp/isl
+(require 2htdp/image)
+
+(define CUTOFF 2)
+
+;
+; Three part termination argument.
+; --------------------------------
+;
+; Base case:
+;
+;   (<= s CUTOFF)
+;
+;
+; Reduction step:
+;
+;   (/ s 2)
+;
+;
+; Argument that repeated application of reduction step will eventually
+; reach the base case:
+;
+;   As long as the cutoff is > 0 and s starts >= 0, repeated division
+;   by 2 will eventually be less than cutoff.
+;
+
+
+;; Number -> Image
+;; Produce a Sierpinski Triangle of given size.
+(check-expect (stri CUTOFF) (triangle CUTOFF "outline" "red"))
+(check-expect (stri (* CUTOFF 2))
+              (overlay (triangle (* 2 CUTOFF) "outline" "red")
+                       (local [(define sub1 (triangle CUTOFF "outline" "red"))]
+                         (above sub1
+                                (beside sub1 sub1)))))
+
+(define (stri s)
+  (cond [(<= s CUTOFF) (triangle s "outline" "red")]
+        [else
+         (overlay (triangle s "outline" "red")
+                  (local [(define sub (stri (/ s 2)))]
+                    (above sub
+                           (beside sub sub))))]))
+
+
+;; Natural -> Image
+;; Produce box with white box inside.
+
+;; Test the TRIVIAL case.
+(check-expect (scarp CUTOFF) (square CUTOFF "outline" "red"))
+
+;; Test the case where it is "1" bigger than the cut-off point.
+;; There will be one recursion here.
+(check-expect (scarp (* CUTOFF 3))
+              (overlay (square (* CUTOFF 3) "outline" "red")
+                       (local [(define sub (square CUTOFF "outline" "red"))
+                               (define blk (square CUTOFF "solid" "white"))]
+                         (above (beside sub sub sub)
+                                (beside sub blk sub)
+                                (beside sub sub sub)))))
+
+
+;
+; THREE PART TERMINATION ARGUMENT FOR SCARPET
+; -------------------------------------------
+;
+; Base case:
+;
+;   (<= s CUTOFF)
+;
+;
+; Reduction step:
+;
+;   (/ s 3)
+;
+;
+; Argument that repeated application of reduction step will eventually
+; reach the base case:
+;
+;   As long as the cutoff is > 0 and s starts >= 0, repeated division
+;   by 3s will eventually be less than cutoff.
+;
+
+
+
+;; Correct solution. Compare with the incorrect one.
+(define (scarp s)
+  (cond [(<= s CUTOFF) (square s "outline" "red")]
+        [else
+         (overlay (square s "outline" "red")
+                  (local [(define sub (scarp (/ s 3)))
+                          (define blk (square (/ s 3) "solid" "white"))]
+                    (above (beside sub sub sub)
+                           (beside sub blk sub)
+                           (beside sub sub sub))))]))
+

09a-fractals/vd03-hailstone-termination-arg.rkt

@@ -0,0 +1,64 @@
+#lang htdp/isl
+
+;
+;; The Collatz conjecture is a conjecture in mathematics named
+;; after Lothar Collatz, who first proposed it in 1937. ...
+;; The sequence of numbers involved is referred to as the hailstone
+;; sequence or hailstone numbers (because the values are usually
+;; subject to multiple descents and ascents like hailstones in a
+;; cloud).
+;;
+;; f(n) = /   n/2     if n is even
+;;        \   3n + 1  if n is odd
+;;
+;;
+;; The Collatz conjecture is: This process will eventually reach
+;; the number 1, regardless of which positive integer is chosen
+;; initially.
+;;
+;;  https://en.wikipedia.org/wiki/Collatz_conjecture
+;
+
+;; Integer[>=1] -> (listof Integer[>=1])
+;; produce hailstone sequence for n
+(check-expect (hailstones 1) (list 1))
+(check-expect (hailstones 2) (list 2 1))
+(check-expect (hailstones 4) (list 4 2 1))
+(check-expect (hailstones 5) (list 5 16 8 4 2 1))
+
+(define (hailstones n)
+  (if (= n 1)
+      (list 1)
+      (cons n
+            (if (even? n)
+                (hailstones (/ n 2))
+                (hailstones (add1 (* n 3)))))))
+
+
+;
+; PROBLEM:
+;
+; The stri, scarpet and hailstones functions use generative recursion. So
+; they are NOT based on a well-formed self-referential type comment. How do
+; we know they are going terminate? That is, how do we know every recursion
+; will definitely stop?
+;
+; Construct a three part termination argument for stri.
+;
+; Base case:
+;
+;   (= n 1)
+;
+;
+; Reduction step:
+;
+;   if n is even    (/ n 2)
+;   if n is odd     (add1 (* n 3))
+;
+;
+; Argument that repeated application of reduction step will eventually
+; reach the base case:
+;
+;   THIS IS A TRICKY PROBLEM!
+;
+