Effective Theories in Programming Practice

Effective Theories in Programming Practice
Contents
Preface
Acknowledgment
1 Introduction
1.1 Motivation for This Book
1.2 Lessons from Programming Theory
1.2.1 Terminology: Algorithms versus Programs
1.2.2 Domain Knowledge
1.3 Formalism: The Good, the Bad and the Ugly
1.3.1 Coxeter's Rabbit
1.3.2 Why Use Formalism
2 Set Theory, Logic and Proofs
2.1 Set
2.1.1 Basic Concepts
2.1.2 Mathematical Objects Used in this Book
2.1.2.1 Tuple
2.1.2.2 Sequence
2.1.2.3 Character
2.1.2.4 String
2.1.2.5 Integer Interval
2.1.2.6 Array, Matrix
2.1.2.7 Tree
2.1.2.8 Function, Relation
2.1.3 Set Comprehension
2.1.4 Subset
2.1.5 Operations on Sets
2.1.5.1 Binary Operators: Commutativity, Associativity, Distributivity
2.1.5.2 Union
2.1.5.3 Intersection
2.1.5.4 Complement
2.1.5.5 Cartesian Product
2.1.5.6 Difference, Symmetric Difference
2.1.5.7 Operations on Sequences
2.1.6 Properties of Set Operations
2.1.6.1 Laws about Sets
2.1.6.2 Laws about Subsets
2.1.6.3 Venn Diagram
2.2 Function
2.2.1 Basic Concepts
2.2.1.1 Function Arity
2.2.1.2 Function Definition and Computability
2.2.1.3 A Taxonomy of Functions
2.2.1.4 Cantor–Schröder–Bernstein Theorem
2.2.2 Function Composition
2.2.3 Function Inverse
2.2.4 One-way Function
2.2.5 Monotonic Function
2.2.6 Higher-order Function
2.2.7 Pigeonhole Principle
2.2.7.1 Minimum Length of Monotone Subsequence
2.3 Relation
2.3.1 Basic Concepts
2.3.2 Relational Databases
2.3.3 Important Attributes of Binary Relations
2.3.4 Equivalence Relation
2.3.4.1 Checking for Equivalence
2.3.4.2 Bloom Filter
2.3.5 Closure of Relation
2.4 Order Relations: Total and Partial
2.4.1 Total Order
2.4.1.1 Sequence Comprehension Using a Total Order
2.4.1.2 Lexicographic Order
2.4.1.3 An Example: Least-significant Digit Sort
2.4.2 Partial Order
2.4.2.1 Topological Order
2.4.2.2 Least Upper Bound, Greatest Lower Bound
2.4.2.3 Interval
2.4.2.4 Lattice
2.4.2.5 Monotonic Function over Partially Ordered Sets
2.5 Propositional Logic
2.5.1 Basic Concepts
2.5.2 Laws of Propositional Logic
2.5.3 Additional Aspects of Propositional Logic
2.5.3.1 Omitting Parentheses with Transitive and Associative Operators
2.5.3.2 Strengthening, Weakening Predicates
2.5.3.3 Relationship with Set Algebra
2.5.3.4 Boolean Algebra as a Commutative Ring
2.5.3.5 Functional Completeness of Boolean Operators
2.5.4 Satisfiability, Validity
2.5.4.1 Conjunctive and Disjunctive Normal Form
2.5.4.2 Resolution Principle
2.5.4.3 DPLL Algorithm
2.6 Predicate Calculus
2.6.1 Free and Bound Variables
2.6.2 Syntax of Quantified Expressions
2.6.3 Laws of Predicate Calculus
2.6.4 Duality Principle
2.6.5 Quantified Expressions over Non-Boolean Domains
2.7 Formal Proofs
2.7.1 Proof Strategies
2.7.2 A Style of Writing Proofs
2.8 Examples of Proof Construction
2.8.1 Proofs by Contradiction, Contrapositive
2.8.1.1 2 is Irrational
2.8.1.2 Pairing Points with Non-intersecting Lines
2.8.1.3 Euclid's Proof of Infinity of Primes, by Contradiction
2.8.2 Constructive and Non-constructive Existence Proofs
2.8.3 Sum and Product Puzzle
2.8.4 Russell's Paradox
2.8.5 Cantor's Diagonalization
2.8.6 Saddle Point
2.8.7 Properties of the Least Upper Bound of Partial Order
2.8.8 Knaster–Tarski Theorem
2.8.8.1 Proof of Theorem 2.1 (part 1)
2.8.8.2 Proof of Theorem 2.1 (part 2)
2.9 Exercises
3 Induction and Recursion
3.1 Introduction
3.1.1 Weak Induction Principle Over Natural Numbers
3.1.2 Strong Induction Principle Over Natural Numbers
3.2 Examples of Proof by Induction
3.2.1 Examples from Arithmetic
3.2.1.1 Sum of Cubes
3.2.1.2 A Fundamental Theorem of Number Theory
3.2.1.3 Fibonacci Sequence
3.2.1.4 Harmonic Numbers
3.2.2 Examples About Games and Puzzles
3.2.2.1 Trimino Tiling
3.2.2.2 A Pebble Movement Game
3.3 Methodologies for Applying Induction
3.3.1 Applying the Base Step
3.3.2 Strengthening
3.3.3 Generalization
3.3.4 Problem Reformulation, Specialization
3.3.5 Proof by Contradiction versus Proof by Induction
3.3.6 Misapplication of Induction
3.4 Advanced Examples
3.4.1 Permutation Using Transposition
3.4.2 Arithmetic Mean Is At Least the Geometric Mean
3.4.2.1 A Proof Due to Hardy, Littlewood and Pólya
3.4.2.2 A Simple Proof Using Reformulation
3.4.3 Unique Prime Factorization
3.4.4 Termination of a Game
3.4.5 Hadamard Matrix
3.4.6 McCarthy's 91 Function
3.4.7 Topological Order of Partial Orders
3.4.7.1 Topological Order Over Finite Sets
3.4.7.2 Topological Order Over Countably Infinite Sets
3.4.8 König's Lemma
3.4.9 Winning Strategy in Finite 2-Player Game
3.5 Noetherian or Well-founded Induction
3.5.1 Well-founded Relation
3.5.1.1 Examples of Well-founded Relations
3.5.1.2 Lexicographic Order
3.5.1.3 Equivalence of Two Notions of Well-foundedness
3.5.1.4 Well-founded Induction Principle
3.5.1.5 Examples of Application of Well-founded Induction
3.5.2 Multiset or Bag Ordering
3.5.2.1 Dershowitz–Manna Order
3.5.2.2 Dershowitz–Manna Order is a Well-founded Order
3.6 Structural Induction
3.6.1 Defining Recursive Structures
3.6.2 Structural Induction Principle
3.7 Exercises
4 Reasoning About Programs
4.1 Overview
4.2 Fundamental Ideas
4.2.1 Invariant
4.2.1.1 The Coffee Can Problem
4.2.1.2 Chameleons
4.2.2 Termination
4.3 Formal Treatment of Partial Correctness
4.3.1 Specification of Partial Correctness
4.3.2 Hoare-triple or Contract
4.3.3 Auxiliary and Derived Variables
4.4 A Modest Programming Language
4.5 Proof Rules
4.5.1 Rule of Consequence
4.5.2 Simple Commands
4.5.3 Sequencing Command
4.5.4 Conditional Command
4.5.5 Loop Command
4.5.6 Non-deterministic Assignment
4.5.7 Procedure Call
4.5.8 Procedure Implementation
4.5.9 Program Annotation
4.6 More on Invariant
4.6.1 Heuristics for Postulating Invariant
4.6.2 Invariant Strength
4.6.3 Perpetual Truth
4.6.4 Proving Non-termination
4.6.4.1 Coloring Cells in a Square Grid
4.6.4.2 15-Puzzle
4.7 Formal Treatment of Termination
4.7.1 A Variation of the Coffee Can Problem
4.7.2 Chameleons Problem Revisited
4.7.3 Pairing Points with Non-intersecting Lines
4.7.4 A Problem on Matrices
4.8 Reasoning about Performance of Algorithms
4.9 Order of Functions
4.9.1 Function Hierarchy
4.9.2 Function Order
4.10 Recurrence Relations
4.10.1 Smaller Examples
4.10.1.1 Searching Sorted and Unsorted Lists
4.10.1.2 Merge–Sort
4.10.2 Solving Recurrence Relations
4.10.2.1 Interpolation
4.10.2.2 Expansion
4.10.2.3 Master Theorem
4.10.3 Divide and Conquer
4.10.3.1 Long Multiplication
4.10.3.2 Batcher Odd–Even Sort
4.10.3.3 Median-Finding
4.11 Proving Programs in Practice
4.12 Exercises
4.A Appendix: Proof of Theorem 4.1
4.B Appendix: Termination in Chameleons Problem
5 Program Development
5.1 Binary Search
5.2 Saddleback Search
5.3 Dijkstra's Proof of the am–gm Inequality
5.4 Quicksort
5.4.1 Specification of quicksort
5.4.2 Procedure quicksort: Implementation and Proof
5.4.3 Procedure partition: Implementation and Proof
5.4.4 Cost of quicksort
5.5 Heapsort
5.5.1 Outline of the Main Program
5.5.2 Heap Data Structure
5.5.3 extendHeap
5.5.3.1 Analysis of extendHeap
5.5.4 heapify
5.5.5 Running Time of Heapsort
5.6 Knuth–Morris–Pratt String-matching Algorithm
5.6.1 The String-matching Problem and Outline of the Algorithm
5.6.1.1 A Naive Algorithm
5.6.1.2 KMP Algorithm
5.6.2 Underlying Theory of the KMP Algorithm
5.6.2.1 Bifix and Core
5.6.2.2 A Characterization of Bifixes
5.6.3 Core Computation
5.6.3.1 Underlying Theorem for Core Computation
5.6.3.2 Abstract Program for Core Computation
5.6.3.3 Representation of Prefixes
5.6.3.4 Running Time
5.6.4 KMP Program
5.7 A Sieve Algorithm for Prime Numbers
5.7.1 Sieve of Eratosthenes
5.7.2 Correctness
5.7.2.1 Invariant
5.7.2.2 Verification Conditions
5.7.2.3 Termination
5.7.3 Characterization of Composite Numbers
5.7.4 Refinement of the Sieve Program
5.7.4.1 Initialization
5.7.4.2 Loop Iteration Condition
5.7.4.3 Removing Multiples of p, Updating p
5.7.4.4 Reestablishing Invariant J
5.7.5 Discussion
5.8 Stable Matching
5.8.1 Formal Description of the Problem and an Algorithm
5.8.2 Correctness
5.8.3 Refinement of the Algorithm
5.9 Heavy-hitters: A Streaming Algorithm
5.9.1 Problem Description
5.9.2 An Abstract Algorithm and its Refinement
5.9.2.1 An Abstract Algorithm
5.9.2.2 Refinement
5.9.3 One-pass Algorithm for Approximate Heavy-hitters
5.9.4 The Majority Element of a Bag
5.10 Exercises
6 Graph Algorithms
6.1 Introduction
6.2 Background
6.2.1 Directed and Undirected Graph
6.2.2 Paths and Cycles
6.2.3 Connected Components
6.2.4 Labeled Graph
6.2.5 Graph Representation
6.2.6 Graph Manipulation: Merging, Pruning and Joining
6.2.6.1 Adding/Removing Nodes/Edges
6.2.6.2 Merging Nodes
6.2.6.3 Join or Replace Paths
6.2.6.4 Join Disjoint Cycles
6.2.6.5 Join Non-disjoint Cycles
6.3 Specific Graph Structures
6.3.1 Tree
6.3.1.1 Rooted Tree
6.3.1.2 Free Tree
6.3.2 Acyclic Graph
6.3.3 Bipartite Graph
6.3.4 Euler Path and Cycle
6.3.5 Hamiltonian Path and Cycle
6.4 Combinatorial Applications of Graph Theory
6.4.1 A Puzzle About Coloring Grid Points
6.4.2 Domino Tiling
6.4.3 Fermat's Little Theorem
6.4.4 De Bruijn Sequence
6.4.5 Hall's Marriage Theorem
6.5 Reachability in Graphs
6.5.1 Definition and Properties of Reachability Relation
6.5.2 An Abstract Program for Reachability
6.5.3 Correctness Proof
6.6 Graph Traversal Algorithms
6.6.1 Breadth-first Traversal
6.6.2 Depth-first Traversal
6.6.2.1 Depth-first Traversal of Tree
6.6.2.2 Properties of Preorder and Postorder Numbering
6.6.2.3 Depth-first Traversal of Directed Graph
6.6.2.4 Properties of Depth-first Traversal of Directed Graph
6.6.2.5 Visiting All Nodes of the Graph: Augmented Graph
6.6.2.6 Depth-first Traversal of Undirected Graph
6.6.3 An Application of dfs: Topological Order in Acyclic Directed Graph
6.7 Connected Components of Graphs
6.7.1 Undirected Static Graph
6.7.2 Undirected Dynamic Graph: Union–Find Algorithm
6.7.2.1 Algorithm
6.7.2.2 Optimization Heuristics
6.7.2.3 Properties of Ranks
6.7.2.4 Amortized Cost Analysis
6.7.3 Strongly Connected Components of Directed Graph
6.7.3.1 Condensed Graph
6.7.4 An Application: 2-Satisfiability
6.7.4.1 Reduction of 2-CNF Boolean Expression to a Graph
6.7.4.2 Graph Structure Determines Satisfiabilty
6.7.4.3 Truth-value Assignment
6.7.4.4 Satisfiability Algorithm
6.8 Transitive Closure
6.8.1 Transitive Closure and Matrix Multiplication
6.8.2 Warshall's Algorithm
6.8.2.1 Space Requirement for Warshall's Algorithm
6.8.3 All-pair Shortest Path Algorithm
6.8.4 Compiling a Metro Connection Directory
6.8.4.1 Definitions of x and + for the Metro Directory
6.8.4.2 Warshall's Algorithm for Metro Connection Directory
6.8.5 Transitive Closure Over Semiring
6.9 Single Source Shortest Path
6.9.1 Formal Description of the Problem
6.9.2 Shortest-path Equation
6.9.3 Single Source Shortest Path in Acyclic Graph
6.9.3.1 Maximum Segment Sum
6.9.4 Shortest Paths with Non-negative Edge Lengths
6.9.4.1 Mathematical Basis of the Algorithm
6.9.4.2 Development of the Algorithm
6.9.5 A Simulation-based Shortest Path Algorithm
6.9.5.1 Real-time Concurrent Program for Shortest Path
6.9.5.2 Simulation-Based Implementation
6.9.6 Shortest Paths with Negative Edge Lengths
6.9.6.1 Underlying Equations
6.9.6.2 Negative Cycles
6.9.6.3 Implementation
6.9.6.4 Cost Analysis
6.9.6.5 Edge Relaxation
6.10 Minimum Spanning Tree
6.10.1 Properties of Spanning Tree
6.10.2 A Fundamental Theorem About Minimum Spanning Trees
6.10.2.1 Safe Edge
6.10.2.2 Independence Among Safe Edges
6.10.2.3 A Fundamental Theorem
6.10.2.4 Abstract Algorithm for MST
6.10.3 Kruskal's Algorithm
6.10.4 Dijkstra–Prim Algorithm
6.10.5 Borůvka's Algorithm
6.11 Maximum Flow
6.11.1 Problem Specification
6.11.2 Residual Network
6.11.3 Computing a Maximum Flow
6.11.4 Max-flow Min-Cut Theorem
6.11.4.1 Algebra of Flows
6.11.4.2 Statement and Proof of Max-Flow Min-Cut Theorem
6.12 Goldberg–Tarjan Algorithm for Maximum Flow
6.12.1 Details of the Algorithm
6.12.1.1 Initialization
6.12.1.2 Push Operation
6.12.1.3 Relabel Operation
6.12.1.4 The Complete Algorithm
6.12.2 Correctness
6.12.2.1 Invariant
6.12.2.2 Preconditions of push and relabel
6.12.2.3 The Preflow is Max Flow at Termination
6.12.2.4 Termination
6.12.3 Timing Analysis
6.12.3.1 Effect of relabel
6.12.3.2 Effect of Saturating push
6.12.3.3 Effect of Non-saturating push
6.13 Exercises
6.A Appendix: Proof of the Reachability Program
6.B Appendix: Depth-first Traversal
6.B.1 Appendix: Proof of Edge-ancestor Lemma
6.B.2 Appendix: Proof of Path-ancestor Theorem
6.B.3 Appendix: Additional Properties of Depth-first Traversal
7 Recursive and Dynamic Programming
7.1 What is Recursive Programming
7.2 Programming Notation
7.2.1 Basic Data Types
7.2.2 Data Structuring: Tuple, List
7.2.2.1 Tuple
7.2.2.2 List
7.2.3 Function Definition
7.2.3.1 Binding Rules
7.2.3.2 Writing Function Definition
7.2.3.3 Multiple Equations in Function Definition
7.2.3.4 Conditional Equation
7.2.3.5 Functions Defined Using where Clause
7.2.4 Program Layout
7.2.5 Recursively Defined Functions
7.2.5.1 Length of a List
7.2.5.2 Computing Fibonacci Numbers
7.2.5.3 Computing Pairs of Fibonacci Numbers
7.2.5.4 Multiplication of Two Numbers
7.2.5.5 Greatest Common Divisor
7.2.5.6 Writing a Sequence of Function Definitions
7.2.5.7 Primitive versus General Recursion
7.2.6 Type
7.2.6.1 Type Expression
7.2.6.2 Polymorphism
7.2.6.3 Type Classes
7.2.6.4 User-defined Types
7.2.7 Pattern Matching
7.2.7.1 Pattern Matching Rules
7.2.7.2 Wildcard
7.2.8 Examples of Pattern Matching Over Lists
7.2.8.1 Elementary Functions Over Lists
7.2.8.2 List Concatenation and Flattening
7.2.8.3 Merge Sort
7.2.9 Higher Order Functions
7.2.9.1 Currying
7.2.9.2 Function foldr
7.2.9.3 Function map
7.2.10 Mutual Recursion
7.3 Reasoning About Recursive Programs
7.3.1 Fibonacci Numbers, Yet Again
7.3.2 Number of Non-zero Bits in a Binary Expansion
7.3.3 A Reversal and Concatenation Function for Lists
7.3.4 Reasoning About Higher Order Functions
7.3.4.1 A Proof About filter
7.3.4.2 Function Composition is Associative
7.3.4.3 Function map Distributes Over Composition
7.4 Recursive Programming Methodology
7.4.1 Alternative Recursive Problem Formulations
7.4.2 Helper Function
7.4.2.1 Enumerating Permutations
7.4.3 Function Generalization
7.4.3.1 Extension Heuristic for Function Generalization Over Lists
7.4.3.2 Maximum Segment Sum
7.4.3.3 Prefix Sum
7.4.3.4 List Reversal
7.4.3.5 Enumerating Permutations
7.4.4 Refining a Recursive Solution: Towers of Hanoi
7.5 Recursive Data Types
7.5.1 Tree Structures
7.5.1.1 Binary Tree
7.5.1.2 Binary Search Tree
7.5.1.3 Full Binary Tree
7.5.1.4 General Tree
7.5.2 Tree Isomorphism
7.5.2.1 Simple Isomorphism
7.5.2.2 Isomorphism of Expressions
7.5.2.3 Isomorphism of Expressions Under Idempotence
7.6 Dynamic Programming
7.6.1 Top–Down versus Bottom–Up Solution Procedures
7.6.1.1 Top–Down Solution Procedures
7.6.1.2 Bottom–Up Solution Procedures
7.6.1.3 When is Bottom–Up Preferable to Top–Down?
7.6.1.4 Encoding Bottom–Up Solutions in Haskell; Memoization
7.6.2 Optimality Principle
7.6.3 Matrix Chain Multiplication
7.6.4 Longest Common Subsequence
7.6.4.1 Dynamic Programming Solution
7.6.5 Minimum Edit Distance
7.6.5.1 Underlying Mathematics
7.6.5.2 A Program to Compute Edit Distance
7.6.5.3 A Dynamic Programming Solution
7.7 Exercises
7.A Appendices
7.A.1 Towers of Hanoi: Simulating an Iterative Solution
7.A.2 Reducing Space Usage in the lcs Computation
8 Parallel Recursion
8.1 Parallelism and Recursion
8.2 Powerlist
8.2.1 Powerlist Constructors
8.2.2 Simple Function Definitions over Powerlists
8.2.3 Laws
8.2.4 Non-standard Powerlists
8.3 Pointwise Function Application
8.3.1 Examples of Scalar Function Application
8.3.2 Powerlist of Indices
8.4 Proofs
8.4.1 Inductive Measures on Powerlists
8.4.2 Permutation Functions
8.4.3 Examples of Permutation Functions
8.4.3.1 Rotate
8.4.3.2 Swap
8.4.3.3 Permute Index
8.4.3.4 Inversion
8.4.3.5 Gray Code
8.4.3.6 Permutations Distribute over Scalar Functions
8.4.4 Correctness of Permutation Functions
8.4.4.1 Proof of revp
8.5 Advanced Examples Using Powerlists
8.5.1 fold
8.5.2 Polynomial
8.5.3 Fast Fourier Transform
8.5.3.1 Problem Description
8.5.3.2 Derivation of the Fast Fourier Transform Algorithm
8.5.3.3 Inverse Fourier Transform
8.5.3.4 Computing Product of Polynomials
8.5.4 Batcher Sorting Schemes
8.5.4.1 Batcher Odd-Even Mergesort
8.5.4.2 Elementary Facts About Sorting
8.5.4.3 Correctness of Batcher Odd-Even Mergesort
8.5.4.4 Bitonic Sort
8.5.5 Prefix Sum
8.5.5.1 Specification
8.5.5.2 Properties of Prefix Sum
8.5.5.3 A Simple Algorithm for Prefix Sum
8.5.5.4 Ladner–Fischer Algorithm
8.5.5.5 Complexity of the Ladner–Fischer Algorithm
8.5.5.6 Remarks on Prefix Sum Description
8.5.5.7 Carry-Lookahead adder
8.6 Multi-dimensional Powerlist
8.6.1 Multi-dimensional Constructors
8.6.1.1 Definitions of Multi-dimensional Constructors
8.6.1.2 Properties of Multi-dimensional Constructors
8.6.1.3 Depth, Shape
8.6.1.4 Proofs over Multi-dimensional Powerlists
8.6.1.5 Indices of Nodes in a Multi-dimensional Powerlist
8.6.2 Algorithms over Multi-dimensional Powerlists
8.6.2.1 Outer Product
8.6.2.2 Matrix Transposition
8.6.2.3 Transposition of Square Matrix
8.6.2.4 Square Matrix Multiplication
8.6.2.5 Strassen's Matrix Multiplication Algorithm
8.6.2.6 Gray Code in Multi-dimensional Powerlist
8.6.2.7 Embedding in Hypercubes
8.7 Other Work on Powerlist
8.8 Exercises
8.A Appendices
8.A.1 Proof of Correctness of inv
8.A.2 Proofs of Laws About Higher-dimensional Constructors
8.A.3 Proof of Hypercube Embedding Algorithm
Bibliography
Author's Biography
Index