Define recursive functions and strengthen the claim that proves them

Try

Imagine reflecting a branching diagram in a vertical mirror. Every left child becomes a right child, including children deep inside the diagram. Swapping only the root branches is not enough. Use finite ordered full binary trees: a tree is either Leaf or Node(L, R). Here L and R are themselves trees; their order matters, and every Node has exactly two children. A single Leaf is a complete tree.

Draw T=Node(Leaf, Node(Leaf, Leaf)). Its mirror is Node(Node(Leaf, Leaf), Leaf). Label the root’s left and right positions before drawing. The trees have the same number of leaves but different ordered shapes. Predict what a second reflection does before checking your drawing.

Predict

Define the mirror function m by two rules: m(Leaf)=Leaf and m(Node(L, R))=Node(m(R), m(L)). These are executable instructions as well as equations. Each recursive call receives a proper subtree. Because the original tree is finite, the number of constructor occurrences strictly decreases along each call chain, so recursion terminates. Unique constructor decomposition also prevents two conflicting rules from applying to the same input. This explains why the definition gives one output for every allowed input.

Predict whether equal leaf counts imply equal trees. The first example already refutes that implication. An invariant can help detect an error without completely describing an object. Do not turn a useful check into a uniqueness theorem.

Experiment

Trace the first example without skipping the inner call. This table is a static worked recursion trace, not a running program.

Call	Smaller calls	Returned tree
m(Leaf)	None	Leaf
m(Node(Leaf, Leaf))	Two calls on Leaf	Node(Leaf, Leaf)
m(T)	Right subtree first, then left subtree	Node(Node(Leaf, Leaf), Leaf)

On paper replace the original right subtree by Node(Leaf, Node(Leaf, Leaf)). Draw both trees and make a fresh trace table. At each row, retain both child results. If an implementation uses the right child twice, leaf counts can change: T=Node(Node(Leaf, Leaf), Leaf) would incorrectly become Node(Leaf, Leaf).

Now measure height in edges: h(Leaf)=0 and h(Node(L, R))=1+max(h(L), h(R)). Count leaves by ℓ(Leaf)=1 and ℓ(Node(L, R))=ℓ(L)+ℓ(R). Our initial T has height two and three leaves. Draw a height-two perfect tree with four leaves, then explain why both satisfy ℓ(T)≤2^h(T).

Understand

To prove mirror is an involution, meaning applying it twice restores the input, use structural induction. Leaf is fixed. For Node(L, R), assume m(m(L))=L and m(m(R))=R. Expanding the definition twice yields Node(m(m(L)), m(m(R)))=Node(L, R). Both subtree hypotheses are essential; the subtrees need not have the same height or shape.

The leaf bound uses a different predicate on the same constructor structure. The Leaf case is 1≤1. Write H=max(h(L), h(R)). The subtree hypotheses give ℓ(L) + ℓ(R) ≤ 2^h(L) + 2^h(R) ≤ 2·2^H = 2^(H+1). Equality requires both child bounds to be equalities and both heights to equal H. Induction therefore characterizes equality: all leaves have the same depth. This is a perfect tree, a stronger condition than merely having two children at each internal node. A chain built by repeatedly attaching one Leaf and the previous tree has height n and only n+1 leaves.

Sometimes the desired predicate is too weak for a recursive call. Finite words make this issue visible. A word is ε, the empty word, or a::u, a first symbol a followed by u. Define append by ε·v=v and (a::u)·v=a::(u·v). Induction on u proves right identity u·ε=u. It also proves associativity: the empty case reduces to v·w; in the constructor case, expanding both sides reduces the claim to (u·v)·w=u·(v·w). Keep v and w arbitrary throughout that induction.

Define ordinary reversal by rev(ε)=ε and rev(a::u)=rev(u)·[a], where [a] is a one-symbol word. An accumulator version uses A(ε, v)=v and A(a::u, v)=A(u, a::v). Its second argument stores the already reversed prefix. For example A([a, b], [c]) becomes A([b], [a, c]), then A(ε, [b, a, c]), then [b, a, c]. The original suffix [c] stays at the end.

Structural recursion with partial arithmetic expressions

A constant outer formula exposes a surprising boundary. Let F(x)=1/(x−1) and E(y)=7. Evaluating F at one fails, so strict composition E∘F is undefined there. But replacing x by F in the syntax of the constant expression 7 changes nothing: the raw substituted expression is still defined everywhere. “Composition is substitution” needs a domain statement even before any algebraic cancellation.

Does a simpler formula keep the same domain?

Predict where evaluation stops. Change the case or input, then inspect which child or denominator creates the restriction.

Expression case Constant outer expression erases the inner syntaxCancelling a ratio retains a holeReciprocal after a removable inner hole Input x -10123 Reset

