1.6. Differentiation theorems 123 For this, we argue as follows. Take any ball Bi in the original collection. Because the algorithm only halts when there are no more balls that are disjoint from the B1,...,Bm, the ball Bi must intersect at least one of the balls Bj in the subcollection. Let Bj be the first ball with this property, thus Bi is disjoint from B1,...,Bj−1, but intersects Bj. Because Bj was chosen to be the largest amongst all balls that did not intersect B1,...,Bj−1, we conclude that the radius of Bi cannot exceed that of Bj. From the triangle inequality, this implies that Bi 3Bj, and the claim follows. Exercise 1.6.18. Technically speaking, the above algorithmic argument was not phrased in the standard language of formal mathematical deduction, because in that language, any mathematical object (such as the natural number m) can only be defined once, and not redefined multiple times as is done in most algorithms. Rewrite the above argument in a way that avoids redefining any variable. (Hint: Introduce a “time” variable t, and recursively construct families B1,t,...,Bmt,t of balls that represent the outcome of the above algorithm after t iterations (or t∗ iterations, if the algorithm halted at some previous time t∗ t). For this particular algorithm, there are also more ad hoc approaches that exploit the relatively simple nature of the algorithm to allow for a less notationally complicated construction.) More generally, it is possible to use this time parameter trick to convert any construction involving a provably terminating algorithm into a construction that does not redefine any variable. (It is, however, dangerous to work with any algorithm
Previous Page Next Page