#
#
In this Auxiliary we’ll wend our way into induction by way of looking at sequences and recursion. Induction is a very important concept seen all over higher math and computer science. Induction seems odd at first glance. It seems to be saying, “We know this case is true, so we’ll say the very next case is true also. And then we’ll just continue doing this until…” Right. So we’ll take apart and see why it actually works.
It’s Tuesday afternoon and the siblings meet in their usual study room at the library to go over their honors computer science course assignments. Yesterday, Professor Chandra gave the first of the week’s three lectures where she introduced the topic of mathematical induction. She had made the upcoming week’s lecture notes and a homework assignment available at the class’ GitHub repository last Friday. The von der Surwitzs are going over their own initial annotations to the lecture notes, as well as comparing their assignment code so far…
But before we join their discussion, we’ll first start out with a key piece of math logic behind the whole idea of induction starting with modus ponens. The von der Surwitzes got most of this material in Monday’s lecture, and reading on in the notes, they’re now ready to discuss it…
Modus ponendo ponens … the way that affirms by affirming, mode that affirms, Latin
or the law of detachment that says
- we start with a conditional premise, e.g., if
$R$ , then$B$ , or,$R$ implies$B$ , ($R ⊃ B\;$ )[fn:4] and we consider it to be true, then - we consider the antecedent (first half) of the conditional premise
$R ⊃ B\;$ , i.e.,$R$ as a stand-alone premise that is also true, -
therefore, we logically conclude the consequent of the
initial conditional premise,
$B$ , is true as a stand-alone too.
e.g.,
-
If you are
$R\!$ eading this, then you must be$B\!$ right ($R ⊃ B\;\;$ ) - Yes, you are
$R\!$ eading this, ($R$ ). - Therefore[fn:5], you must be
$B\!$ right ($\therefore B\;$ ).
This can also be written as
R implies B, and R is true, implies (therefore) B is true.
Modus ponens is called the law of detachment because after asserting that both the conditional premise and its antecedent are true we then detach the consequent from the conditional premise as a stand-alone truth in and of itself[fn:6].
Modus ponens is a rule of inference that says anytime we can assert
the truth of the two premises, namely,
- cite:&bender2010lists
⇲ This was right at the end of Dr. Chandra’s intriguing lecture in class on Friday…
⌜ If we have a bag of marbles, and each marble seems to be a different color, and we empty them out on the floor in a straight line, could we make any sense out of their order? Using our imagination, sure, why not? For just that first pouring-out we could make up any story we wanted about the order we see. But we would only have to dump out the marbles one more time to see our imaginings were false. Why? Because they would invariably come out in a different order. And if we repeated this dumping out over and over we would see only random order, that is, no rhyme or reason to how they’re lining up from one dump to the next.
But let’s say we have “magic” marbles that do in fact come out of the
bag in a certain order. Yes, it might be interesting to know why they
have this self-ordering thing going on. Is there some machine in the
bag that’s sending them out in a particular order? So this week we’re
going to look at something deeper with order. What if creating a
sequence were based on a formula or algorithm, and not just some
built-in ordering principle that we give it with a Haskell Ord
instance? What if we could create an ordered sequence by applying a
formula?
Now, we know about sequences from Haskell lists, and in math a sequence is defined as an enumerated collection of objects in which repetitions are allowed and order matters … that’s a quote from the Wikipedia page on sequences. And no, let’s not confuse sequences and series. In math they’re not interchangeable. A series in math is a summation of an infinitely many quantities to some starting quantity. We’ll see more of them later. So going forth, we’re going to see how sequences can be created. One way is through recurrence relationships, where one element is built from the previous element. We’ll take a look at some things you saw in basic algebra but probably didn’t realize were about sequences and recurrence. ⌟
At first glance, the first homework problem seems trivial to the von der Surwitzes
⇲ How high would you be if you
climbed a certain number of steps, e.g.,
𝔘𝔱𝔢: The steps are all the same so their order doesn’t really
matter. That’s obvious.
𝔘𝔴𝔢: Right, and we just enumerate them with the natural
numbers. Gosh, I don’t think I’ll ever get “enumerate with natural
numbers” out of my head again.\
[Laughter] \
𝔘𝔯𝔰𝔲𝔩𝔞: So we don’t need to take the
Ursula had plugged her laptop into the big monitor on the wall. She pulled up her homework
stepsAltCalc steps =
let stepinches = 8 -- 8 inch step height basealt
basealt = 800 -- 800 feet base altitude
in ((stepinches * steps) / 12) + basealt -- divide by 12 for feet
stepsAltCalc 127884.6666666666666
𝔘𝔱𝔢: So like the professor said, the take-away here is that when we
declare variables like stepinches and basealt inside the let and
in, they’re visible only inside that let...in structure and never
outside them.
𝔘𝔯𝔰𝔲𝔩𝔞: And then she asks if we can rewrite it with another
let...in inside the first one, right? And the stuff inside the
nested let...in can’t be seen by the outside, but the outside
let...in can be seen by the inside.
And so they did another version of stepsAltCalc
stepsAltCalc2 steps =
let basealt = 800
stepasfeet = 8/12
in
let feethigh = stepasfeet * steps
in feethigh + basealt
stepsAltCalc2 127884.6666666666666
𝔘𝔴𝔢: And then we still need to tame those decimal places. What do you think?
They then followed the professor’s link to a stackoverflow question, as well as an article on rounding in Haskell. They studied them for a while, then traded glances.
𝔘𝔴𝔢: Sometimes I can’t tell if Professor Chandra is, yeah,
was heißt zerstreut, geistesabwesend?
𝔘𝔯𝔰𝔲𝔩𝔞: Absent-minded? \
𝔘𝔴𝔢: Right. Absent-minded. \
𝔘𝔯𝔰𝔲𝔩𝔞: Why? \
𝔘𝔴𝔢: Well, do you remember she’s talking about rounding, but then
she’s off on this tangent about how [writing on the board] 51, is actually
fromIntegral 51 to the system. \
𝔘𝔯𝔰𝔲𝔩𝔞: And [paging through her written notes] right, 3.14 is
actually, ahh, here it is: fromRational 3.14 internally.
Ursula then typed this in at the REPL
fromRational 3.143.14
𝔘𝔴𝔢: Get the type for it.
Ursula then typed in
:t fromRational 3.14fromRational 3.14 :: Fractional a => a
𝔘𝔴𝔢: And get the type for an integer, non-decimal number, can you?
𝔘𝔯𝔰𝔲𝔩𝔞: [complies] Got it.
:t fromIntegral 1fromIntegral 1 :: Num b => b
𝔘𝔴𝔢: [slapping his thighs and exhaling loudly] Okay bright sisters,
what does all this mean?
𝔘𝔯𝔰𝔲𝔩𝔞: [reading her notes] Well, for one it means you’re not really
ever dealing with just the naked numbers, because they’re always
packaged with either fromIntegral for a non-decimal number and
fromRational with a decimal number. \
𝔘𝔱𝔢: So the naked literal numbers are part of the type class system,
it’s got the class methods fromIntegral and fromRational
involved. \
𝔘𝔯𝔰𝔲𝔩𝔞: Okay, let’s get back to the example code. Here, look
[pulling up the stackoverflow example on the monitor]
round' :: Double -> Integer -> Double
round' num sg = (fromIntegral . round $ num * f) / f
where f = 10^sg
She evaluated it, then ran a test case
round' 884.6666666666666 2884.67
𝔘𝔱𝔢: [going to the board and writing ] So as the professor explained
it, you always start at the inner-most operation. That would the
num * f. So we know num is a Double. Right? I mean it’s declared
as one in the type declaration. And (*) is a binary operation of
type Num a => a -> a -> a.
𝔘𝔴𝔢: So we can assume that f becomes a Double because they have
to be of the same type a. \
𝔘𝔯𝔰𝔲𝔩𝔞: And then we look at the division [typing into the REPL]
: (/)(/) :: Fractional a => a -> a -> a
𝔘𝔯𝔰𝔲𝔩𝔞: [continuing] So just (num * f) / f would be division of a
Double by a Double since the class Fractional has an instance
Fractional Double [typing into the REPL]
:i Fractionaltype Fractional :: * -> Constraint
class Num a => Fractional a where
(/) :: a -> a -> a
recip :: a -> a
fromRational :: Rational -> a
{-# MINIMAL fromRational, (recip | (/)) #-}
-- Defined in ‘GHC.Real’
instance Integral a => Fractional (Ratio a)
-- Defined in ‘GHC.Real’
instance Fractional Float -- Defined in ‘GHC.Float’
instance Fractional Double -- Defined in ‘GHC.Float’
𝔘𝔴𝔢: But now we need to put the numerator through round [Ursulu
types into the REPL]
:t roundround :: (RealFrac a, Integral b) => a -> b
𝔘𝔴𝔢: [continuing] Right, so the output of round will have an
instance of Integral. But we’re trying to divide…
𝔘𝔱𝔢: [writing on the board] (/) demands that the result of round
has to have the same as the denominator f :: Double. \
𝔘𝔯𝔰𝔲𝔩𝔞: [typing into the REPL]
:i Integraltype Integral :: * -> Constraint
class (Real a, Enum a) => Integral a where
quot :: a -> a -> a
rem :: a -> a -> a
div :: a -> a -> a
mod :: a -> a -> a
quotRem :: a -> a -> (a, a)
divMod :: a -> a -> (a, a)
toInteger :: a -> Integer
{-# MINIMAL quotRem, toInteger #-}
-- Defined in ‘GHC.Real’
instance Integral Word -- Defined in ‘GHC.Real’
instance Integral Integer -- Defined in ‘GHC.Real’
instance Integral Int -- Defined in ‘GHC.Real’
𝔘𝔯𝔰𝔲𝔩𝔞: [continuing] And since there is no instance of Double in
Integral. We can’t go into the Integral b => b and pull out a
Double.
𝔘𝔴𝔢: So the numerator part won’t work as is. \
𝔘𝔯𝔰𝔲𝔩𝔞: [typing into the REPL] It shouldn’t.
:t (round (844.666 * 100.0)) / 100.0(round (844.666 * 100.0)) / 100.0 :: (Integral a, Fractional a) => a
The siblings study this for a while.
𝔘𝔴𝔢: Try an example.
𝔘𝔯𝔰𝔲𝔩𝔞: [types into the REPL] Got it. But this should blow up.
(round (844.666 * 100.0)) / 100.0<interactive>:208:1-33: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘print’
prevents the constraint ‘(Show a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance (Show a, Show b) => Show (Either a b)
-- Defined in ‘Data.Either’
instance Show a => Show (Ratio a) -- Defined in ‘GHC.Real’
instance Show Ordering -- Defined in ‘GHC.Show’
...plus 25 others
...plus 82 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In a stmt of an interactive GHCi command: print it
𝔘𝔴𝔢: Now put in the fromIntegral in front of round in the
numerator. Use some actual numbers.
𝔘𝔯𝔰𝔲𝔩𝔞: [typing] Exactly.
(fromIntegral (round (844.666 * 100.0))) / 100.0844.67
𝔘𝔱𝔢: Of course. It works now.
𝔘𝔯𝔰𝔲𝔩𝔞: [typing] Let me do a type on this. \
:t (fromIntegral (round (844.666 * 100.0)))(fromIntegral (round (844.666 * 100.0))) :: Num b => b
𝔘𝔴𝔢: Yes!
𝔘𝔱𝔢: We get something that has an instance in Num and will do
division. \
𝔘𝔴𝔢: That’s because fromIntegral is magical, right? \
[Laughter.]
𝔘𝔱𝔢: No it’s because [searching her notes] because [reading]
fromIntegralconverts from anyIntegraltype into aNumtype.
𝔘𝔴𝔢: [pointing at the code] Which does include Double like we need
to be in the numerator of Double dividing Double.
The siblings surveyed the code and then looked at each other with blank face.
𝔘𝔴𝔢: And why was all this in and out of types and classes necessary?
𝔘𝔱𝔢: Well, like she said, it’s because having types controlling how
they play together is a logical entailment of working with numbers
on a computer. \
𝔘𝔯𝔰𝔲𝔩𝔞: She said other languages tend to coerce things to work
without understanding all the consequences. That’s all we can say at
this point, I suppose. \
𝔘𝔱𝔢: I suppose we’ll understand it more as we go along. \
𝔘𝔴𝔢: Time for a break.
They visited the campus student center where they all got hot chocolates. While enjoying their drinks, they discussed some of the things Professor Chandra had said about how they were getting a preview of what the incoming university Freshman students are hit with in the Computer Science program. She had said their department — like many other schools — had a high flunk-out, major-change rate, which she believed was attributable to the math of computer science being completely new.
𝔘𝔱𝔢: She also said a lot of new students come into comp-sci with
completely wrong ideas about what computer science studies are
about.
𝔘𝔯𝔰𝔲𝔩𝔞: Yeah, they’re expecting to learn a bunch of programming
hacks for phone apps or video games, and instead they’re hit with
applied math. \
𝔘𝔴𝔢: She floored me when she said you can go a whole semester and
not even touch a computer. It’s all just applied math theory. \
[Rueful murmurs of acknowledgement.] \
𝔘𝔱𝔢: Well, I think we’re all grateful to be getting some of it here
before college. \
𝔘𝔯𝔰𝔲𝔩𝔞: It’s not like regular math where you get at least ten years,
but it’s better than nothing. \
𝔘𝔴𝔢: Reduces that shock. \
[Murmurs of agreement.]
Upon returning Ursula scrolled to the next problem
⇲ If a population increases at a rate
of
@@html:<span
class=”fraktur”>@@𝔘𝔯𝔰𝔲𝔩𝔞: So again we’ll
probably use let or where.
@@html:<span
class=”fraktur”>@@𝔘𝔱𝔢: This is one of those
“compound interest rate” calculator things. @@html:<font color =
“#111”><span class=”fraktur”>@@𝔘𝔴𝔢: [writing on
the board] Right. First, the rate
\begin{align*} rate &= 1.5\% \;\: \text{per year} \[.5em] &= \frac{1.5}{100} \[.5em] &= 0.015 \end{align*}
@@html:<span
class=”fraktur”>@@𝔘𝔴𝔢: [continuing] Or the
factor of
𝔘𝔱𝔢: And this
time we don’t really care about what $P0$ is. \
𝔘𝔴𝔢: [writing]
No, just how long in years until there’s a doubling.
\begin{align*} P(t) &= P0 ⋅(1.015)t \end{align*}
𝔘𝔴𝔢: [continuing] So it’s that initial population times two because it’s doubled
\begin{align*} P(t) &= 2P0 \;\; \text{for} \;\; t = ? \end{align*}
𝔘𝔴𝔢: [continuing] So now we just sub in. And we use $log10$ to deal
with the
\begin{align*}
2P0 &= P0 ⋅(1.015)t \quad\quad \ldots \text{factor out
𝔘𝔯𝔰𝔲𝔩𝔞: [typing] Let me just plug this in to see what it gives
us. [going out on the Internet to look up how Haskell does base-10
logarithms] Okay, it’s logBase and then two parameters, the first is
the base you want, the second the number you want done — and I’ll
run it through the decimal-tamer
round' ((logBase 10 2) / (logBase 10 1.015)) 246.56
𝔘𝔴𝔢: Do we need to code this?
𝔘𝔱𝔢: Nah. I think she just wanted to jar our memory with the basic
$N = N0 (1 + 4)t\;\;$ situation and exponential functions. All right,
next one.\
As was noted, the question came from Serge Lang’s Basic Mathematics. The professor had reserved the book at the university library and encouraged the students to peruse it and note his formal style in describing very basic pre-Algebra material
A chemical substance disintegrates
in such a way that it gets halved every
𝔘𝔯𝔰𝔲𝔩𝔞: So look at this org-mode table she gave us. [scrolling down]
#+NAME: ratetable | 0 min | 10 min | 20 min | 30 min | 40 min | 50 min | | 20.0 | 10. | 5. | 2.5 | 1.25 | 0.625 | #+TBLFM: @2$2..@2$> = @2$-1/2
𝔘𝔴𝔢: She doesn’t expect
us to learn that sort of Emacs spreadsheet stuff, does she?
𝔘𝔱𝔢: No, I think she
just wants to show us — once again — how getting the math out of
books and paper and your brain and onto the computer is what this is
all about. \
𝔘𝔴𝔢: You’re not done
until the math’s been turned into code. \
[murmurs of agreement] \
𝔘𝔴𝔢: [continuing] But
still it’s cool to know this stuff. Remember early on she showed us
all the org-mode stuff about being able to chain things together. So
you can take this table and plug it in other places. It’s modular. \
𝔘𝔯𝔰𝔲𝔩𝔞: Yeah, sort of
like when she showed us how to pipe things at the command line. \
𝔘𝔱𝔢: Right. But I think
Haskell will take up all of our time for the immediate future. Linux
and Emacs will have to wait. \
[murmurs of agreement] \
𝔘𝔴𝔢: So once again,
we’re supposed to recall what we know about geometric
progression. \
𝔘𝔱𝔢: So following the
link to the Wikipedia page, she wants us to understand that this is a
form of recursion. \
𝔘𝔯𝔰𝔲𝔩𝔞: Yes, we’re
slowly easing into, being funneled into the idea of recursion. \
[murmurs of agreement] \
𝔘𝔱𝔢: So does everybody
have a basic understanding of recursion? \
𝔘𝔴𝔢: Yeah, it’s just
the idea that you
𝔘𝔯𝔰𝔲𝔩𝔞: But remember
that talk she gave about proofs?
[murmurs of acknowledgement] \
𝔘𝔱𝔢: All right, let’s
tackle the Bird book. [pulling Richard Bird’s Thinking Functionally
with Haskell and opening it to a bookmarked page] So we’re supposed
to read these sections and try out the code. It’s supposed to get us
prepared from induction. \
𝔘𝔴𝔢: That’s on reserve,
right? \
[Ute nods.] \
𝔘𝔴𝔢: Did you read it
yet? \
𝔘𝔱𝔢: Yes, and it’s
fairly straightforward. \
𝔘𝔯𝔰𝔲𝔩𝔞: I read her
notes on this and … ja, verstehe nur Bahnhof.[fn:8]
𝔘𝔱𝔢: We covered that
chapter in Learn You… on recursion[fn:9]. [murmurs of agreement]
All right, so this first part goes over how to set up an alternative
version of the natural numbers. You might want to pull up file,
Ursula, and code this in [writing on the board] data Nat = Zero |
Succ Nat
𝔘𝔯𝔰𝔲𝔩𝔞: [typing] Got
it. Evaluating.
data Nat = Zero | Succ Nat𝔘𝔯𝔰𝔲𝔩𝔞: [continuing] So
reading the text I’m getting that this is a data declaration where you
get a choice of either a Zero or a Succ Nat. That much is
clear.
𝔘𝔱𝔢: She didn’t go over
this in class, right? \
Then they went on in the lecture notes
𝔘𝔱𝔢: Okay, next. Here’s the pictures of the strange broccoli and the
sunflower head she showed us in class. There’s supposed to be a
pattern and she wanted us to think about it. Without looking ahead in
the notes.
𝔘𝔯𝔰𝔲𝔩𝔞: I had no idea where to go on that one. Anyone have any luck?
\
𝔘𝔴𝔢: Maybe. I looked it up and it’s got something to do with what
they call the Fibonacci sequence. \
𝔘𝔱𝔢: Yeah, I’ve heard of it, but that’s about all. \
𝔘𝔴𝔢: I just quickly looked at it, but basically it’s a sequence of
numbers that you can build according to a rule, a formula. [He got up
and went to the whiteboard and started to write.] So you start the
sequence with
They then took a look on the monitor at the Wikipedia article called Fibonacci number, but when they got to the definition, they got stuck
The Fibonacci numbers may be defined by the recurrence relation
\begin{align*} Fn &= 0, F1 = 1 \[.5em] Fn &= Fn-1 + Fn-2 \quad \text{for} \;\; n > 1 \end{align*}
They decided that this was some new sort of piecewise function, although they weren’t sure. They followed the link to recurrence relation and studied it, but didn’t quite understand the definition. However, they skipped on to the examples and found the formula for factorial
\begin{align*} 0! &= 1\;, \[.5em] n! &= n(n-1)! \quad \text{for}\;\; n> 0 \end{align*}
𝔘𝔱𝔢: [getting up and writing on the whiteboard] Okay, remember the definition of the absolute value function? [continuing on the board]
\begin{align*}
| x | = |
\begin{cases}
x, & \text{if
This is two-part just like factorial is is all I’m saying.
Uwe, Ursula: [murmurs of agreement] \
𝔘𝔱𝔢: So the
\begin{align*} 2! &= 2(2-1)! &= 2(1)! &= 2(1) &= 2 \end{align*}
Much simpler would be your feet and legs going up a flight of steps, each step the same as the last, except that it’s higher and more forward than the last. With the certainty of one step being a given amount up and over the other we would be able to, e.g., calculate our altitude given how many steps we had climbed.
Anytime we have a sequence of things following a certain regular pattern from one to the next, this “one to the next” phenomenon can be leveraged. This means we may figure out a “solution,” in that we create a formula to compute any element in the sequence.
Consider the factorial of a number,
fac :: (Integral a) => a -> a
fac 0 = 1
fac n = n * fac (n - 1)If you’ve covered Chapter 5 Recursion of LYAHFGG, you’re familiar
with the idea of recursive functions as Haskell does it. What makes
recursion a special case of this concept of knowing sequences is that
we go from one to the next by building on the previous step. With
fac above, we go down a recursion rabbit hole, then come back out
the rabbit hole, multiplying the previous result to the next. So for
3! we’re creating
fac (3) 3 * fac (2) 3 * 2 * fac (1) 3 * 2 * 1 * fac (0) 3 * 2 * 1 * 1
i.e., each line, starting at the top, resolves to the next as it goes
into the recursive process of a function calling itself[fn:11]. Again, this
is a building process. That is to say recursive fac is not an
algorithm, per se, a “solution” for drilling directly into any place
in a sequence. What would a solution look like for going straight to a
place in a sequence?
[fn:3] Professor Chandra assumes the students have worked up to if not beyond Kwong’s Arguments and Rules of Inference.
[fn:4] also written as
[fn:5]
[fn:6] A good study technique is to read the theoretical explanation, then some examples, then go back to the theoretical explanation to see how it is the perfect generalization of all the examples.
[fn:7] See this LYAGFGG treatment of let.
[fn:8] German phrase meaning “It’s Greek to me.”
[fn:9] Check it out here.
[fn:10] Another version of factorial would be simply fac n = product
[1..n]. See product here. Try it out. And if you’re feeling really
brave, look under the hood here. What you’re seeing is a special
fold function that — and only if you’re really brave — is talked
about here. So product is based on a more basic concept of a
fold. More later.
[fn:11] By the way, why is the result of fac with input 0 set to
1? In math, a product of no factors is considered to be the
multiplicative identity, i.e., that number when multiplied by any
number gives that number back. 1 times something is just that
something again.