Next: Rewrites Answer 5, Previous: Rewrites Answer 3, Up: Answers to Exercises

#### 3.7.55 Rewrites Tutorial Exercise 4

Here is a suitable set of rules to solve the first part of the problem:

         [ seq(n, c) := seq(n/2,  c+1) :: n%2 = 0,
           seq(n, c) := seq(3n+1, c+1) :: n%2 = 1 :: n > 1 ]

Given the initial formula ‘`seq(6, 0)`’, application of these rules produces the following sequence of formulas:

         seq( 3, 1)
         seq(10, 2)
         seq( 5, 3)
         seq(16, 4)
         seq( 8, 5)
         seq( 4, 6)
         seq( 2, 7)
         seq( 1, 8)

whereupon neither of the rules match, and rewriting stops.

We can pretty this up a bit with a couple more rules:

         [ seq(n) := seq(n, 0),
           seq(1, c) := c,
           ... ]

Now, given ‘`seq(6)`’ as the starting configuration, we get 8 as the result.

The change to return a vector is quite simple:

         [ seq(n) := seq(n, []) :: integer(n) :: n > 0,
           seq(1, v) := v | 1,
           seq(n, v) := seq(n/2,  v | n) :: n%2 = 0,
           seq(n, v) := seq(3n+1, v | n) :: n%2 = 1 ]

Given ‘`seq(6)`’, the result is ‘`[6, 3, 10, 5, 16, 8, 4, 2, 1]`’.

Notice that the ‘`n > 1`’ guard is no longer necessary on the last rule since the ‘`n = 1`’ case is now detected by another rule. But a guard has been added to the initial rule to make sure the initial value is suitable before the computation begins.

While still a good idea, this guard is not as vitally important as it was for the `fib` function, since calling, say, ‘`seq(x, [])`’ will not get into an infinite loop. Calc will not be able to prove the symbol ‘`x`’ is either even or odd, so none of the rules will apply and the rewrites will stop right away.