80 lines
4.7 KiB
Markdown
80 lines
4.7 KiB
Markdown
---
|
|
title: Understanding Induction
|
|
abstract: I am fucking stupid and I can't understand this
|
|
author:
|
|
---
|
|
|
|
## Understanding Induction
|
|
|
|
There are a few assumptions to be made when performing induction proofs (in general):
|
|
- There is *some* non-decreasing property about the category we're observing (i.e. difference between elements in a sequence, length of a list, height of a tree)
|
|
- The structure needs to be *well-defined*[^1]
|
|
|
|
And then we move on to the mechanism for proofs itself:
|
|
1. Induction Base Case: The base case(s) must be **sufficient** to cover all minimal or simplest cases of the structure.
|
|
For instance, when proving properties of lists, we often start by showing the property holds for the empty list.
|
|
|
|
2. Inductive Hypothesis: We assume that the property we're trying to prove holds for an arbitrary case. It must explicitly account for all necessary assumptions about the intermediate state of the structure.
|
|
|
|
3. Inductive Step: To establish the general inductive step, we should demonstrate that if the property holds for a given category (the induction hypothesis), it also holds for the next element (based on the non-decreasing property mentioned earlier).
|
|
|
|
We should be able to guarantee termination and avoid ambiguity in the process.
|
|
|
|
## Induction in Haskell
|
|
Given Haskell's [purity](Introduction%20to%20Functional%20Programming.md), we can perform induction proofs on most of its structure.
|
|
|
|
The non-decreasing property is defined by the data structure (`data` keyword) and/or the logic we have implemented (i.e. natural numbers - n > n-1 > 0, lists -> length, tree -> height).
|
|
|
|
We then proceed with the process mentioned above, although slightly altered as to fit the data structure category:
|
|
- **BC**: We must first establish a base case, which is a minimal instance of the structure that satisfies the property being proven. For example, this could be an empty list, a single element, or a tree with only one node. The base case must be simple enough to verify directly.
|
|
|
|
- **IH**: Assume that the property holds for some arbitrary but fixed instance of the structure. This is often referred to as the **induction step assumption**, where you posit[^2] that the property is valid for a smaller or simpler instance of the structure.
|
|
|
|
- **IS**: Using the inductive hypothesis, prove that the property holds for a larger or more complex instance of the structure.
|
|
|
|
For example, if the property holds for a list of length $n$, you need to show it holds for a list of length $n+1$. Similarly, for a tree of height $h$, show it holds for a tree of height $h+1$. This step bridges the smaller case to the larger one.
|
|
|
|
|
|
|
|
For example, when proving that reversing twice returns the original list, we can use mathematical induction:
|
|
|
|
1. **Base Case**: We need to show the property holds for the empty list (`[]`). Here, it's clear that `reverseList [] = []` and `reverseList (reverseList [])` is also `[]` since `reverseList` appends elements to the left `(++)`, and an empty list cannot be appended to anything.
|
|
|
|
2. **Inductive Step**: Suppose the property holds for a given non-empty list `x:xs` (induction hypothesis). To prove it holds for the longer list xs (`x:xs`), we apply `reverseList` and use the defined function properties as follows:
|
|
```haskell
|
|
-- Induction Hypothesis (property holds for xs)
|
|
prop_reverseTwice xs =>
|
|
|
|
-- Show that property also holds for x:xs (inductive step)
|
|
prop_reverseTwice (reverseList x:xs) =
|
|
-- Break down the list using reverseList and pattern matching
|
|
prop_reverseTwice ((reverseList xs) ++ [x]) =
|
|
-- Use the definition of concatenation, reverse, and the induction hypothesis
|
|
prop_reverseTwice (xs ++ reverseList [] ++ [x]) =
|
|
-- Use the fact that concatenating an empty list with any other list returns the original list.
|
|
prop_reverseTwice (xs ++ [x]) =
|
|
-- The property holds for xs by our induction hypothesis
|
|
True
|
|
```
|
|
By showing the base case and inductive step, we have successfully proven that `reverseList` reverses lists twice, returning the original list.
|
|
|
|
|
|
### TL;DR
|
|
1. Base case - empty list or tree
|
|
2. Inductive hypothesis - assume it works for an arbitrary list `xs` or tree (i.e.)
|
|
```haskell
|
|
data Tree a = Empty -- A tree can be empty
|
|
| Node a (Tree a) (Tree a) -- Or a node with a value and two
|
|
deriving (Show, Eq)
|
|
|
|
-- when a Tree a is Empty
|
|
|
|
```
|
|
|
|
3. Inductive Step - show that it works for a larger list `x:xs` or a non-empty tree
|
|
|
|
This process involves knowing *some* implementation details of higher-order functions (or at least a vague idea as to how they work).
|
|
|
|
|
|
[^1]: Clear rules as to how it's constructed
|
|
[^2]: to propose as an explanation **:** [suggest](https://www.merriam-webster.com/dictionary/suggest) |