Editing Mathematical induction (section)

=== Prefix induction ===
The most common form of proof by mathematical induction requires proving in the induction step that
<math display="block">\forall k \, (P(k) \to P(k+1))</math>

whereupon the induction principle "automates" {{mvar|n}} applications of this step in getting from {{math|''P''(0)}} to {{math|''P''(''n'')}}. This could be called "predecessor induction" because each step proves something about a number from something about that number's predecessor.

A variant of interest in [[computational complexity]] is "prefix induction", in which one proves the following statement in the induction step:
<math display="block">\forall k\, (P(k) \to P(2k) \land P(2k+1))</math>
or equivalently
<math display="block">\forall k\, \left( P\!\left(\left\lfloor \frac{k}{2} \right\rfloor \right) \to P(k) \right)</math>

The induction principle then "automates" [[binary logarithm|log<sub>2</sub>]]&thinsp;''n'' applications of this inference in getting from {{math|''P''(0)}} to {{math|''P''(''n'')}}. In fact, it is called "prefix induction" because each step proves something about a number from something about the "prefix" of that number — as formed by truncating the low bit of its [[binary representation]]. It can also be viewed as an application of traditional induction on the length of that binary representation.

If traditional predecessor induction is interpreted computationally as an {{mvar|n}}-step loop, then prefix induction would correspond to a log-{{mvar|n}}-step loop. Because of that, proofs using prefix induction are "more feasibly constructive" than proofs using predecessor induction.

Predecessor induction can trivially simulate prefix induction on the same statement. Prefix induction can simulate predecessor induction, but only at the cost of making the statement more syntactically complex (adding a [[bounded quantifier|bounded]] [[universal quantifier]]), so the interesting results relating prefix induction to [[polynomial-time]] computation depend on excluding unbounded quantifiers entirely, and limiting the alternation of bounded universal and [[existential quantifier|existential]] quantifiers allowed in the statement.<ref name=Buss:BA>{{cite book | last=Buss|first=Samuel | title=Bounded Arithmetic | date=1986 | publisher=Bibliopolis | location=Naples}}</ref>

One can take the idea a step further: one must prove
<math display="block">\forall k \, \left( P\!\left( \left\lfloor \sqrt{k} \right\rfloor \right) \to P(k) \right)</math>
whereupon the induction principle "automates" {{math|log log ''n''}} applications of this inference in getting from {{math|''P''(0)}} to {{math|''P''(''n'')}}. This form of induction has been used, analogously, to study log-time parallel computation.{{citation needed|date=January 2018}}