From ae1b88e5244231b16dd55c998c96d561ce018682 Mon Sep 17 00:00:00 2001 From: Len Huang Date: Thu, 7 Jan 2021 23:56:41 -0500 Subject: [PATCH 1/7] initial commit --- .gitignore | 4 ++++ src/concepts/inductionintuition.md | 34 +++++++++++++++++++++++++----- 2 files changed, 33 insertions(+), 5 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..fe199e8 --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +# Default folder for mdbook build +docs +# For mac file browser +.DS_Store \ No newline at end of file diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index be5ff4f..396ce96 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -1,7 +1,12 @@ -# Thinking About Recursion Inductively + + + +# Thinking About Recursion Inductively There's a strong association between mathematical induction and recursion, especially in SML. Often times, we'll be able to use similar vocabularies when describing SML problems and mathematical induction. In particular, we're going to be use the words **base case, induction hypothesis, and induction step** to describe both types of problems. +In essence, we'll be able to approach writing SML functions the same way we approach writing induction proofs. + ## Inductive Intuition Approaching induction proofs can fall along the following line of logic: @@ -10,14 +15,22 @@ Approaching induction proofs can fall along the following line of logic: 2. Define the **inductive hypothesis**. 3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. -We can similarly apply this line of logic to solving problems with SML functions! Let's take a look at a common recursive problem. `treeSum` takes an int tree and returns the sum of all the integers in that tree. By the end of this, we'll be able to implement recursive functions with the following inductive logic: +We can similarly apply this line of logic to solving problems with SML functions! We'll look at two problems that can be solved with recursion: `fact` and `len`. + +## Factorial + +The following function implements the factorial operator in SML. ```sml -fun treeSum (Empty : int tree) : int = 0 - | treeSum (Node(L,x,R)) = treeSum(L) + treeSum(R) + x +(* REQUIRES: n >= 0 + * ENSURES: fact n ==>* (n)(n-1)...(1), or n! *) + fun fact (0 : int) : int = 1 + | fact (n : int) : int = n * fact (n - 1) ``` -> The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. Define my **inductive step** to be for a tree `T = Node(L,x,R)`. By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. If I sum all of these, I will get `treeSum(T)`. By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. +Let's think of this as a proof of extensional equivalence. I want to show that `fact` is equivalent to the mathematical definition of [factorial](https://en.wikipedia.org/wiki/Factorial). + +#### Factorial -- (1) Solve the Base Cases ## An Exploration of Tree Sums @@ -89,3 +102,14 @@ And like that, we're able to leverage mathematical induction to help us find the 1. Solve the **base cases**. 2. Define the **inductive hypothesis**. 3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. + +### More Examples + +1. Tree Sum + +```sml +fun treeSum (Empty : int tree) : int = 0 + | treeSum (Node(L,x,R)) = treeSum(L) + treeSum(R) + x +``` + +> The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. Define my **inductive step** to be for a tree `T = Node(L,x,R)`. By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. If I sum all of these, I will get `treeSum(T)`. By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. From be4a84c44a94f9852dc21dfcd03057ebb8099156 Mon Sep 17 00:00:00 2001 From: Len Huang Date: Fri, 8 Jan 2021 00:00:13 -0500 Subject: [PATCH 2/7] consolidate treeSum --- src/concepts/inductionintuition.md | 77 ++++++------------------------ 1 file changed, 15 insertions(+), 62 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index 396ce96..34f3339 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -32,52 +32,31 @@ Let's think of this as a proof of extensional equivalence. I want to show that ` #### Factorial -- (1) Solve the Base Cases -## An Exploration of Tree Sums - -Let's define `treeSum`. This function should take in an `int tree` and return the sum of all the integers in that tree. - -```sml -datatype int tree = Empty | Node of int tree * int * int +## QED -fun treeSum (T : int tree) : int = ... -``` +And like that, we're able to leverage mathematical induction to help us find the solution to part of an SML function. For some, this intuition is obvious. But for others, it isn't! A deep spiral of pure math and proving every single aspect of your code isn't usually needed. **BUT**, it will definitely be helpful to adopt this style of thinking when approaching more difficult and advanced recursion problems. Whenever you're trying to implement a recursive function in SML, remember to think inductively! -Note that in SML, the `tree` datatype is recursively defined. This is a good hint that we should be using recursive/inductive strategies to approach this problem. Consider the proof of the following theorem: +1. Solve the **base cases**. +2. Define the **inductive hypothesis**. +3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. -> **Theorem:** For all `T : int tree`, `treeSum T` is correct. +### More Examples -Let's not worry about formalizing this proof too much so that we can focus on the **inductive intuition** of it. If we were to prove this using induction, we'll need a **(1) base case, (2) induction hypothesis, and (3) induction step.** +1. Tree Sum -### 1. Solving for the Base Cases +```sml +fun treeSum (Empty : int tree) : int = 0 + | treeSum (Node(L,x,R)) = treeSum(L) + treeSum(R) + x +``` -Let's first think about proving the base case: `T = Empty`. What does it mean for `treeSum Empty` to be correct? Well, an `Empty` tree does not have any nodes, and if there are no nodes, there are no `int` values. The sum of nothing is 0. Let's write that in a proof-like manner: +> The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. Define my **inductive step** to be for a tree `T = Node(L,x,R)`. By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. If I sum all of these, I will get `treeSum(T)`. By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. > **Base Case:** `T = Empty` > > - `treeSum(Empty) ==> 0` because an `Empty` int tree does not have an int value. - -That wasn't so bad! If we have an empty node, we can't have a value there, and so the sum is 0. Before we move on to solving the recursive step, let's tie in this idea of how recursion and induction are related. In our proof, we say that `treeSum Empty` is correct when it evaluates to 0. Let's use this as an answer to how to define the base case of our function: - -```sml -fun treeSum (Empty : int tree): int = 0 -``` - -Nice job! We've leveraged inductive reasoning to help us define the base case for our recursive problem. Let's move on to something a little harder and may be less obvious than what we've done here. - -### 2. Define the Inductive Hypothesis - -The next step in our proof is to define the inductive hypothesis. Here, we'll assume the correctness of a smaller part, then use that to prove the correctness of a bigger part. More specifically, we'll be using some ideas of [structural induction](https://smlhelp.github.io/#todolinktostructuralinductionsection) for this problem. Let's elaborate more on that: - -> **Induction Hypothesis:** Assume for all `L : int tree` and `R : int tree` that `treeSum L` is correct and `treeSum R` is correct. - -Because we've shown our base case to be true, let's assume tha for the recursive structures (the left subtree `L` and the right subtree `R`), `treeSum` is correct. Just like how in induction we can use these nuggets of information to help us prove our **inductive step**, we can do the same to help us solve the SML function. - -### 3. Assume the Inductive Hypothesis to Show the Inductive Step. - -What nuggets of information do we know from the previous step, and how can we use that to help us with inductive step? We assume that both `treeSum L` and `treeSum R` are correct by the **inductive hypothesis (IH)**. Since they are correct, their outputs represent the sum of all the integers in them. For `treeSum L` is the sum of all integers in the int tree `L` and for `treeSum R` is the sum of all integers in the int tree `R`. - -We also know that since `L` and `R` are the left and right subtrees of `T`, by definition, they represent all nodes of `T` (except the root node). Then, to get sum of `T`, we just need the sum of `L`, `R`, and the value of the root node! Let's proof-ify this line of thought a bit more: - +> +> **Induction Hypothesis:** For subtrees `L, R`, `treeSum(L)` and `treeSum(R)` are correct. +> > **Inductive Step:** `T = Node(L,x,R)` > > - `treeSum L` is correct by **IH** @@ -87,29 +66,3 @@ We also know that since `L` and `R` are the left and right subtrees of `T`, by d > - `treeSum T = (treeSum L) + (treeSum R) + x` by definition of `treeSum`. > - `(treeSum L) + (treeSum R) + x` is correct by math and above logic. > - `treeSum T` is correct by substitution. - -Using the logic needed to complete the proof, we were able to arrive at how to implement our function! Let's translate the above logic into SML: - -```sml -fun treeSum (Empty : int tree) : int = 0 - | treeSum (Node(L,x,R)) = (treeSum L) + (treeSum R) + x -``` - -## QED - -And like that, we're able to leverage mathematical induction to help us find the solution to part of an SML function. For some, this intuition is obvious. But for others, it isn't! A deep spiral of pure math and proving every single aspect of your code isn't usually needed. **BUT**, it will definitely be helpful to adopt this style of thinking when approaching more difficult and advanced recursion problems. Whenever you're trying to implement a recursive function in SML, remember to think inductively! - -1. Solve the **base cases**. -2. Define the **inductive hypothesis**. -3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. - -### More Examples - -1. Tree Sum - -```sml -fun treeSum (Empty : int tree) : int = 0 - | treeSum (Node(L,x,R)) = treeSum(L) + treeSum(R) + x -``` - -> The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. Define my **inductive step** to be for a tree `T = Node(L,x,R)`. By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. If I sum all of these, I will get `treeSum(T)`. By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. From 574b9eda871165916aba79b7f252fdb504f69480 Mon Sep 17 00:00:00 2001 From: Len Huang Date: Mon, 11 Jan 2021 00:59:28 -0500 Subject: [PATCH 3/7] flesh out factorial --- src/concepts/inductionintuition.md | 124 ++++++++++++++++++++++++++--- 1 file changed, 111 insertions(+), 13 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index 34f3339..f33597c 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -3,9 +3,18 @@ # Thinking About Recursion Inductively -There's a strong association between mathematical induction and recursion, especially in SML. Often times, we'll be able to use similar vocabularies when describing SML problems and mathematical induction. In particular, we're going to be use the words **base case, induction hypothesis, and induction step** to describe both types of problems. +There's a strong association between mathematical induction and recursion, +especially in SML. Often times, we'll be able to use similar vocabularies +when describing SML problems and mathematical induction. In particular, we're +going to be use the words **base case, induction hypothesis and induction step** +to describe both types of problems. In essence, we'll be able to approach +writing SML functions the same way we approach writing induction proofs. -In essence, we'll be able to approach writing SML functions the same way we approach writing induction proofs. + + +> This page assumes an understanding of mathematical induction proofs. If you +> need a refresher on this subject, check out this +> [Wikipedia Page](https://en.wikipedia.org/wiki/Mathematical_induction). ## Inductive Intuition @@ -13,36 +22,125 @@ Approaching induction proofs can fall along the following line of logic: 1. Solve the **base cases**. 2. Define the **inductive hypothesis**. -3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. +3. Prove the **inductive step** by assuming the IH. -We can similarly apply this line of logic to solving problems with SML functions! We'll look at two problems that can be solved with recursion: `fact` and `len`. +We can similarly apply this line of logic to solving problems with SML +functions! We'll look at a problems that can be solved with recursion: `fact`. +We'll look at how thinking of it's proof relates to implementing the problem. ## Factorial -The following function implements the factorial operator in SML. +Let's say your asked to implement the following function with these specs. + +```sml +(* REQUIRES: n >= 0 + * ENSURES: fact n ==>* (n)(n-1)...(1), or n! *) + fun fact (n : int) = ... +``` + +We can think of this as a proof of extensional equivalence. I want to show that +`fact` is equivalent to the mathematical definition of +[factorial](https://en.wikipedia.org/wiki/Factorial). Let's set up this proof +and use that to help implement the function. + +### Factorial -- Want To Show + +We want to prove the following theorem: + +> For all `n` such that `n >= 0`, `fact n == n!`. + +_In other words, the `fact` function is equivalent to the mathematical_ +_factorial operator._ + +### Factorial -- (1) Solve the Base Cases + +We want our base case of `fact` to be equivalent to the base case of +mathematical factorial. Since factorial is undefined for negative numbers, +our first valid "input" to the factorial number is `0`. In other words, +`0! = 1`. Because we want our `fact` function to be equivalent, we will +define it in this way. + +```sml +(* REQUIRES: n >= 0 + * ENSURES: fact n ==>* (n)(n-1)...(1), or n! *) +fun fact(0 : int) : int = 1 +``` + +The correctness proof is as follows; + +> **Base Case: `n = 0`** +> +> - `0! = 1` by math +> - `fact 0 ==>* 1` by clause 1 of `fact`. +> - `1 = 1` as desired + +### Factorial -- (2) Define the Induction Hypothesis + +The next step of our proof is the inductive hypothesis. We want to assume +that our theorem holds for all "smaller" scenarios. In other words, + +> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k == k!`. + +### Factorial -- (3) Show the Inductive Step + +In most induction proofs, you would make a few logical deductions, apply the +IH (induction hypothesis) and prove the theorem. When we think about how to +implement `fact`, we will do something similar! Ask yourself, +**"what can I say if I assume `fact (n-1) == (n-1)!`?** (this assumption is +given by our **IH**). + +> **💡 Key Insight 💡** +> +> _When solving the recursive case of an SML function, try to ask yourself: "How would I solve this if I assume the recursive call is correct?"_ + +Well, we know that the mathematical definition of factorial is the product of +all nonnegative integers up to `n`. Note, by definition, that `n! == n * (n-1)!`. +But also note, that by our **IH**, `(n-1)! == fact (n-1)`. From here, we gain +the insight that `n! == n * fact (n-1)`. Just like in the base case, because +we want our `fact` function to be equivalent, we will define it in this way. ```sml (* REQUIRES: n >= 0 * ENSURES: fact n ==>* (n)(n-1)...(1), or n! *) - fun fact (0 : int) : int = 1 - | fact (n : int) : int = n * fact (n - 1) +fun fact(0 : int) : int = 1 + | fact(n : int) : int = n * fact (n-1) ``` -Let's think of this as a proof of extensional equivalence. I want to show that `fact` is equivalent to the mathematical definition of [factorial](https://en.wikipedia.org/wiki/Factorial). +The correctness proof is as follows: -#### Factorial -- (1) Solve the Base Cases +> **Induction Step: `n`** +> +> - `n! == n * (n-1)!` by math +> - `n! == n * fact (n-1)` by IH +> - `n! == fact n` by clause 2 of `fact` + +And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. ## QED -And like that, we're able to leverage mathematical induction to help us find the solution to part of an SML function. For some, this intuition is obvious. But for others, it isn't! A deep spiral of pure math and proving every single aspect of your code isn't usually needed. **BUT**, it will definitely be helpful to adopt this style of thinking when approaching more difficult and advanced recursion problems. Whenever you're trying to implement a recursive function in SML, remember to think inductively! +And like that, we're able to leverage mathematical induction to help us implement +an SML function. For some, this intuition is obvious. But for others, it isn't! A +deep spiral of pure math and proving every single aspect of your code isn't usually +needed. **BUT**, it will definitely be helpful to adopt this style of thinking when +approaching more difficult and advanced recursion problems. Whenever you're trying +to implement a recursive function in SML, remember to think inductively! 1. Solve the **base cases**. 2. Define the **inductive hypothesis**. -3. Assume the correctness of the **inductive hypothesis** to show the correctness of the **inductive step**. +3. Prove the **inductive step** by assuming the IH. + +## More Examples -### More Examples +Here are some more examples, with their code, thought processes, and proof outlines. + +### List Length + +```sml +fun len ([] : int list) : int = 0 + | len (x::xs) = len(xs) + 1 +``` -1. Tree Sum +### Tree Sum ```sml fun treeSum (Empty : int tree) : int = 0 From f6805759341cc0202321cc518b9842c1a619a76b Mon Sep 17 00:00:00 2001 From: Len Huang Date: Mon, 11 Jan 2021 01:09:45 -0500 Subject: [PATCH 4/7] compile factorial --- src/concepts/inductionintuition.md | 58 ++++++++++++++++++++++++++++-- 1 file changed, 55 insertions(+), 3 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index f33597c..40f59b3 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -28,6 +28,12 @@ We can similarly apply this line of logic to solving problems with SML functions! We'll look at a problems that can be solved with recursion: `fact`. We'll look at how thinking of it's proof relates to implementing the problem. +# Todo Elaborate on This Metaphor + +- Base Case == Base Case +- Induction Hypothesis == Recursive Call +- Induction Step == Recursive Case + ## Factorial Let's say your asked to implement the following function with these specs. @@ -113,8 +119,8 @@ The correctness proof is as follows: > - `n! == n * (n-1)!` by math > - `n! == n * fact (n-1)` by IH > - `n! == fact n` by clause 2 of `fact` - -And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. +> +> And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. ## QED @@ -133,6 +139,43 @@ to implement a recursive function in SML, remember to think inductively! Here are some more examples, with their code, thought processes, and proof outlines. +### Factorial (Compiled) + +#### Factorial -- Code + +```sml +(* REQUIRES: n >= 0 + * ENSURES: fact n ==>* (n)(n-1)...(1), or n! *) +fun fact(0 : int) : int = 1 + | fact(n : int) : int = n * fact (n-1) +``` + +#### Factorial -- Thought Process + +- The base case is `0`, and `0! == 1`, so we define it like that. +- Define IH to be that `fact (n-1) == (n-1)!` +- What can I say if I assume IH? +- `n * (n-1)! == n * fact(n-1)` +- So we define our recursive case like that. + +#### Factorial -- Proof + +> **Base Case: `n = 0`** +> +> - `0! = 1` by math +> - `fact 0 ==>* 1` by clause 1 of `fact`. +> - `1 = 1` as desired +> +> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k == k!`. +> +> **Induction Step: `n`** +> +> - `n! == n * (n-1)!` by math +> - `n! == n * fact (n-1)` by IH +> - `n! == fact n` by clause 2 of `fact` +> +> And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. + ### List Length ```sml @@ -143,11 +186,20 @@ fun len ([] : int list) : int = 0 ### Tree Sum ```sml +(* REQUIRES: true + * ENSURES: treeSum T ==>* the sum of all the elements of T *) fun treeSum (Empty : int tree) : int = 0 | treeSum (Node(L,x,R)) = treeSum(L) + treeSum(R) + x ``` -> The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. Define my **inductive step** to be for a tree `T = Node(L,x,R)`. By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. If I sum all of these, I will get `treeSum(T)`. By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. +- The **base case** for `treeSum` is that an `Empty` tree has a sum of 0. +- Let's define the **inductive hypothesis** to be that for some tree `T`, that `treeSum` is correct for its left subtree and right subtree. +- Define my **inductive step** to be for a tree `T = Node(L,x,R)`. + - By the definition of trees, I know that all integers in `T` are represented by the integers in `L`, `R`, and the integer `x`. + - If I sum all of these, I will get `treeSum(T)`. + - By assuming the **IH**, I can say that `treeSum L` and `treeSum R` are correct. + - Therefore, by math, I will say that `treeSum T = (treeSum L) + (treeSum R) + x` is correct by the above reasoning. +- As such, I've shown my **IS** to be correct, and thus the theorem that `treeSum T` is correct for all `T : int tree`. > **Base Case:** `T = Empty` > From fa0c4866d2fef3fb6350dd1c9c36d90e88bfff7c Mon Sep 17 00:00:00 2001 From: Len Huang Date: Mon, 11 Jan 2021 19:22:09 -0500 Subject: [PATCH 5/7] terms --- src/concepts/inductionintuition.md | 36 ++++++++++++++++++------------ 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index 40f59b3..55fcf4f 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -3,12 +3,12 @@ # Thinking About Recursion Inductively -There's a strong association between mathematical induction and recursion, -especially in SML. Often times, we'll be able to use similar vocabularies -when describing SML problems and mathematical induction. In particular, we're -going to be use the words **base case, induction hypothesis and induction step** -to describe both types of problems. In essence, we'll be able to approach -writing SML functions the same way we approach writing induction proofs. +There's a strong association between mathematical induction and recursion. +Often times, we'll be able to use similar vocabularies when describing SML +problems and mathematical induction. In particular, we're going to be use the +words **base case, induction hypothesis, and induction step** to describe both +types of problems. In essence, we'll be able to approach writing SML functions +the same way we approach writing induction proofs. @@ -28,11 +28,19 @@ We can similarly apply this line of logic to solving problems with SML functions! We'll look at a problems that can be solved with recursion: `fact`. We'll look at how thinking of it's proof relates to implementing the problem. -# Todo Elaborate on This Metaphor +## Terminology -- Base Case == Base Case -- Induction Hypothesis == Recursive Call -- Induction Step == Recursive Case +When writing an induction proof, we may use the terms **base case, induction** +**hypothesis, and induction step** to describe its general outline. When +writing a recursive SML function, we may use the terms **base case, recursive** +**call, and recursive case** to describe its general outline. Throughout this +article you'll see a very strong correspondence between these terms. + +- The **base cases** are easy to hard code to be the same as one another +- The **induction step** of a proof discusses the **recursive case** +- The **induction hypothesis** lets us reason about the **recursive call** + +We'll explore this relationship between induction and recursion with an example. ## Factorial @@ -49,7 +57,7 @@ We can think of this as a proof of extensional equivalence. I want to show that [factorial](https://en.wikipedia.org/wiki/Factorial). Let's set up this proof and use that to help implement the function. -### Factorial -- Want To Show +### 0. Want To Show We want to prove the following theorem: @@ -58,7 +66,7 @@ We want to prove the following theorem: _In other words, the `fact` function is equivalent to the mathematical_ _factorial operator._ -### Factorial -- (1) Solve the Base Cases +### 1. Solve the Base Cases We want our base case of `fact` to be equivalent to the base case of mathematical factorial. Since factorial is undefined for negative numbers, @@ -80,14 +88,14 @@ The correctness proof is as follows; > - `fact 0 ==>* 1` by clause 1 of `fact`. > - `1 = 1` as desired -### Factorial -- (2) Define the Induction Hypothesis +### 2. Define the Induction Hypothesis The next step of our proof is the inductive hypothesis. We want to assume that our theorem holds for all "smaller" scenarios. In other words, > **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k == k!`. -### Factorial -- (3) Show the Inductive Step +### 3. Show the Inductive Step In most induction proofs, you would make a few logical deductions, apply the IH (induction hypothesis) and prove the theorem. When we think about how to From 9fd445d302e82a6ddc3e2c3c6ce7bb41aa055e80 Mon Sep 17 00:00:00 2001 From: Len Huang Date: Mon, 11 Jan 2021 21:34:25 -0500 Subject: [PATCH 6/7] single equals --- src/concepts/inductionintuition.md | 41 +++++++++++++++--------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index 55fcf4f..ee5ae7e 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -61,7 +61,7 @@ and use that to help implement the function. We want to prove the following theorem: -> For all `n` such that `n >= 0`, `fact n == n!`. +> For all `n` such that `n >= 0`, `fact n = n!`. _In other words, the `fact` function is equivalent to the mathematical_ _factorial operator._ @@ -86,31 +86,32 @@ The correctness proof is as follows; > > - `0! = 1` by math > - `fact 0 ==>* 1` by clause 1 of `fact`. -> - `1 = 1` as desired +> - `1` _(the integer)_ is equivalent to `1` _(the SML `int`)_ as desired. +> In other words, `1 = 1`. ### 2. Define the Induction Hypothesis The next step of our proof is the inductive hypothesis. We want to assume that our theorem holds for all "smaller" scenarios. In other words, -> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k == k!`. +> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k = k!`. ### 3. Show the Inductive Step In most induction proofs, you would make a few logical deductions, apply the IH (induction hypothesis) and prove the theorem. When we think about how to implement `fact`, we will do something similar! Ask yourself, -**"what can I say if I assume `fact (n-1) == (n-1)!`?** (this assumption is +**"what can I say if I assume `fact (n-1) = (n-1)!`?** (this assumption is given by our **IH**). > **💡 Key Insight 💡** > -> _When solving the recursive case of an SML function, try to ask yourself: "How would I solve this if I assume the recursive call is correct?"_ +> _When solving the recursive case of an SML function, try to ask yourself: "How would I solve this if I assume the recursive call is correct?" We do this because earlier, we said that we can use the Induction Hypothesis to reason about the Recursive Calls we can make in our function._ Well, we know that the mathematical definition of factorial is the product of -all nonnegative integers up to `n`. Note, by definition, that `n! == n * (n-1)!`. -But also note, that by our **IH**, `(n-1)! == fact (n-1)`. From here, we gain -the insight that `n! == n * fact (n-1)`. Just like in the base case, because +all nonnegative integers up to `n`. Note, by definition, that `n! = n * (n-1)!`. +But also note, that by our **IH**, `(n-1)! = fact (n-1)`. From here, we gain +the insight that `n! = n * fact (n-1)`. Just like in the base case, because we want our `fact` function to be equivalent, we will define it in this way. ```sml @@ -124,11 +125,11 @@ The correctness proof is as follows: > **Induction Step: `n`** > -> - `n! == n * (n-1)!` by math -> - `n! == n * fact (n-1)` by IH -> - `n! == fact n` by clause 2 of `fact` +> - `n! = n * (n-1)!` by math +> - `n! = n * fact (n-1)` by IH +> - `n! = fact n` by clause 2 of `fact` > -> And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. +> And so we have shown for all `n` such that `n >= 0`, `fact n = n!`. ## QED @@ -160,10 +161,10 @@ fun fact(0 : int) : int = 1 #### Factorial -- Thought Process -- The base case is `0`, and `0! == 1`, so we define it like that. -- Define IH to be that `fact (n-1) == (n-1)!` +- The base case is `0`, and `0! = 1`, so we define it like that. +- Define IH to be that `fact (n-1) = (n-1)!` - What can I say if I assume IH? -- `n * (n-1)! == n * fact(n-1)` +- `n * (n-1)! = n * fact(n-1)` - So we define our recursive case like that. #### Factorial -- Proof @@ -174,15 +175,15 @@ fun fact(0 : int) : int = 1 > - `fact 0 ==>* 1` by clause 1 of `fact`. > - `1 = 1` as desired > -> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k == k!`. +> **Induction Hypothesis:** For all `k` such that `0 <= k < n`, `fact k = k!`. > > **Induction Step: `n`** > -> - `n! == n * (n-1)!` by math -> - `n! == n * fact (n-1)` by IH -> - `n! == fact n` by clause 2 of `fact` +> - `n! = n * (n-1)!` by math +> - `n! = n * fact (n-1)` by IH +> - `n! = fact n` by clause 2 of `fact` > -> And so we have shown for all `n` such that `n >= 0`, `fact n == n!`. +> And so we have shown for all `n` such that `n >= 0`, `fact n = n!`. ### List Length From b5c03fef3f141d52da03daaf049824de89686ff6 Mon Sep 17 00:00:00 2001 From: Len Huang Date: Tue, 12 Jan 2021 22:14:37 -0500 Subject: [PATCH 7/7] increasing problem --- src/concepts/inductionintuition.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/concepts/inductionintuition.md b/src/concepts/inductionintuition.md index ee5ae7e..4748cc4 100644 --- a/src/concepts/inductionintuition.md +++ b/src/concepts/inductionintuition.md @@ -185,11 +185,16 @@ fun fact(0 : int) : int = 1 > > And so we have shown for all `n` such that `n >= 0`, `fact n = n!`. -### List Length +### Increasing ```sml -fun len ([] : int list) : int = 0 - | len (x::xs) = len(xs) + 1 +(* REQUIRES: true + * ENSURES: increase L ==>* true if all elements in L are + * strictly increasing. Otherwise + * it evaluates to false. *) +fun increase ([] : int list) : bool = true + | increase (x::[]) = true + | increase (x::y::L) = x < y andalso increase(L) ``` ### Tree Sum