On maths and engineering
I want to be dangerous with maths, at least, with regard to software engineering. I know math isn't necessarily a requirement for the field, but being competent never hurts. Moreover, time and time again I have found myself trying to read through some CS literature like Intro to Algorithms, or SICP, or (most recently) The Algorithm Design Manual only to find myself waylaid by the math weaved into the essence of the prose. Some of it, I am able to overcome, but often it ends up being a point of frustration that causes me to lose interest or take too long to make any meaningful progress.
When I was just starting out, I didn't really think much of this gap. I was more occupied with just learning programming, but now I think I want to do more to study computer science: do a little more theory rather than just practicals. I want to get good at the relevant math which, from my research, seems to just be mostly discrete math (plus linear algebra and statistics for ML). Maybe some Calculus, but that seems more useful in specific niches, if anything.
Oddly enough, I have taken a Calculus class, Calculus I specifically, back in community college (CC). However, since I wasn't able to complete a Bachelor's degree immediately after CC, I haven't taken a discrete math class. Well, that's not entirely true. I did do some study in the semester before my hiatus at WGU. Needless to say, for all intents and purposes, I haven't really taken a discrete math class, so I'm just gonna do that.
I've found the textbook, Discrete Mathematics with Applications by Susanna S. Epp, to be fantastic so far. Super accessible, and I hope to get through it cover-to-cover or close enough to achieve my ends. In parallel, I am also reading The Algorithm Design Manual for DSA practice. Yes, sure I could just take one of the many DSA/Leetcode courses geared specifically towards getting a person interview-ready, and I did start with that, but I guess I wanted something a little more comprehensive? I also wanted to make progress on this curriculum, so I figured reading TADM would be killing two birds with one stone.
I'm in a pretty good spot to dive into this, I think. Let's just hope it stays that way long enough for me to get to where I want to go.
Anyways, while I go through TADM, particularly the exercises, I find myself needing to do things like come up with counterexamples or prove algorithms. This stuff was never interesting to me, but I find it more and more fascinating as the days go by. I'm even looking to learn Lean to get better at formally expressing the proofs I write. I haven't gotten to the proof section of Discrete Mathematics with Applications yet, so the proof exercises in TADM are still a bit of a slog. I have found Claude to be particularly helpful, but I don't let it just give me the answers. I have system prompts that specifically disable this behavior. No, I have configured Claude to be a kind of tutor, and it's been working wonders in helping me get through the TADM exercises while I shore up my math.
A couple of days ago, Claude and I worked through a proof for Horner's method using loop invariants. Below is what I was able to come up with following Claude's assistance (all of this below is in my own words):
Horner(a, x)
p = a_n
for i from n − 1 to 0
p = p · x + a_i
return p
What is/are the invariant(s) that directly assert on the expected end result of this algorithm? Horner's method is an algorithm for evaluating [[Polynomials]]. So it stands to reason that our invariant ought to be something related to the evaluation of polynomials. The algorithm returns a value
Some scrutiny suggests that the invariant we care about here is that "
- At initialization,
which adheres to our invariant since, at this point, is not initialized, there is no but holds the first term of the polynomial. - After each iteration, we can see that our invariant holds true as with every iteration,
still contains an evaluated polynomial up to . - For iteration 1, we are 1 away from
, so . Thus, . Since at this iteration , is also equal to , matching our invariant - For iteration 2, we are 2 away from
, so . Thus . Again, because at this iteration we are at , , thus , matching our invariant - For iteration 3, we are 3 away from
, so . Thus, . Once more, because at this iteration we are at , , a for each iteration. Thus, , matching our invariant
- For iteration 1, we are 1 away from
- Notice how with each iteration, the polynomial held by
increases by a term and all the exponents increase by 1? Also note that the exponent for the first time is equal to the number of iterations. At our first iteration the first term had an exponent of 1. At the second iteration, the exponent was 2, and in our third, it was 3. Likewise, at our first iteration , at the second , and at the third iteration . Doing some quick algebra shows us that we could generalize our exponent as ( -> -> ). And because each subsequent term has an exponent that is 1 less than the exponent of the previous term, the second and third terms will have an exponent of and respectively. Thus we can state our invariant more algebraically as . Notice how this is more or less equivalent to what we got as the value of after each iteration. - At termination, that is, when
, . This is equivalent to our invariant, so the invariant holds all through.
Note that
Look at how beautiful that is. It's enough to make a grown man cry! Though I think what I have here is accurate, I'm always open to correction.
Learning about loop invariants and using them for this proof took me a while, and there was a lot of stumbling and fumbling, but I managed it. My goal now is to make it easier for me to do these kinds of things, and by extension open myself up to more CS literature. Not all of it, mind, but enough to help broaden my engineering capabilities. Let's see how it goes.