Substructure

From CS2800 wiki

Given an element [math]x [/math] of an inductively defined set [math]X [/math], a substructure [math]x' [/math] of [math]x [/math] is one of the "smaller" elements of [math]X [/math] that was used when creating [math]x [/math].

Substructures are important, because they tell you what inductive assumptions you can make when proving [math]P(x) [/math] in a proof by structural induction, and also what recursive uses of [math]f [/math] you can use when defining [math]f(x) [/math] in an inductively defined function.

You can identify the substructures of [math]x [/math] by looking at the rule defining [math]x [/math]: each of the uses of the variable from [math]X [/math] in the rule indicates a substructure. For example, if [math]x \href{/cs2800/wiki/index.php/%5Cin}{\in} \href{/cs2800/wiki/index.php/Natural_number}{\mathbb{N}} = \href{/cs2800/wiki/index.php/S}{S}~(\href{/cs2800/wiki/index.php/S}{S}~\href{/cs2800/wiki/index.php/Z}{Z}) [/math], then the only substructure of [math]x [/math] is [math]\href{/cs2800/wiki/index.php/S}{S}~\href{/cs2800/wiki/index.php/Z}{Z} [/math]; you can see this because [math]x [/math] was constructed using the rule [math]n \href{/cs2800/wiki/index.php/%5Cin}{\in} \href{/cs2800/wiki/index.php/Natural_number}{\mathbb{N}} \href{/cs2800/wiki/index.php/BNF}{::=} \cdots \href{/cs2800/wiki/index.php/%5Cmid}{\mid} S~n [/math]; this rule has a reuse of the variable [math]n [/math] from the LHS, so the corresponding part of [math]x [/math] is a substructure.

In the binary tree example, if [math]t \href{/cs2800/wiki/index.php/%5Cin}{\in} T \href{/cs2800/wiki/index.php/BNF}{::=} nil \href{/cs2800/wiki/index.php/%5Cmid}{\mid} tree(a,t_1,t_2) [/math], there are no substructures of [math]nil [/math], and the substructures of [math]tree(a,t_1,t_2) [/math] are [math]t_1 [/math] and [math]t_2 [/math], since these reuse the variable [math]t [/math] from the LHS.