MATH.4:4 - Solution
Local mantra: state the wanted object; build the base; build the next case from smaller cases; justify the construction; use the witness.
MATH.4:4.1 - State the input construction and wanted result
Name the input family, its constructors and any fixed parameters. For natural numbers, the constructors are zero and successor. A finite binary tree can be a leaf or a new root joining two smaller trees. The supplied constructor and constituents determine which recursive clause applies. If different constructions are later identified, retain that identification as a separate condition.
For each input x, state the kind of output y and the property P(x,y) it must satisfy. Include bounds or retained information that the next use consumes. For division by a positive integer d, the output is a pair (q,r) satisfying n=q*d+r and 0≤r<d.
Use the input’s actual formation rules to choose the cases. A proof about trees cannot be applied to a structure with additional edges without considering those edges.
MATH.4:4.2 - Construct the base witnesses
For each constructor with no smaller inputs, give an output and show that it satisfies the required property. This supplies the point at which recursive evaluation can return a value.
If the base fails, inspect the specification or its parameter conditions. Do not invent a default output that fails the requirement merely to complete the cases.
MATH.4:4.3 - Construct the step and strengthen what it needs
Take one constructor with smaller inputs. Assume that each smaller input already has an output satisfying the stated property. Give an operation that uses those outputs to build the required output for the whole input.
Show why the construction preserves the property. Check each branch that changes the returned object. When the step needs information absent from the proposed output, strengthen the result or generalize a fixed parameter, then revisit the base cases and affected steps.
For example, a tree-coloring step may need to choose either color for a subtree’s root. A construction that promises only a root of color zero leaves that step unsupported. A construction parameterized by the required root color supplies what the step uses.
To obtain an executable construction, each case distinction must be decidable from the supplied data, and each operation used to build an output must itself return. A step that says only “choose a suitable object” identifies further mathematical work unless a way to make that choice is already supplied.
MATH.4:4.4 - Define the operation and establish its result
For a natural-number input, let b be the base witness and let step(n,y) produce a witness for n+1 from one for n. Define:
F(0)=b
F(n+1)=step(n,F(n)).
The base argument establishes P(0,F(0)). The step argument establishes P(n+1,F(n+1)) from P(n,F(n)). Induction therefore establishes the property for every natural number.
For another finite inductive input, give one defining clause and one property argument per constructor. Recursive calls use its immediate constituents. Evaluation terminates because these calls descend through a finite input construction, provided the operations within each clause terminate.
When different constructor expressions represent one object, the recursion first gives a function of expressions. To obtain a function of the represented object, establish that all its permitted expressions yield the same required output, using MATH.2. Alternatively, supply an additional rule that chooses one construction from the object. Keeping the construction as part of the input is also useful when its history matters.
For example, build a finite set with Empty and Insert(a,S) for a outside S. Returning [] at the base and prepending a at each step gives a list containing each element once. Yet Insert(1,Insert(2,Empty)) and Insert(2,Insert(1,Empty)) represent the same set and return [1,2] and [2,1]. Both are valid witnesses, but these clauses define a function of the insertion construction. If a function of the set is required and its elements have a supplied total order, strengthen the output requirement to an increasing list and insert each element in order. The unique increasing list then makes the output independent of insertion order. This repair uses the ordering operation and a stronger specification.
A dependent-type description can package the output with a proof of its property. Its first projection returns the witness; the other component justifies that witness for the stated input. An ordinary mathematical presentation may instead give the function and proof separately. Use the presentation needed for the receiving work.
MATH.4:4.5 - Use the witness and return after a changed requirement
Evaluate the construction for the needed input. Return the object and the property on which its next use relies. Reuse the general argument while its constructors, clauses and premises remain unchanged.
If the receiver needs another quantity, check whether the current result retains it. If a parameter or formation rule changes, return to the affected base or constructor clause. If constructions are newly identified, check whether the output still defines a function on those identified inputs. A failed clause can supply a counterexample or a more specific construction question.
An executable recursive construction is already an algorithm. Its operation count, storage and representation can become further design questions when the intended scale makes them matter. A faster implementation can retain the same mathematical specification; the correspondence between the two constructions needs its own argument.
Stop with the required witness, a reusable construction with its property, or a particular unresolved clause. Formalizing the same result in a proof assistant is useful when that receiving use needs it.