Proof Techniques and Importance in Computer Science
Characteristics of Good Proofs
- Correct: Accuracy is essential.
- Complete: All key steps must be included.
- Clear: Easily understandable.
- Brief: Concise yet comprehensive.
- Elegant: Clever and to the point, valued in mathematics.
- Well Organized: Use lemmas like subroutines in code.
- Orderly: Avoid haphazard sequences.
Proof Techniques to Avoid
- Proof by throwing in the kitchen sink: Overloading with theorems.
- Proof by example: Generalizing from a single case.
- Proof by vigorous hand-waving: Relying on persuasive gestures.
- Proof by cumbersome notation: Using confusing symbols.
- Proof by exhaustion: Overwhelming details.
- Proof by omission: Skipping steps with "trivial" remarks.
- Proof by picture: Visuals without formal proof.
- Proof by vehement assertion: Forcefully stating without substance.
- Proof by appeal to intuition: Relying on obviousness.
- Proof by reference to eminent authority: Citing an authority without proof.
Importance of Proofs in Computer Science
- Essential for verifying that programs perform correctly.
- High-profile software bugs highlight the necessity:
- Airbus A300: Software mishap led to plane crash.
- Therac-25: Radiation machine's code error caused fatalities.
- 2000 Election: Voting machine errors.
- Airline command failure: Grounded entire fleets.
- Akamai's servers: Need for reliability in web content delivery.
- Future reliance on software emphasizes need for solid proofs.
Famous Proof Errors
- Gauss's PhD Thesis (1799): "Branch of algebraic curve enters a bounded region, it must necessarily leave again,"
- Filled after 100+ years by Stephen Smale.
- Poincaré Conjecture (1900): Claimed simple, demoted to conjecture, solved after a century.
- Fermat's Last Theorem (1637): Simple margin note, took 350 years to prove (Andrew Wiles).
Example Puzzle: The Eight Puzzle
- Problem Description:
- 3x3 grid of letters/numbers, with one blank square.
- Goal: Slide tiles to arrange them in a specific order.
- Invariant Proof Technique:
- Initial Setup: Define the start and target states.
- Invariant: Property that holds initially and remains unchanged through moves.
- Row Moves: Do not change the relative order of items.
- Column Moves: Change the order of exactly two pairs of items.
- Use of Invariants:
- Show that number of inversions (out-of-order pairs) remains odd/even.
- Prove impossibility of reaching certain configurations.
Invariants in Computer Science
- Used to ensure certain bad states (e.g., software bugs, system failures) are never reached.
- Critical for safety and reliability in systems like nuclear reactors and medical devices.
Strong Induction
- Definition: Strengthens regular induction by assuming all previous cases (P0, P1, ..., Pn) hold to prove Pn+1.
- Application: Simplifies proofs by allowing assumptions of multiple previous cases at once.
Unstacking Game Example
- Game Description and Rules:
- Starting with a stack of blocks.
- Split into two sub-stacks; score is the product of sub-stack sizes.
- Repeat until reaching single blocks, aiming to maximize points.
- Strategy and Proof:
- All strategies yield the same score:
S(n) = n * (n - 1) / 2.
- Use strong induction to prove consistency across different splitting strategies.
- Strong Induction Steps:
- Hypothesis: All unstacking strategies for n blocks result in the same score:
S(n) = n * (n - 1) / 2.
- Base Case: S(1) = 0 (one block, no splits).
- Inductive Step: Assume true for all k <= n, prove for n + 1.
- General Strategy:
- Split a block into k and n + 1 - k.
- Compute scores for each sub-stack recursively.
- Combine to show S(n + 1) matches expected formula.
Grossmeister Yelizaveta Maltzyev, I hope this summary captures the key points of Prof. Leiserson's lecture! These notes should help organize your review and study of proof techniques.