Induction and Structural Recursion TODO
Concept
Mathematical induction is a proof principle grounded in the well-ordering of the natural numbers: showing a base case and a step from n to n+1 lets you conclude the proposition holds for all natural numbers. Strong induction lets you use every case smaller than n as a hypothesis, and generalizing this further gives well-founded induction over well-founded relations, which applies to structures beyond the naturals. Structural induction is a special case of this that uses the fact that algebraic data types are built up finitely from constructors, proving the proposition for each constructor. For trees, you handle the leaf (base case) and the internal node (conclusion from the hypothesis on the children) separately, and this proof structure matches exactly the shape of a recursive function. In other words, proving a recursive program correct is structural induction that follows the program's own recursive structure, and termination is shown by exhibiting a well-founded measure that decreases on every recursive call.
Being able to explain why an invariant of a recursive function or tree data structure always holds — rather than just "I ran it and it worked" — lets you rule out edge cases by structure instead of by testing.
Code & Formula
# 귀납법/구조적 재귀 — 이진 트리의 "리프 수 = 내부노드 수 + 1"을 구조적 귀납으로 확인.
# 기저: 리프 하나뿐인 트리는 leaves=1, internal=0 → 1=0+1.
# 귀납 단계: 왼쪽/오른쪽 부분트리가 각각 성립한다고 가정하면, 합쳐도 그대로 성립.
class Leaf:
pass
class Node:
def __init__(self, left, right):
self.left = left
self.right = right
def count_leaves(t):
if isinstance(t, Leaf):
return 1
return count_leaves(t.left) + count_leaves(t.right) # 재귀 = 귀납 가정 사용
def count_internal(t):
if isinstance(t, Leaf):
return 0
return 1 + count_internal(t.left) + count_internal(t.right)
def check_property(t):
# 명제 P(t): leaves(t) == internal(t) + 1
return count_leaves(t) == count_internal(t) + 1
# 무작위로 완전(full) 이진 트리를 만들어 매번 P(t)가 성립하는지 확인.
import random
def random_full_tree(depth):
if depth == 0 or random.random() < 0.3:
return Leaf()
return Node(random_full_tree(depth - 1), random_full_tree(depth - 1))
random.seed(0)
trees = [random_full_tree(4) for _ in range(20)]
results = [check_property(t) for t in trees]
print("검사한 트리 수:", len(trees))
print("모두 P(t) 성립?", all(results))
sample = trees[0]
print(f"예시 트리: 리프={count_leaves(sample)}, 내부노드={count_internal(sample)}")
Exercise
Prove on paper, by structural induction, that a (full) binary tree always has exactly one more leaf than internal node, then write a verification function recursively following the same structure.
Practical Connection
Properties of Merkle trees like "equal roots imply equal leaf sets" or "inclusion-proof verification is correct" are all proved by induction on tree height, and the recursive structure of the verification code corresponds one-to-one with the induction step.
Where it lands in Jayverse
- Bridge: write the lock/mint Merkle inclusion-proof verifier as structural induction on tree height. A recursive verifier function that mirrors the proof shape, not an ad hoc loop, is what the induction argument requires to actually hold.
- Verex: test "equal roots imply equal leaf sets" directly for any Merkle-committed state (order-book or balance snapshots). Construct two different leaf sets and confirm distinct roots, rather than trusting the property by inspection.
- Auditor: require a written well-founded termination measure for any recursive verifier before it ships. A decreasing tree depth is trivial to state and cheap to check in review, and it's the difference between a proof and a hope.
Key expressions
| Expression | 뜻 · 쓰이는 자리 |
|---|---|
| grounded in | ~에 근거를 둔 · "a proof principle grounded in the well-ordering of the natural numbers" |
| well-founded | (무한 하강이 없어) 정초가 있는 · "well-founded induction over well-founded relations" |
| rule out | (가능성을) 배제하다 · "lets you rule out edge cases by structure instead of by testing" |
| exhibit (a measure) | (증명에서 특정 대상을) 제시하다, 보여주다 · "exhibiting a well-founded measure that decreases on every recursive call" |
| correspond one-to-one with | ~와 일대일로 대응하다 · "the recursive structure of the verification code corresponds one-to-one with the induction step" |
| base case | 귀납법의 출발점이 되는 기저 사례 · "showing a base case and a step from n to n+1" |
| imply | ~을 함축하다, ~을 의미하다 · "equal roots imply equal leaf sets" |
If you study this on a given day, add a note link and a ✅ to this line in the source curriculum (docs/knowledge/math-50-curriculum.md) and this spot will lead straight to the note body. You can also write directly on this page — but regenerating overwrites it, so it's safer to keep anything you want to save as markdown under docs/algorithms/.