commit 10861dec9b980519d83e98d74f004e3e4e2d42a9
parent 02782b5256c3d8144eb5248f75374abe5b4e7618
Author: ling0x <ling0x@users.noreply.github.com>
Date: Thu, 25 Jun 2026 13:21:59 +0100
refactor: piper
Diffstat:
2 files changed, 397 insertions(+), 0 deletions(-)
diff --git a/algorithms/inductive_proofs.txt b/algorithms/inductive_proofs.txt
@@ -0,0 +1,383 @@
+=================================================================
+ INDUCTIVE PROOFS AND ALGORITHMS
+ A Software Engineer's Guide to Correctness
+=================================================================
+
+
+WHY THIS MATTERS
+-----------------------------------------------------------------
+
+Algorithms are step-by-step procedures. In software engineering
+we care about two things beyond "it seems to work":
+
+ 1. Does the algorithm always produce the right answer?
+ 2. Does it terminate?
+
+Inductive proof is the standard mathematical tool for answering
+both questions when an algorithm is defined recursively or
+iterates over a growing structure (lists, trees, arrays, loop
+counters).
+
+You do not need to write formal proofs on every pull request. But
+understanding induction helps you:
+
+ - State loop invariants clearly during code review
+ - Debug off-by-one errors and missing base cases
+ - Design recursive solutions with confidence
+ - Read correctness arguments in papers, textbooks, and specs
+ - Connect tests, contracts, and formal methods to the same
+ mental model
+
+
+WHAT IS MATHEMATICAL INDUCTION?
+-----------------------------------------------------------------
+
+Induction proves a statement P(n) for all integers n >= n0 (often
+n0 = 0 or 1).
+
+Structure:
+
+ BASE CASE Prove P(n0) is true.
+ INDUCTIVE STEP Assume P(k) for some k >= n0 (inductive
+ hypothesis). Prove P(k+1) follows.
+
+If both hold, P(n) holds for every n >= n0.
+
+Intuition: dominoes. Knock over the first (base). Each domino
+knocks the next (inductive step). The whole row falls.
+
+Example — sum of first n positive integers:
+
+ Claim: 1 + 2 + ... + n = n(n+1)/2
+
+ Base (n=1): 1 = 1(2)/2 [ok]
+
+ Step: Assume 1 + ... + k = k(k+1)/2.
+ Then 1 + ... + k + (k+1)
+ = k(k+1)/2 + (k+1)
+ = (k+1)(k+2)/2
+ which is the formula for n = k+1. [ok]
+
+
+WEAK VS STRONG INDUCTION
+-----------------------------------------------------------------
+
+WEAK INDUCTION (ordinary induction)
+ Inductive hypothesis: P(k) only.
+
+STRONG INDUCTION
+ Inductive hypothesis: P(n0), P(n0+1), ..., P(k) all hold.
+ Then prove P(k+1).
+
+Use strong induction when the next case depends on more than one
+prior case (e.g. Fibonacci, divide-and-conquer where subproblems
+are smaller but not exactly k and k+1).
+
+In practice, pick whichever makes the inductive step easiest to
+write.
+
+
+INDUCTION AND RECURSION ARE THE SAME SHAPE
+-----------------------------------------------------------------
+
+A recursive function has:
+
+ BASE CASE Stop recursion (smallest input).
+ RECURSIVE CASE Solve a smaller instance, combine results.
+
+A proof by induction mirrors that call structure:
+
+ BASE CASE Prove correctness for the smallest input.
+ INDUCTIVE STEP Assume correctness for size k; prove for k+1
+ (often by invoking the hypothesis on the
+ recursive call).
+
+Example — factorial:
+
+ function fact(n):
+ if n == 0: return 1
+ return n * fact(n - 1)
+
+ Claim: fact(n) = n! for n >= 0.
+
+ Base: fact(0) = 1 = 0! [ok]
+
+ Step: Assume fact(k) = k! for k >= 0.
+ fact(k+1) = (k+1) * fact(k) [by code]
+ = (k+1) * k! [by hypothesis]
+ = (k+1)! [ok]
+
+When you write a recursive algorithm, you are already halfway to
+an inductive proof. The missing piece is stating the claim
+precisely.
+
+
+STRUCTURAL INDUCTION (INDUCTION ON DATA)
+-----------------------------------------------------------------
+
+Software rarely works on bare integers alone. We use lists,
+trees, graphs.
+
+STRUCTURAL INDUCTION proves a property for all values of a
+recursively defined type:
+
+ - Linked list: Nil | Cons(head, tail)
+ - Binary tree: Leaf | Node(left, value, right)
+
+Base: property holds for Nil / Leaf.
+Step: if it holds for subtrees, it holds for Cons / Node.
+
+Example — length of a list:
+
+ length(Nil) = 0
+ length(Cons(x, xs)) = 1 + length(xs)
+
+ Claim: length(xs) equals the number of elements in xs.
+
+ Base: length(Nil) = 0; Nil has 0 elements. [ok]
+
+ Step: Assume length(xs) = |xs|.
+ length(Cons(x, xs)) = 1 + length(xs)
+ = 1 + |xs|
+ = |Cons(x,xs)|. [ok]
+
+This pattern appears everywhere: map, filter, fold, tree
+traversals, serializers.
+
+
+LOOP INVARIANTS — INDUCTION WITHOUT RECURSION
+-----------------------------------------------------------------
+
+Iterative algorithms use loops instead of recursion. Induction
+still applies via a LOOP INVARIANT: a predicate that is:
+
+ 1. TRUE before the loop starts (initialization)
+ 2. PRESERVED each iteration (maintenance)
+ 3. USEFUL when the loop exits (termination +
+ conclusion)
+
+Together with a variant (a quantity that strictly decreases,
+e.g. loop counter or remaining array size), this proves
+correctness and termination.
+
+Example — linear search for target t in array A[0..n-1]:
+
+ Invariant: After i iterations, t is not in A[0..i-1].
+
+ Init: i = 0; A[0..-1] is empty; nothing to find. [ok]
+ Maint: If A[i] != t, t not in A[0..i]; extend to A[0..i].
+ [ok]
+ Term: Loop ends when i = n or A[i] = t.
+ If i = n, t not in entire array.
+ If A[i] = t, we found it.
+
+The invariant is what you wish you had written as a comment
+before debugging for two hours.
+
+Template for loop-heavy code:
+
+ // Invariant: <what is always true at the top of each
+ // iteration>
+ // Variant: <what decreases so the loop cannot run
+ // forever>
+ while (condition) {
+ ...
+ }
+ // Postcondition: <what we know when we exit>
+
+
+PROVING A DIVIDE-AND-CONQUER ALGORITHM
+-----------------------------------------------------------------
+
+Merge sort on array segment A[low..high]:
+
+ If low >= high: return (base — segment of size 0 or 1 is
+ sorted).
+ Split at mid, sort left half, sort right half, merge.
+
+Claim: merge_sort(A, low, high) returns A[low..high] sorted.
+
+Proof uses strong induction on segment length n = high - low + 1.
+
+ Base (n <= 1): trivially sorted. [ok]
+
+ Step: For n > 1, both halves have length < n.
+ By inductive hypothesis, recursive calls return sorted
+ halves. Merge of two sorted sequences is sorted (separate
+ lemma). Therefore full segment is sorted. [ok]
+
+Complexity (O(n log n)) is a different proof — often by
+recurrence — but correctness and complexity are both inductive
+arguments over problem size.
+
+
+PARTIAL VS TOTAL CORRECTNESS
+-----------------------------------------------------------------
+
+ PARTIAL CORRECTNESS
+ IF the algorithm terminates, THEN the output satisfies the
+ spec.
+
+ TOTAL CORRECTNESS
+ The algorithm terminates AND the output satisfies the spec.
+
+Induction on the inductive step often proves partial correctness
+(the invariant or recursive structure gives the right answer).
+
+A VARIANT FUNCTION (or well-founded ordering on inputs) proves
+termination.
+
+Example — Euclidean GCD while loop:
+
+ while b != 0: (a, b) = (b, a % b)
+
+ Invariant: gcd(a, b) = gcd(original a, original b).
+ Variant: b strictly decreases and stays >= 0; must reach
+ b = 0.
+
+
+COMMON PITFALLS IN SOFTWARE (AND IN PROOFS)
+-----------------------------------------------------------------
+
+ OFF-BY-ONE
+ Induction base at n=0 vs n=1; array bounds [0,n) vs [1,n].
+ Symptom: works on "most" inputs, fails on empty or single
+ element.
+
+ MISSING BASE CASE
+ Recursion without a stop condition; induction without a base.
+ Symptom: stack overflow, infinite loop, or vacuous "proof".
+
+ WRONG INDUCTIVE HYPOTHESIS
+ Claim too weak to prove the next step; or too strong to prove
+ from prior. Symptom: "it works for k but I cannot show k+1."
+
+ INVARIANT NOT MAINTAINED
+ A line of the loop breaks the predicate you thought was true.
+ Symptom: intermittent wrong answers depending on input shape.
+
+ CONFUSING EXAMPLE WITH PROOF
+ Tests pass on many cases but do not cover the inductive
+ structure. Symptom: ship now, debug in production on edge
+ cases.
+
+Debugging tip: when a loop or recursion fails, write the
+invariant you expected. Find the first iteration or call where it
+becomes false.
+
+
+FROM PROOFS TO ENGINEERING PRACTICE
+-----------------------------------------------------------------
+
+You will rarely publish a full inductive proof in application
+code. You will use the same ideas:
+
+ LOOP INVARIANTS IN CODE REVIEW
+ "What is always true here? Can this assignment break it?"
+
+ PRECONDITIONS / POSTCONDITIONS
+ (contracts, asserts, design by contract)
+ Base case = precondition; postcondition = what induction
+ concludes.
+
+ RECURSIVE API DESIGN
+ Smaller subproblem + combine = inductive step. Document the
+ "size" that decreases.
+
+ PROPERTY-BASED TESTING
+ Generators produce random inputs; properties state P(n) for
+ all n. Failing case is a counterexample to your inductive
+ claim.
+
+ FORMAL VERIFICATION (TLA+, Dafny, Coq, Lean, etc.)
+ Machine-checked induction on invariants and recursive
+ definitions.
+
+ DOCUMENTATION
+ README or spec: "This maintains invariant X; on exit, Y
+ holds."
+
+The proof is the specification made precise. Tests sample the
+specification. Induction explains why infinite families of inputs
+behave the same way.
+
+
+WORKED MINI-EXAMPLE — BINARY SEARCH
+-----------------------------------------------------------------
+
+Binary search on sorted A[0..n-1] for target t.
+
+Invariant (main loop, search space [lo, hi]):
+
+ If t is in A, then t is in A[lo..hi].
+
+Init: lo = 0, hi = n-1; entire array is search space. [ok]
+
+Maint: mid = lo + (hi - lo) / 2.
+ A is sorted.
+ If A[mid] < t, any index with value t must be > mid,
+ so t in A[mid+1..hi]. Set lo = mid + 1; invariant
+ preserved (and lo <= hi or exit).
+ Symmetric if A[mid] > t.
+ If A[mid] == t, found.
+
+Term: lo > hi => search space empty => t not in A
+ (consistent).
+ Or return mid when A[mid] == t.
+
+Variant: hi - lo shrinks each step (when not found at mid) =>
+ O(log n) iterations.
+
+This is the argument behind every "buggy binary search" blog
+post: the invariant must match the update to lo and hi exactly.
+
+
+CHECKLIST BEFORE YOU SHIP A RECURSIVE OR LOOPING ALGORITHM
+-----------------------------------------------------------------
+
+ [ ] State the property P(n) or invariant I explicitly.
+ [ ] Identify the base case(s) — empty input, n=0, leaf nodes.
+ [ ] Show the inductive / maintenance step in one short
+ paragraph.
+ [ ] Name the variant that proves termination.
+ [ ] Test base cases and one "representative" inductive step
+ size (e.g. n=2).
+ [ ] For loops: check first and last iteration against the
+ invariant.
+
+
+FURTHER READING
+-----------------------------------------------------------------
+
+ - "Introduction to Algorithms" (CLRS) — loop invariants,
+ correctness proofs
+ - "The Algorithm Design Manual" (Skiena) — practical proof
+ sketches
+ - "How to Prove It" (Velleman) — induction for programmers new
+ to proofs
+ - Software Foundations / Logical Foundations (Coq) —
+ mechanized induction
+ - "A Discipline of Programming" (Dijkstra) — invariants as
+ design method
+
+
+SUMMARY
+-----------------------------------------------------------------
+
+Inductive proof is the mathematical backbone of algorithm
+correctness:
+
+ Recursion <-> induction on size / structure
+ Loops <-> loop invariants + variant
+ Data types <-> structural induction
+ Engineering <-> specs, contracts, tests, and reviews that
+ encode the same claims
+
+Learn to state what your algorithm keeps true at every step.
+Correctness follows from that habit — whether you write a formal
+proof or not.
+
+
+=================================================================
+ algorithms/inductive_proofs.txt
+=================================================================
diff --git a/commands/piper-tts.txt b/commands/piper-tts.txt
@@ -0,0 +1,13 @@
+Install Piper on archlinux:
+
+yay -S piper-tts-bin
+
+Install voices:
+
+yay -S piper-voices-en-us
+
+How to use it to play audio directly:
+
+cat test.txt | piper-tts \
+ --model /usr/share/piper-voices/en/en_US/bryce/medium/en_US-bryce-medium.onnx \
+ --output-raw | aplay -r 22050 -f S16_LE -t raw -
+\ No newline at end of file
