From: Thomas Walker Lynch
- Define the refer to the maximum index for accessing a component of a vector, the extent is often denoted as . Performing extensions to calculate the function value at call will make use of the initial tape up to index , or as many nonzero values as are available up to that extent. + Let the refer to the maximum index for accessing a component of a vector; the extent is often denoted as . Performing extensions to calculate the function value at call will make use of the initial tape up to index , or as many nonzero values as are available up to that extent.
- This can be proven by induction on the step index, . + To make this precise, let us define the at call as . The components of this vector are , where is the maximum available difference. The first component, , is the function value itself. The component is the first difference, and so on. +
+ ++ The extension operation follows a simple recurrence relation for any component : .
- Base Case (k=0): To generate the value at index 0, , the machine performs zero extensions. It requires the initial tape to have an extent of at least 0, accessing only the value at index 0, which is the function value itself. + We can now prove by induction on the call index that computing requires exactly the components through from the initial tape .
- Inductive Hypothesis: Assume that generating the value at step index requires the initial tape to have an extent of , consuming indices 0 through : . + Base Case (k=0): To generate the value at call 0, , the machine performs zero extensions. It accesses only the value at index 0 of the initial tape. The required extent is 0.
- Inductive Step: Consider the requirement for the value at step index . By the definition of the forward difference, . + Inductive Hypothesis: Assume that generating the value at call , which is , requires the initial tape components through . +
+ ++ Inductive Step: Consider the requirement for the value at call , which is . By the extension rule, .
- The union of the dependencies for and spans from index 0 to index . Thus, generating the value at step index requires the initial tape to have an extent of exactly . The lemma holds. + The union of the dependencies for and spans from index 0 to index . Thus, generating the value at call requires the initial tape to have an extent of exactly . The lemma holds.
- Consequently, on a finite tape with no constant difference, each extension reduces the extent of the logical state by one. If a programmer intends to call the extension function to reach step index 4, the initial tape must have an extent of 4, meaning it holds 5 values. The first result tape will have an extent of 3, the second an extent of 2, the third an extent of 1, and the final call will leave an extent of 0: the requested answer. + This proof applies regardless of whether the finite difference table is infinitely deep or truncated. If a person evaluates a tenth degree polynomial but only programs the machine to perform two calls, the initial tape only needs an extent of 2, utilizing components 0, 1, and 2. Each extension consumes one cell of state. If a programmer intends to execute the extension function to reach call , the initial tape must have an extent of , meaning it holds values.
- -