Info Catalog calc: Rewrites Answer 3 calc: Answers to Exercises calc: Rewrites Answer 5

calc: Rewrites Answer 4

 
 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.
 

Info Catalog calc: Rewrites Answer 3 calc: Answers to Exercises calc: Rewrites Answer 5