prog

frontpage - thread list - new thread - preferences - ?

Help on the Way

85 2022-06-25 14:09

>>82
Let X{t} be the value of the local variable X after t steps. Let X be the unmodified value passed to you from the outside. Initial conditions:

a{0} = 1, b{0} = b, n{0} = n

Invariant:

a{0} * b{0}^n{0} = b^n

Recall that when deconstructing a number into bits with parity or modulo 2 and right shift or quotient 2, you proceed from the LSB to the MSB. Keeping that in mind, the algorithm can be recovered from the invariant by the usual process of assuming you've already performed k steps correctly and you just need to perform step k+1. In other words you just need a state transformation:

(a{k}, b{k}, n{k}) --> (a{k+1}, b{k+1}, n{k+1})

The invariant assures you that:

a{k} * b{k}^n{k} = b^n

Therefore if n{k} = 0 then a{k} = b^n and you're done. Otherwise you're in this situation:

        n{k}
+-------------------+
|                   |
+---------------+   +-----------+
|bit bit bit bit|bit|bit bit bit| = n
+---------------+ ^ +-----------+
     n{k+1}       |     k bits
               current

The bit deconstruction equations can be read off the diagram:

n{k+1} = n{k} // 2   [eq1]
current = n{k} mod 2 = 0 or 1
2 * n{k+1} + current = n{k}
2 * (n{k} // 2) + (n{k} mod 2) = n{k}

where // stands for integer division. The next invariant that you must satisfy:

a{k} * b{k}^n{k} = b^n = a{k+1} * b{k+1}^n{k+1}

Use [eq1]:

a{k} * b{k}^n{k} = a{k+1} * b{k+1}^(n{k} // 2)

You need to account for the halving of the exponent to maintain the invariant. You can do so in either a{k+1} or b{k+1}. But a{k+1} has no exponent applied to it, so it would need to compensate with its own internal exponentiation using some dependence on n{k}. This would make the process recursive, but the exercise https://mitpress.mit.edu/sites/default/files/sicp/full-text/book/book-Z-H-11.html#%_thm_1.16 requires the process to be iterative. So you account for the halving of the exponent in b{k+1}. To account in a base for the halving of its exponent you square the base, as the exercise already suggests.

b{k+1} = b{k}^2   [eq2]

Plug it back into the invariant:

a{k} * b{k}^n{k} = a{k+1} * (b{k}^2)^(n{k} // 2)

To compute nested powers multiply the exponents.

a{k} * b{k}^n{k} = a{k+1} * b{k}^(2 * (n{k} // 2))

Use the [eq1] group to rewrite the exponent:

a{k} * b{k}^n{k} = a{k+1} * b{k}^(n{k} - (n{k} mod 2))

Simplify to get a{k+1}:

a{k+1} = a{k} * b{k}^(n{k} mod 2)

You don't need to actually exponentiate here because (n{k} mod 2) can only be 0 or 1.

a{k+1} = | a{k}        if (n{k} mod 2) = 0
         | a{k} * b{k} if (n{k} mod 2) = 1
                                             [eq3]
a{k+1} = | a{k}        if current bit = 0
         | a{k} * b{k} if current bit = 1

Together [eq1], [eq2] and [eq3] specify the state transformation. This sort of technique can be used in general to recover algorithms from invariants.

103