Sipser: Section 4.2
From CSWiki
CSC 341:Front Door | CSC 341: Cooperative commentary | Sipser:_Chapter_4
Contents |
The Halting Problem
Basically, software verification problem is not solvable by computer. This section proves that certain problems are not solvable by computer by proving that they are undecidable by Turing-machine.
Theorem 4.11
ATM is undecidable. (page 174, 179)
Sipser proves this theorem using diagonalization method, the technique found by Georg Cantor.
The Diagonalization Method
This method compares size of two sets without counting each of them. This means we can compare infinite sets!
Definition 4.12 (page 175)
Assume we have set A and B, Definition 4.12 define the following relationship: one-to-one onto same size correspondence
Definition 4.14
A set A is countable if either it is finite or it has the same size as N.
Theorem 4.17
R is uncountable.
Corollary 4.18
Some languages are not Turing-recognizable.
This corollary is proved by showing that "the set of all languages cannot be out into a correspondence with the set of all Turing machines." (page 179)
The Halting Problem Is Undecidable (Proof of Theorem 4.11)
A Turing-unrecognizable Language
Co-Turing-recognizable language is a complement of a Turing-recognizable language.
Theorem 4.22
A language is decidable iff it is Turing-recognizable and co-Turing-recognizable.
Corollary 4.23
is not Turing-recognizable.
Coonclusion/Summary
This section establishes problem ATM (and its derivitives) which will be used throughout the rest of the book as a tool to distinguish problems that are computable and that are not computable. This section also introduces the concept of "diagonal method" which will be used again several times further into the book.