Outer E(x)=7; inner F(x)=(1 ÷ (x + -1)). Proposed simpler expression: 7.

• F(x): Undefined
• Raw substituted E[F](x): 7
• Strict composition E∘F: Undefined
• Substitution retaining the F-domain guard: Undefined
• Simpler expression on its natural domain: 7

Evaluation	Subexpression	Value	Status
Inner F	1	1	Defined
Inner F	x	1	Defined
Inner F	-1	-1	Defined
Inner F	(x + -1)	0	Defined
Inner F	(1 ÷ (x + -1))	Undefined	Zero denominator
Raw E[F]	7	7	Defined

Temporary fixed-expression experiment; no learner text is executed. Undefined is a domain result, not zero. A finite table checks examples; the structural proof establishes the general theorem.

Use finite expression trees built from a variable x, real constants, and the binary constructors addition, multiplication and division. Evaluation is strict: both children must be defined before a binary operation is defined. A quotient additionally requires a nonzero denominator value. Constants and the variable have domain all real numbers. These rules define each expression’s domain D(E) and value recursively. Termination follows from descent to proper subtrees, not from assuming every expression has a value at every input.

Define syntactic substitution E[F] by replacing every variable leaf in E by the whole finite tree F, keeping constants and each binary constructor. This recursive construction terminates by descending through E. Prove the following strengthened claim by structural induction on E, with F and the real input t arbitrary: if t belongs to D(F), then E[F] is defined at t exactly when E is defined at F(t), and their values agree whenever defined.

At a variable leaf the claim is the assumed definedness of F and its own value. At a constant leaf both expressions return that constant. At addition or multiplication, the two induction hypotheses equate both child-definedness conditions and their values, so strict evaluation and the operation agree. At division the hypotheses first equate definedness of both children; when both are defined, they equate the denominator values, so the nonzero-denominator condition is also identical. Thus both domain equivalence and value equality hold at every constructor. A value-only induction would omit precisely this last obligation.

It follows that strict composition has domain D(F) intersected with D(E[F]), and equals the substituted value on that set. Equivalently, it consists of inputs in D(F) whose F-value lies in D(E). Attach the F-domain guard to raw substitution to represent composition exactly. If E contains a variable leaf, strict evaluation forces every substituted occurrence of F to be defined, so D(E[F]) is already a subset of D(F) and the extra guard is redundant. This follows by induction from domain intersections up to the root. If E has no variable occurrence, the guard can be essential, as the opening example proves. Algebraic simplification can erase variable occurrences and domain restrictions even when the original E contains them.

Trace a cancellation that loses a removable hole

Take F(x)=(x²−1)/(x−1) and E(y)=1/y. The inner domain excludes one, and its zero at minus one creates another failure in the outer denominator. Thus the composition domain is all reals except minus one and one; there its value is 1/(x+1). The simpler expression 1/(x+1) on its natural domain excludes only minus one, and takes value one-half at one. It extends the composition; it is not the same partial function. At minus one F is defined with value zero, so the outer evaluation fails for a different reason from the inner failure at one. The trace distinguishes these causes.

For partial-function equality, compare both domains and values. Equal values wherever both expressions happen to be defined establish less. A numerical table that never visits an excluded input cannot certify equality of domains.

Apply

The desired result A(u, ε)=rev(u) is a consequence of the stronger statement for every u and every v, A(u, v)=rev(u)·v. Induct on u while retaining all v. The empty case is v=ε·v. In the step, apply the hypothesis to the changed accumulator a::v:

A(a::u, v)=A(u, a::v)=rev(u)·(a::v)=(rev(u)·[a])·v=rev(a::u)·v.

The middle equality uses the append associativity already proved. A hypothesis restricted to the empty accumulator would not apply to a::v. Strengthening the claim is useful precisely because it matches the recursive call; it is not an instruction to assume the desired result.

Try a new trace A([d, e, f], [g, h]), then prove its result using the generalized formula. Diagnose the variation that appends a to the accumulator’s end instead of its front. Finally explain why a cyclic reference C=Node(Leaf, C) is outside the domain: its right-child calls never reach Leaf. These proofs establish totality for finite constructor objects, not for arbitrary pointer graphs or infinite trees.

Continue

Keep three pieces of evidence: a recursion trace, a constructor-by-constructor proof, and a counterexample to an incorrect definition. They answer different questions. Traces check selected inputs; structural induction covers every finite generated object; counterexamples expose a broken claim. The practice below asks you to construct each kind of evidence and to explain why the stronger accumulator predicate is necessary. Implementing these definitions in a programming language additionally requires suitable data representations and tests; this written lesson does not execute learner code or certify an implementation.