Created
March 13, 2011 05:33
-
-
Save kanak/867901 to your computer and use it in GitHub Desktop.
Discrete Math Using a Computer: Chapter 04 Induction notes and exercise solutions
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#+TITLE: DiscreteMathComputer 04 - Induction | |
#+DATE: | |
#+LATEX_HEADER: \usepackage{fullpage} | |
#+LATEX_HEADER: \usepackage{tgschola} | |
#+OPTIONS: H:3 toc:nil | |
* Introduction | |
- Want to prove that every element $x$ of a set $X$ has a property $P$ | |
- i.e. $\forall x \in X, P(x)$ | |
- Direct proof for each element doesn't work because we want finitely long proof even for an infinite set | |
- We'll use: | |
+ *Mathematical Induction*: Proving properties about natural numbers | |
+ *Structural Induction*: Proving properties about lists | |
* Principle of Mathematical Induction | |
- We'll focus on induction on natural numbers | |
- Strategy: | |
+ Prove P(0). This is the *base case* | |
+ Prove that P(i) implies P(i + 1). This is the *inductive case* | |
- Since every element in the set of natural numbers can be reached by starting at 0 and repeatedly adding 1, we have a finitely long proof that the property holds for each natural number | |
** Theorem: Principle of Mathematical Induction | |
*** Statement | |
- Let $P(x)$ be a predicate on the natural numbers | |
- If $P(0)$ is true and $P(n) \rightarrow P(n + 1)$ holds $\forall n \geq 0$ then $\forall x \in N, P(x)$ is true | |
*** Proof | |
- Using axiomatic set theory | |
- "beyond the scope of this book" | |
* Examples of Induction on Natural Numbers | |
** Sum of natural numbers | |
*** Theorem: Statement | |
- $\forall n \in N, \sum_{i = 0}^n i = \frac{n (n + 1)}{2}$ | |
*** Theorem: Proof | |
- Proof is by induction on $n$ | |
**** Base case, n = 0 | |
- Left side = $\sum_{i = 0}^0 i = 0$ | |
- Right side = $\frac{0(0 + 1)}{2} = \frac{0}{2} = 0$ | |
**** Inductive case, n = k + 1 | |
- Inductive hypothesis: $\sum_{i = 0}^k i = \frac{k (k + 1)}{2}$ | |
- Add $k + 1$ to both sides of the inductive hypothesis | |
- Left side: $\sum_{i = 0}^k i + (k + 1) = \sum_{i = 0}^{k + 1} i$ by definition of $sum$ | |
- Right side: $\frac{k (k + 1)}{2} + (k + 1) = (k + 1)(\frac{k}{2} + 1) = \frac{(k + 1) (k + 2)}{2}$ | |
** Exercise 1: Exponentiation | |
*** Problem Statement | |
- Suppose $a \in \mathbb{R}$ | |
- $\forall m, n \in \mathbb{N}, a^{mn} = (a^m)^n$ | |
*** Proof | |
- Proof is by induction on $n$ | |
**** Base case, $n = 0$ | |
- Left side: $a^{m0} = a^0 = 1$ | |
- Right side: $(a^m)^0 = 1$ | |
**** Inductive case, $n = k + 1$ | |
- Inductive hypothesis: $a^{mk} = (a^m)^k$ | |
- If $a = 0$, trivially true because $\forall x \in \mathbb{N}, 0^x = 0$ (what about $0^0$ ??) | |
- Assume $a \neq 0$, multiply both sides by $a^m$ | |
+ Left side: $a^{mk} * a^k = a^{mk + m} = a^{m(k + 1)}$ | |
+ Right side: $(a^m)^k * a^m = (a^m)^{k +1}$ | |
** Exercise 2: Sum of first n odd numbers | |
*** Problem Statement | |
- Sum of first $n$ odd positive numbers is $n^2$ | |
*** Proof | |
- Proof is by induction on $n$ | |
**** Base case, $n = 0$ | |
- Left side: 0 | |
- Right side: 0 | |
**** Inductive case, $n = k + 1$ | |
- Inductive hypothesis: sum of first $k$ odd numbers is $k^2$ | |
- The $k+1$ th odd number is $2k + 1$ | |
- Add it to both sides | |
- Left side: becomes sum of first $k + 1$ odd numbers | |
- Right side: $k^2 + 2k + 1 = (k + 1)^2$ | |
** Exercise 3: Geometric Sum | |
*** Problem Statement | |
- Suppose, $a \in \mathbb{R}, a\neq 1$ | |
- $\sum_{i=0}^n a^i = \frac{a^{n+1} - 1}{a - 1}$ | |
*** Proof | |
- Proof is by induction on n | |
**** Base case, $n = 0$ | |
- Left side: $\sum_{i = 0}^0 a^1 = a^0 = 1$ | |
- Right side: $\frac{a^1 - 1}{a - 1} = 1$ | |
**** Inductive case, $n = k$ | |
- Inductive hypothesis: $\sum_{i=0}^k a^i = \frac{a^{k+1} - 1}{a - 1}$ | |
- add $a^{k + 1}$ to both sides | |
- Left side is now $\sum_{i = 0}^{k + 1} a^i$ | |
- Right side is $a^{k + 1} * \frac{a^{k + 1} - 1}{a - 1} = \frac{a^{k + 2} - a^{k + 1} + a^{k + 1} - 1}{a - 1} = \frac{a^{k + 2} - 1}{a - 1}$ | |
* Induction and Recursion | |
- Common technique for proving the properties of a recursively defined function | |
** Theorem: Factorial | |
*** Problem Statement | |
- $factorial(n) = \prod_{i = 1}^n \forall n \in \mathbb{N}$ | |
*** Proof | |
- Proof is by induction on n | |
**** Base case: n = 0 | |
- $factorial 0 = 1$ by definition of factorial | |
- $\prod_{i = 1}^0 i = 1$ (by definition of $\prod$) | |
**** Inductive case: n = k + 1 | |
- Inductive hypothesis: $factorial k = \prod_{i = 1}^k i$ | |
- $factorial (k + 1) = (k + 1) * factorial k = (k + 1) *\prod_{i = 1}^k = \prod_{i = 1}^{k + 1} i$ | |
- | |
** Exercise 4: Fibonacci | |
*** Problem Statement | |
- $\sum_{i = 1}^n fib(i) = fib (n + 2) - 1 \forall n \in \mathbb{N}$ | |
*** Proof | |
- Proof is by induction on $n$ | |
**** Base case, n = 0 | |
- Left side = $\sum_{i = 1}^0 fib(i) = 0$ (by definition of $\sum$) | |
- Right side = $fib(0 + 2) - 1 = fib(2) - 1 = fib(0) + fib(1) - 1 = 0 + 1 - 1 = 0$ | |
**** Inductive case, n = k + 1 | |
- Inductive hypothesis: $\sum_{i = 1}^k fib(i) = fib (k + 2) - 1$ | |
- Add $fib(k + 1)$ to both sides | |
- Left side: $\sum_{i = 1}^{k + 1} fib(i)$ | |
- Right side: $fib (k + 2) + fib(k + 1) - 1 = fib(k + 3) - 1$ | |
* Induction on Peano Numerals | |
** Theorem: Self-equality | |
*** Problem Statement | |
- $\forall$ x type Nat, equals x x = True | |
- Where equals is the function we defined earlier | |
*** Proof | |
- Proof is by structural induction on Peano | |
**** Base case: Zero | |
- equals Zero Zero is True (by pattern matching) | |
**** Inductive case: (Succ x) == (Succ x) | |
- Inductive hypothesis: equals x x = True | |
- equals (Succ x) (Succ x) = equals x x = True | |
** Theorem: Subtraction in Peano | |
*** Statement | |
- sub (add y x) x = y | |
- x and y are of type Peano | |
*** Proof | |
- by structural induction on x | |
**** Base case, x = Zero | |
- Left side: | |
+ sub (add y Zero) Zero | |
+ add y Zero | |
+ y | |
- Right side: | |
+ y | |
**** Inductive case, x = (Succ a) | |
- Inductive hypothesis: sub (add y a) a = y | |
- Left side: sub (add y (Succ a)) (Succ a) | |
+ sub (Succ (add y a)) (Succ a) (lemma) | |
+ sub (add y a) a | |
+ y (by inductive hypothesis | |
**** Proof of the lemma | |
- Statement: add y (Succ a) = Succ (add y a) | |
- Proof is by induction on a | |
***** Base case: a = Zero | |
- Left Side | |
+ add y (Succ Zero) | |
+ add (Succ y) Zero | |
+ Succ y | |
- Right Side | |
+ Succ (add y Zero) | |
+ Succ y | |
***** Inductive case: a = (Succ b) | |
- Inductive hypothesis: add y (Succ b) = Succ (add y b) | |
- Left Side | |
+ add y (Succ a) | |
+ add y (Succ (Succ b)) | |
+ add (Succ y) (Succ b) | |
+ Succ (add (Succ y) b) by inductive hypothesis | |
- Right side | |
+ Succ (add y a) | |
+ Succ (add y (Succ b)) | |
+ Succ (add (Succ y) b) | |
* Induction on Lists | |
- Suppose $P(xs)$ is a predicater on lists of type $[a]$ | |
- Suppose $P([])$ is true (base case) | |
- Suppose that if $P(xs)$ holds for an arbitrary xs, then $P(x:xs)$ is also true | |
- Then, $P(xs)$ holds for every list of type $[a]$ | |
** Theorem: sum (xs ++ ys) = sum xs + sum ys | |
- Proof is by induction over xs | |
*** Base Case, xs = [] | |
- Left side | |
+ sum ([] ++ ys) | |
+ sum ys | |
- Right side | |
+ sum [] + sum ys | |
+ 0 + sum ys | |
+ sum ys | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: sum (ks ++ ys) = sum ks + sum ys | |
- Left side | |
+ sum (k:ks ++ ys) | |
+ sum (k:(ks ++ ys)) by the relation between cons and append | |
+ k + sum (ks ++ ys) by definition of sum | |
+ ks + sum ks + sum ys | |
- Right side | |
+ sum xs ++ sum ys | |
+ sum (k:ks) ++ sum ys | |
+ k + sum ks + sum ys | |
** Theorem: length (xs ++ ys) = length xs + length ys | |
- Proof is by induction over xs | |
*** Base Case, xs = [] | |
- Left Side: length ([] ++ ys) = length ys | |
- Right Side: length [] + length ys = 0 + length ys = length ys | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: length (ks ++ ys) = length ks + length ys | |
- Left Side: | |
+ length (xs ++ ys) | |
+ length (k:ks ++ ys) | |
+ length (k:(ks ++ ys)) | |
+ 1 + length (ks ++ ys) | |
+ 1 + length ks + length ys | |
- Right Side: | |
+ length xs + length ys | |
+ length (k:ks) + length ys | |
+ 1 + length ks + length ys | |
** Theorem: length (map f xs) = length xs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left side: length (map f []) = length [] = 0 | |
- Right side: length [] = 0 | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: length (map f ks) = length ks | |
- Left Side | |
+ length (map f xs) | |
+ length (map f k:ks) | |
+ length ((f k) : (map f ks)) | |
+ 1 + length (map f ks) | |
+ 1 + length ks | |
- Right Side | |
+ length xs | |
+ length k:ks | |
+ 1 + length ks | |
** Theorem: map f (xs ++ ys) = (map f xs) ++ (map f ys) | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left side: map f ([] ++ ys) = map f ys | |
- Right side: (map f []) ++ (map f ys) = [] ++ (map f ys) = map f ys | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: map f (ks ++ ys) = (map f ks) ++ (map f ys) | |
- Left Side | |
+ map f (xs ++ ys) | |
+ map f (k:ks ++ ys) | |
+ map f (k:(ks ++ ys)) | |
+ (f k) : (map f (ks ++ ys)) | |
+ (f k) : ((map f ks) ++ (map f ys)) | |
+ (f k):(map f ks) ++ (map f ys) | |
+ map f (k:ks) ++ (map f ys) | |
+ (map f xs) ++ (map f ys) (which is the right side) | |
** Theorem: (map f . map g) xs = map (f . g) xs | |
- Proof is by induction on xs | |
*** Base Case, xs = [] | |
- Left side: (map f . map g) [] = map f (map g []) = map f [] = [] | |
- Right side: map (f . g) [] = [] | |
*** Inductive Case, xs = k:ks | |
- Inductive Hypothesis: (map f . map g) ks = map (f . g) ks | |
- Left Side | |
+ (map f . map g) xs | |
+ map f (map g (k:ks)) | |
+ map f ((g k) : (map g ks)) | |
+ (f (g k)) : (map f (map g ks)) | |
+ ((f . g) k) : ((map f . map g) ks) i.e. change from bracket form back to point form | |
+ ((f . g) k) : (map (f . g) ks) by inductive hypothesis | |
+ map (f . g) (k:ks) by definition of map | |
+ map (f . g) xs | |
** Theorem: sum (map (1+) xs) = length xs + sum xs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left side: sum (map (1+) []) = sum [] = 0 | |
- Right side: length [] + sum [] = 0 + 0 = 0 | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: sum (map (1+) ks) = length ks + sum ks | |
- Left Side | |
+ sum (map (1+) xs) | |
+ sum (map (1+) k:ks) | |
+ sum ((1 + k) : (map (1+) ks)) | |
+ (1 + k) + sum (map (1+) ks) | |
+ 1 + k + length ks + sum ks [by inductive hypothesis] | |
+ 1 + length ks + k + sum ks | |
+ length (k:ks) + sum (k:ks) [since length (k:ks) = 1 + length ks, and k + sum ks = sum (k:ks)] | |
+ length xs + sum xs | |
** Theorem: foldr (:) [] xs = xs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left side: foldr (:) [] xs = foldr (:) [] [] = [] | |
- Right side: xs = [] | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: foldr (:) [] ks = ks | |
- Left side | |
+ foldr (:) [] (k:ks) | |
+ k : (foldr (:) [] ks) [by applying foldr] | |
+ k : ks [by inductive hypothesis] | |
+ xs | |
** Theorem: map f (concat xss) = concat (map (map f) xss) | |
- Where xss is list of lists | |
- Proof is by induction on xss | |
*** Base case: xss = [] | |
- Left side: | |
+ map f (concat xss) | |
+ map f (concat []) | |
+ map f [] | |
+ [] | |
- Right side: | |
+ concat (map (map f) []) | |
+ concat [] | |
+ [] | |
*** Inductive case: xss = ks:kss | |
- Inductive hypothesis: map f (concat kss) = concat (map (map f) kss) | |
- Left Side: | |
+ map f (concat (ks:kss)) | |
+ map f (ks ++ concat kss) | |
+ (map f ks) ++ map f (concat kss) | |
+ (map f ks) ++ (concat (map (map f) kss)) [by induction hypothesis] | |
+ concat ((map f ks):(map (map f) kss)) [ by definition of concat] | |
+ concat (map (map f) (ks:kss)) | |
+ concat (map (map f) xs) | |
** Theorem: length (xs ++ (y:ys)) = 1 + length xs + length ys | |
- Direct Proof | |
- Left Side: | |
+ length (xs ++ (y:ys)) | |
+ length xs + length (y:ys) | |
+ length xs + 1 + length ys | |
** Exercise 9 | |
- (Exercises 5,6,7,8 are about proving theorems that I proved while reading) | |
- Theorem: sum (map (k +) xs) = k * length xs + sum xs | |
- Proof is by induction on xs | |
*** Base case: xs = [] | |
- Left side: sum (map (k +) []) = sum [] = 0 | |
- Right side: k * length [] + sum [] = k * 0 + 0 = 0 | |
*** Inductive case: xs = y:ys | |
- Inductive Hypothesis: sum (map (k +) ys) = k * length ys + sum ys | |
- Left side: | |
+ sum (map (k +) xs) | |
+ sum (map (k +) (y:ys)) | |
+ sum ((k + y) : (map (k +) ys)) | |
+ k + y + sum (map (k +) ys) | |
+ k + y + k * length ys + sum ys | |
+ k * 1 + k * length ys + y + sum ys | |
+ k (1 + length ys) + sum (y:ys) | |
+ k * length xs + sum xs | |
* Functional Equality | |
** Definition | |
- Equality: If you give two functions/algorithms the same input, they provide the same output | |
*** Intensional Equality | |
- f and g are intensionally equal if definitions are identical | |
- i.e. go through the source and it is exactly identical | |
*** Extensional Equality | |
- f and g are extensionally equal if | |
+ Have the same type a -> b | |
+ f x = g x for all well typed arguments | |
- "we are almost always interested in extensional equality" | |
** Theorem: foldr (:) [] = id | |
- earlier we proved by induction that foldr (:) [] xs = xs for all lists xs | |
- If we can prove that id xs = xs for all xs (trivial, by definition of id) | |
- then we know that foldr (:) [] = id | |
** Theorem: map f . concat = concat (map (map f)) | |
- Proved earlier by induction on xss, i.e. list of lists | |
- Note that "concat (map (map f))" is not well typed! | |
- same dealio | |
** Exercise: Prove that ++ is associative | |
- i.e. xs ++ (ys ++ zs) = (xs ++ ys) ++ zs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left side: [] ++ (ys ++ zs) = ys ++ zs | |
- Right side: ([] ++ ys) ++ zs = ys ++ zs | |
*** Inductive case, xs = k:ks | |
- Inductive hypothesis: ks ++ (ys ++ zs) = (ks ++ ys) ++ zs | |
- Left Side: | |
- xs ++ (ys ++ zs) | |
- (k:ks) ++ (ys ++ zs) | |
- k:(ks ++ (ys ++ zs)) | |
- k:((ks ++ ys) ++ zs) by inductive hypothesis | |
- k:(ks ++ ys) ++ zs (relation between : and ++) | |
- ((k:ks) ++ ys) ++ zs | |
- (xs ++ ys) ++ zs | |
** Exercise: Prove that sum . map length = length . concat | |
- To prove that the two functions are equivalent, we consider arbitrary argument xss of type [ [ a ] ] | |
- Proof is by inductio on xss | |
*** Base case, xss = [] | |
- Left Side: | |
+ sum . map length [] | |
+ sum [] | |
+ 0 | |
- Right Side: | |
+ length . concat [] | |
+ length [] | |
+ 0 | |
*** Inductive case, xss = ks:kss | |
- Inductive Hypothesis: sum (map length kss) = length (concat kss) | |
- Left Side: | |
+ sum (map length xss) | |
+ sum (map length (ks:kss)) | |
+ sum ((length ks) : (map length kss) | |
+ (length ks) + sum (map length kss) | |
+ (length ks) + length (concat kss) | |
+ length (ks ++ (concat kss)) | |
+ length (concat ks:kss) | |
+ length (concat xss) | |
* Pitfalls and Common Mistakes | |
** Exercise: All horses have the same color faulty proof | |
- Tricky problem! | |
- The problem arises in inductive step with n = 2 | |
- the two sets each have one horse | |
- proof asks us to pick a horse that is in both sets | |
- there is no horse that is in both sets | |
* Limitations of Induction | |
- set must be countably infinite | |
- *ordinary induction cannot prove the properties of infinite objects, it just proves the properties of an infinite number of objects* | |
- i.e. you don't prove something about P(infinity), you just show that for any P(n), n is finitely large, P holds | |
- e.g. proving that reverse (reverse) = id is only true for finite lists | |
- for infinite lists, reverse returns bottom | |
- problem is that infinite lists cannot be constructed in a finite number of steps, which is the key to making induction work | |
** Exercise 14: Length constraint in concat xss = foldr (++) [] xss | |
- xss must be finite for concat to yield a meaningful value | |
** Exercise 15: show reverse (reverse [1,2,3]) = [1,2,3] | |
- reverse [3,2,1] = [1,2,3] | |
** Exercise 16: Prove reverse (xs ++ys) = reverse ys ++ reverse xs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left Side: reverse (xs ++ ys) = reverse ([] ++ ys) = reverse ys | |
- Right Side: reverse ys ++ reverse [] = reverse ys ++ [] = reverse ys | |
*** Inductive case, xs = k:ks | |
- Inductive Hypothesis: reverse (ks ++ ys) = reverse ys ++ reverse ks | |
- Left Side: | |
+ reverse (xs ++ ys) | |
+ reverse (k:ks ++ ys) | |
+ reverse (k:(ks ++ ys)) | |
+ reverse (ks ++ ys) ++ [k] | |
+ reverse ys ++ reverse ks ++ [k] [by inductive hypothesis] | |
+ reverse ys ++ reverse (k:ks) | |
+ reverse ys ++ xs | |
** Exercise 17: Prove that reverse (reverse xs) = xs | |
- Proof is by induction on xs | |
*** Base case, xs = [] | |
- Left Side: reverse (reverse []) = reverse [] = [] | |
- Right Side: [] | |
*** Inductive case, xs = k:ks | |
- Inductive Hypothesis: reverse (reverse ks) = ks | |
- Left Side: | |
+ reverse (reverse (k:ks)) | |
+ reverse (reverse ks ++ [k]) | |
+ reverse [k] ++ reverse (reverse ks) [result from ex 16] | |
+ [k] ++ ks [by inductive hypothesis] | |
+ k:ks | |
+ xs | |
** Exercise 18: Why doesn't Ex 17's result hold for infinite lists | |
- reverse never terminates | |
* Suggestions for Further Reading | |
- Concrete Mathematics | |
- Problem Solving Strategies by Engel | |
- Bird-Meertens calculus | |
* Review Exercises | |
** Ex 19: length (concat xss) = sum (map length xss) for finite xss | |
- Proof is by induction on xss | |
*** Base case, xss = [] | |
- Left side: length (concat []) = length [] = 0 | |
- Right side: sum (map length []) = sum [] = 0 | |
*** Inductive case, xss = ks:kss | |
- Inductive hypothesis: length (concat kss) = sum (map length kss) | |
- Left Side: | |
+ length (concat (ks:kss)) | |
+ length (ks ++ concat kss) | |
+ length ks + length (concat kss) | |
+ length ks + sum (map length kss) | |
+ sum ((length ks) : (map length kss)) | |
+ sum (map length (ks:kss)) | |
** Ex 20: Or | |
- Problem statement: "or" defined over an argument that has an arbitrary number of elements delivers True if True occurs as one of the elements of its argument | |
- Long-winded way of saying if or is passed a list that has a True in it, then it returns True | |
- Proof is by induction on the list argument, xs | |
*** Base Case: xs = [True] | |
- or [True] | |
- True || or [] | |
- True (because || short circuits) | |
*** Inductive Case: xs = y:ys, xs is of length n + 1 | |
- Inductive hypothesis: On lists of length n containing "True", or works correctly | |
- or [y:ys] | |
- y || (or ys) | |
- If y is true, then return True immediately by short-circuit | |
- otherwise, the True must be in ys so we have to evaluate (or ys) | |
- but ys is a list of length n containing True so, by inductive hypothesis, we return True | |
** Ex 21: And | |
- And returns true if all the elements in its argument are True | |
- Proof is by induction on the list argument, xs | |
- (Actually, it's on n, which is the size of the list) | |
*** Base Case: xs = [True] | |
- and [True] = True && and [] = True && True = True | |
*** Inductive Case: xs = y:ys, xs is of length n + 1 | |
- Inductive Hypothesis: For lists sized n containing all True, "and" returns True | |
- Left Side: | |
+ and (y:ys) | |
+ y && (and ys) | |
+ (and ys) [since xs is a list of all True, and y is an element of xs] | |
+ True [inductive hypothesis] | |
** Ex 22: Using max, write maximum | |
#+begin_src haskell | |
maximum :: (Ord a) => [a] -> a | |
maximum = foldr1 max | |
#+end_src | |
** Ex 23: Prove that maximum, written in Ex22 has a property | |
- Property: (maximum xs) >= x, x is an arbitrary element of xs | |
- Proof is by contradiction | |
- Suppose (maximum xs) = y, and y < x for some x in xs | |
+ if y occurred ahead of x then max x y returned y | |
+ if x occurred ahead of y then max y x returned x | |
+ neither is possible if y < x assuming that max is correct | |
** Ex 24: Function that givem a sequence of non-empty sequences, delivers the sequence made up of the first elements of those non-empty sequences | |
#+begin_src haskell | |
firstElts :: [[a]] -> [a] | |
firstElts = map head | |
#+end_src | |
** Ex 26: Prove that concat = foldr (++) [], assuming that lists are finite | |
- Proof is by induction on the argument to concat, xss which is a list of lists | |
*** Base case: xss = [] | |
- Left side: concat [] = [] | |
- Right side: foldr (++) [] [] = [] | |
*** Inductive case: xss = ks:kss | |
- Inductive hypothesis: concat kss = foldr (++) [] kss | |
- Left side: | |
+ concat (ks:kss) | |
+ ks ++ concat kss [by definition of concat] | |
+ ks ++ (foldr (++) [] kss) | |
+ foldr (++) [] (ks:kss) [by definition of foldr] | |
+ foldr (++) [] xss | |
** Ex 27: Define and using && and foldr | |
#+begin_src haskell | |
and :: [Bool] -> Bool | |
and = foldr (&&) True | |
#+end_src |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment