For a hash tree defined recursively over data blocks, how do you prove a property of every such tree without an integer n?

Most claims worth proving about a recursively built structure are not naturally claims about a number. Forcing them into "induct on n" is what makes people stall on unbalanced trees; inducting on the definition itself is both easier and more honest. ## Induction without a number A recursive data definition names a finite set of **constructors**, each taking zero or more values of the same type. A hash tree over data blocks has two: - `Leaf(block)` - a base constructor, taking no subtree; - `Node(left, right)` - a combining constructor, taking two. The ordering that makes induction sound is "is an immediate subterm of". Every value is built by finitely many constructor applications from base constructors, so no chain of subterms descends forever. That is exactly the well-foundedness ordinary induction gets from the integers, and it is all induction ever needs. ## One obligation per constructor To prove property `Q` of every tree: 1. **Leaf case.** Prove `Q(Leaf(b))` directly. No hypothesis exists here - this is the base case, and skipping it as obvious is the most common omission. 2. **Node case.** Assume `Q(left)` and `Q(right)`, then derive `Q(Node(left, right))`. Nothing else is required. There is no "and now for trees of height h + 1" - height never appears. ## A worked claim Take `internal(t) = leaves(t) - 1`, a fact a reviewer might want before trusting a node-count or memory estimate. - **Leaf:** `internal = 0`, `leaves = 1`, and `0 = 1 - 1`. Holds. - **Node:** the hypothesis gives `internal(l) = leaves(l) - 1` and `internal(r) = leaves(r) - 1`. Then `internal(Node(l, r)) = internal(l) + internal(r) + 1 = (leaves(l) - 1) + (leaves(r) - 1) + 1 = leaves(l) + leaves(r) - 1 = leaves(Node(l, r)) - 1`. Holds. Two lines of arithmetic, and it covers every shape - a spine of depth 1000 and a perfectly balanced tree alike. An induction on "the number of blocks" would have needed the strong hypothesis and a paragraph about how the split falls. ## How far the hypothesis reaches The plain form gives you the property at the **immediate** subterms only. Some arguments need it at every descendant - that is the strong version over the same subterm ordering, and it is sound for the same reason, because the ordering is well-founded no matter how many levels down you look. Choose the weaker one when it suffices; it makes the proof shorter to re-check when the definition changes. ## What structural induction does and does not license | Claim about a hash tree | Provable this way? | |---|---| | Internal nodes number one fewer than the leaves | Yes - one case per constructor, shown above | | The set of blocks under a node is the union of its children's | Yes - the definition of `blocks` is itself structural | | The root digest is determined by the block contents alone | **No** - it is false; the shape participates | | Every tree over n blocks has height about log n | No - false for lopsided trees; needs a balancing invariant | The third row is the one that bites. Because an internal digest is computed over its children's digests, two trees holding the same blocks in the same order under different groupings produce different root digests (barring a hash collision). Structural induction will happily prove the *true* version - that a root digest is a function of the subtree's block sequence **and** its shape - and will fail to prove the false one, which is the behaviour you want from a proof technique. ## Where the technique stops working Soundness rests on "every value is finitely built". Two situations break that: - **Cyclic structures.** If a node can point back to an ancestor, "is an immediate subterm of" is no longer well-founded and the argument is worthless. Graph claims need a different measure, such as an explicitly shrinking set of unvisited vertices. - **Unbounded, lazily generated structures.** A definition that admits infinite values has no base to stand on, and properties of it need a different principle entirely. In an interview, the move that reads as senior is not reciting the schema but choosing it: "this claim has no natural n and the tree is not balanced, so I would induct on the definition - leaf case, node case, hypothesis on both children" - and then admitting which claims the technique cannot reach.