Computability

This chapter is getting really long and it is time to end it ☺️

We will see how the discussion of infinite comes in the context of computer science very nicely.

Theorem 33

The set of all possible computer programs is countable.

Exercise 82

In particular, a computer program can be seen as a (finite) string of characters (e.g. english alphabet and special characters (like %, $ and so on)).

• Let $\Sigma$ be a finite set and $k \in {\mathbb N}$. Prove that $\Sigma^k$ is finite.
• Prove that $\Sigma^* = \bigcup_{k \in {\mathbb N}} \Sigma^k$ is countable.

These two exercises imply immediately Theorem 33.

We say that a set $S \subseteq \{0,1\}^*$ is decidable if there is a yes-no program $P$ such that $P(x)$ says yes if and only if $x \in S$; otherwise (no such program exists), it is undecidable. The concept of decidable sets captures exactly the decision problems (yes-no answers) that can be solvable by a computer program.

Theorem 34

There exists an undecidable set.

This theorem alone is not really surprising. In the end, the set of all computer programs is countable, while the set of all decision problems, which is just $\mathcal{P}(\{0,1\}^*)$, is uncountable. So definitely, some problem cannot be decidable.

A more surprising result (due to Alan Turing - the "father" of computer science.) is actually the fact that some not-so-difficult looking problems are in fact undecidable. In particular, Turing's proof implies that the following problem (called the halting problem) is undecidable:

Given a student's program $P$ and an test input $x$, decide whether $P(x)$ terminates or runs forever.¹

In a way, the theorem of Turing is really a teacher's misery (especially a programming teacher), since we will never have any intelligent way to check whether a program terminates or not. The proof of this theorem crucially relies on the diagonalization technique. We will not cover the proof in this course, but we will mention an interesting implication.

Theorem 35 (Gödel's incompleteness, informal)

In any natural formal axiom system, there exists a mathematical statement which is neither provably true nor false.

Proof(sketch):

This is only a sketch, so it will be sloppy (meaning that the students are advised against writing this kind of proof as a homework solution :-)). Nevertheless, we do hope that it illustrates a nice connection between computation and proofs. Let us assume that the theorem statement is false, i.e, a formal proof system can always prove a statement true or false. Then, one can decide the halting problem in the following way. Given a program $P$ and input $x$, encode the following statement as a mathematical statement:

$\Phi_{P,x}:$ There exists a finite program execution-log of $P(x)$ (which shows that $P(x)$ terminates).

Any natural logic can encode this statement mathematically (this is a sloppy part ☺️). This would imply, from our assumption, that there exists a proof that $\Phi_{P,x}$ is true or false. We use a computer program $Q$ to enumerate and check the proof (since the proof is finite, we can do this, by just enumerating all axioms and logical deductions and checking can be done efficiently). This implies that $Q$ could decide whether $P(x)$ terminates, a contradiction to the theorem of Turing (this is another sloppy part).

The previous proof only relies on the fact that a given formal proof system would be able to encode statements about computation (any reasonable proof system would be able to do that). Of course, sloppy parts are there, but students should note that we have a total awareness of which steps are sloppy.

Footnotes

1. One could think of a computer that interprets $P$ as a program and runs it on input $x$ and reports if $P$ finishes, do you see why this is not a yes-no program? ↩