Structural induction is a proof method that is used in mathematical logic (e.g., the proof of Los' theorem), computer science, graph theory, and some other mathematical fields.
A D V E R T I S E M E N T
It is a generalization of mathematical induction. Structural recursion is a recursion method bearing the same relationship to structural induction as ordinary recursion bears to ordinary mathematical induction.
In general, the idea is that one wishes to prove some proposition P(x), where x is any instance of some sort of recursively-defined structure such as lists or trees. A well-founded partial order is defined on the structures. The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure S, then it must hold for S also. (Formally speaking, this then satisfies the premises of an axiom of well-founded induction, which asserts that these two conditions are sufficient for the proposition to hold for all x.)
A structurally recursive function uses the same idea to define a recursive function: "base cases" handle each minimal structure and a rule for recursion. Structural recursion is usually proved correct by structural induction; in particularly easy cases, the inductive step is often left out. The length and ++ functions in the example below are structurally recursive.
For example, if the structures are lists, one usually introduces the partial order in which L < M whenever list L is the tail of list M. Under this ordering, the empty list [] is the unique minimal element. A structural induction proof of some proposition P(l) then consists of two parts: A proof that P([]) is true, and a proof that if P(L) is true for some list L, and if L is the tail of list M, then P(M) must also be true.
USER(33): (list-length '(2 3 5 7 11 13 17 19))
8
Let us try to see how such a function can be implemented recursively. A given
list L is created by either one of the two constructors, namely nil
or a cons:
Case 1: L is nil.
The length of an empty list is zero.
Case 2: L is constructed by cons.
Then L is composed of two parts, namely, (first L)
and (rest L). In such case, the length of L can
be obtained inductively by adding 1 to the length of (rest L).
Formally, we could implement our own version of list-length as
follows:
(defun recursive-list-length (L)
"A recursive implementation of list-length."
(if (null L)
0
(1+ (recursive-list-length (rest L)))))
Here, we use the recognizer null to differentiate how L is
constructed. In case L is nil, we return 0 as its length.
Otherwise, L is a cons, and we return 1 plus the length of
(rest L). Recall that (1+ n) is simply a
shorthand for (+ n 1).
Again, it is instructive to use the trace facilities to examine the unfolding
of recursive invocations:
USER(40): (trace recursive-list-length)
(RECURSIVE-LIST-LENGTH)
USER(41): (recursive-list-length '(2 3 5 7 11 13 17 19))
0: (RECURSIVE-LIST-LENGTH (2 3 5 7 11 13 17 19))
v
1: (RECURSIVE-LIST-LENGTH (3 5 7 11 13 17 19))
2: (RECURSIVE-LIST-LENGTH (5 7 11 13 17 19))
3: (RECURSIVE-LIST-LENGTH (7 11 13 17 19))
4: (RECURSIVE-LIST-LENGTH (11 13 17 19))
5: (RECURSIVE-LIST-LENGTH (13 17 19))
6: (RECURSIVE-LIST-LENGTH (17 19))
7: (RECURSIVE-LIST-LENGTH (19))
8: (RECURSIVE-LIST-LENGTH NIL)
8: returned 0
7: returned 1
6: returned 2
5: returned 3
4: returned 4
3: returned 5
2: returned 6
1: returned 7
0: returned 8
8
The kind of recursion we see here is called structural recursion.
Its standard pattern is as follows. To process an instance X of a
recursive data type:
Use the recognizers to determine how X is created (i.e. which
constructor creates it). In our example, we use null to decide if a
list is created by nil or cons.
For instances that are atomic (i.e. those created by constructors with
no components), return a trivial value. For example, in the case when a list
is nil, we return zero as its length.
If the instance is composite, then use the selectors to extract its
components. In our example, we use first and rest to
extract the two components of a nonempty list.
Following that, we apply recursion on one or more components of X.
For instance, we recusively invoked recursive-list-length on
(rest L).
Finally, we use either the constructors or some other functions to
combine the result of the recursive calls, yielding the value of the
function. In the case of recursive-list-length, we return one plus
the result of the recursive call.
Sometimes, long traces like the one for list-length may be difficult to read
on a terminal screen. Common LISP allows you to capture screen I/O into a file
so that you can, for example, produce a hard copy for more comfortable reading.
To capture the trace of executing (recursive-list-length '(2 3 5 7 11 13 17
19)), we use the dribble command:
The form (dribble "output.txt") instructs Common LISP to begin
capturing all terminal I/O into a file called output.txt. The trailing
(dribble) form instructs Common LISP to stop I/O capturing, and closes
the file output.txt. If we examine output.txt, we will see the
following:
