Recursive definitions and structural induction

Consider fully parenthesized expressions built from one symbol x using a binary plus constructor. First declare x an expression. Next, whenever A and B are expressions, declare the parenthesized object (A + B) an expression. Finally, the collection contains only objects obtainable by finitely many uses of these rules. That last clause excludes unexplained objects and infinitely descending constructions. The syntax concerns written trees; it does not identify two expressions merely because their numerical evaluations might agree.

A recursive function on these expressions needs a value for the base symbol and a rule that computes the value at a compound expression from values at its immediate subexpressions. For example, leaf count assigns one to x and adds the counts of the two children. This is well founded because each child is a strictly smaller finite syntax tree. If the notation allowed more than one parse, the proposed definition would require an additional argument that the result is independent of the parse.

Structural induction proves a claim first for each base object and then for each constructor under the assumption that it already holds for the constructor’s immediate inputs. For our grammar there is one base case and one binary case. The two child expressions can have very different sizes, so ordinary predecessor induction would obscure the construction. The structural hypotheses are exactly the claims about A and B needed to handle (A + B).

To prove that a full binary expression has one more leaf than plus symbol, define another recursive function counting plus symbols. The base has one leaf and zero plus symbols. In the compound case, leaf counts add, while plus counts add and gain one for the new root. Substituting the two child hypotheses yields the desired difference. This argument covers every finite shape produced by the grammar, including highly unbalanced trees, without assuming that both children have equal depth.

Changing the constructors can change the invariant. If a unary negation constructor is added, counting every operation as an internal node no longer makes leaves equal internal nodes plus one: the expression −x already violates that revised claim. A corrected invariant could count only binary constructors, or use a general relation between nodes and outgoing edges. Always reread the grammar after extending a language; a proof that omits the new constructor no longer establishes a universal statement about the expanded collection.

Distinguish structural induction from evaluating a few example trees and from induction on an arbitrary integer label attached to them. A size-based proof can work, but it must show that every recursive input has smaller size and that every object of the next size is covered. Structural induction makes those obligations explicit through the construction rules. It also explains reliable recursive programs: each clause should match a constructor, and each recursive call should be on an input justified by that constructor.