Math for CS: Infinite Sets

This chapter is about infinite sets and some challenges in proving things about them.

There has been a truly astonishing outcome of studying infinite sets. Their study led to the discovery of fundamental, logical limits on what computers can possibly do. For example, in a later section, they use reasoning developed for infinite sets to prove that it’s impossible to have a perfect type-checker for a programming language. So in this chapter, they ask us to bite the bullet and start learning to cope with infinity. Bite the bullet because it may seem irrelevant.

In the late nineteenth century, the mathematician Georg Cantor was studying the convergence of Fourier series and found some series that he wanted to say converged "most of the time," even though there were an infinite number of points where they didn’t converge. As a result, Cantor needed a way to compare the size of infinite sets. To get a grip on this, he got the idea of extending the Mapping Rule to infinite sets: he regarded two infinite sets as having the "same size" when there was a bijection between them. Likewise, an infinite set A should be considered "as big as" a set B when A surj B. So we could consider A to be "strictly smaller” than B, which we abbreviate as A strict B, when A is not "as big as” B.

However, don’t assume that surj has any particular "as big as” property on infinite sets until it’s been proved.

We go over some theorems and lemmas.

Adding a constant to infinity results in infinity still.

Cantor’s astonishing discovery was that not all infinite sets are the same size. In particular, he proved that for any set, A, the power set, pow(A), is "strictly bigger” than A.

I understand the basic idea, and intuitively, it makes sense why A to Pow(A) is injective. But the proof is difficult to understand. This proof is covered in a Real Analysis course at MIT. I was watching the lecture video about this to try to understand it better but it’s not clicking for me just yet. Revisited a day or two later and now I understand!

Countable vs. uncountable sets are discussed.

Went over the diagonal argument, which is a simple but powerful way to explain why some infinite sets are uncountable.

This lesson was interesting to me. Though it was not 100% easy to follow. Thinking in terms of infinity is abstract.

It’s not rocket science though, so I was able to understand.

There was a lot of lecture videos for this unit. I like the lecture videos too.

Halting problem. Similar to diagonal argument reasoning. The more practical implication is for writing a type checker. There is no string procedure that type checks perfectly.

The type checker was an arbitrary example, but the idea extends that there is no perfect checker for essentially any property of procedure outcomes.

Most compilers do “static” type-checking at compile time to ensure that programs won’t make run-time type errors. A program that type-checks is guaranteed not to cause a run-time type-error. But since it’s impossible to recognize perfectly when programs won’t cause type-errors, it follows that the type-checker must be rejecting programs that really wouldn’t cause a type-error.

The conclusion is that no type-checker is perfect—you can always do better! It’s a different story if we think about the practical possibility of writing programming analyzers. The fact that it’s logically impossible to analyze perfectly arbitrary programs does not mean that you can’t do a very good job analyzing interesting programs that come up in practice.

In fact, these “interesting” programs are commonly intended to be analyzable in order to confirm that they do what they’re supposed to do. In the end, it’s not clear how much of a hurdle this theoretical limitation implies in practice. But the theory does provide some perspective on claims about general analysis methods for programs. The theory tells us that people who make such claims either

• are exaggerating the power (if any) of their methods, perhaps to make a sale or get a grant, or
• are trying to keep things simple by not going into technical limitations they’re aware of, or
• perhaps most commonly, are so excited about some useful practical successes of their methods that they haven’t bothered to think about the limitations which must be there.

So from now on, if you hear people making claims about having general program analysis/verification/optimization methods, you’ll know they can’t be telling the whole story.

One more important point: there’s no hope of getting around this by switching programming languages. Our proof covered programs written in some given programming language like Java, for example, and concluded that no Java program can perfectly analyze all Java programs. Could there be a C++ analysis procedure that successfully takes on all Java programs? After all, C++ does allow more intimate manipulation of computer memory than Java does.

But there is no loophole here: it’s possible to write a virtual machine for C++ in Java, so if there were a C++ procedure that analyzed Java programs, the Java virtual machine would be able to do it too, and that’s impossible. These logical limitations on the power of computation apply no matter what kinds of programs or computers you use.