commit 17c92129eec74e7c8a910e0bb9606e5dfb659f8d
parent e8e2d1bfafdafd3bd7eaa71926efa18eadabda86
Author: ling0x <ling0x@users.noreply.github.com>
Date: Thu, 30 Jul 2026 11:43:42 +0100
algorithms
Diffstat:
3 files changed, 50 insertions(+), 385 deletions(-)
diff --git a/algorithms/inductive_proofs.txt b/algorithms/inductive_proofs.txt
@@ -1,383 +0,0 @@
-=================================================================
- 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/algorithms/introduction_to_algorithms.txt b/algorithms/introduction_to_algorithms.txt
@@ -0,0 +1,39 @@
+========================================================================
+Introduction to Algorithms
+========================================================================
+
+Loop Invariant
+
+Loop invariant help up understand why an algorithm is correct. When you're
+using a loop invariant, you need to show three things:
+
+- Initialization: If it is true prior to the first iteration of the loop.
+
+- Maintenance: If it is true before an iteration of the loop, it remains
+true before the next iteration.
+
+- Termination: The loop terminates, and when it terminates, the invariant,
+usually along with the reason that the loop terminated, gives us a useful
+property that helps show that the algorithm is correct.
+
+A loop-invariant proof is a form of mathematical induction, where to prove
+that a property holds, you prove a base case and an inductive step.
+
+Example:
+
+Loop invariant of a sum array:
+
+SUM-ARRAY (A,n)
+ sum = 0
+ for i = 1 to n
+ sum = sum + A[i]
+ return sum
+
+i-1
+ Σ k
+k=1
+
+or
+
+Σ(k = 1 to i-1) k
+
diff --git a/commands/pdf-image.txt b/commands/pdf-image.txt
@@ -1,4 +1,6 @@
+=========================================================================
PDF and Images related commands
+=========================================================================
Combine PDFs:
@@ -10,4 +12,11 @@ gs -dNOPAUSE -dBATCH -sDEVICE=pdfwrite -dPDFSETTINGS=/ebook -sOutputFile=combine
Rasterize PDF to reduce its size:
-convert -density 200 combined.pdf -quality 90 -compress jpeg combined_raster_hq.pdf
-\ No newline at end of file
+convert -density 200 combined.pdf -quality 90 -compress jpeg combined_raster_hq.pdf
+
+=========================================================================
+Read PDF in terminal
+=========================================================================
+
+sudo pacman -S poppler
+pdftotext -layout file.pdf - | less
+\ No newline at end of file
