Mathematical Logic
Computability Theory
Turing in 1936 proved: some things cannot be computed. This became the foundation of theoretical computer science. Turing's diagonal argument and Goedel's diagonalization are the same mathematical technique applied to different objects.
- Static code analysis (Coverity, PVS-Studio): complete verification of arbitrary properties is impossible, so analyzers work only with decidable approximations
- Antivirus programs: full detection of malicious code is undecidable by the Rice theorem, so antivirus software relies on heuristics
- Hardware verification (model checking): the model-checking problem is finite and decidable precisely because the models are finite; for infinite systems the problem is undecidable
- Compilers: optimizations such as dead-code elimination are undecidable in general, so only conservative approximations are implemented
Turing Machines and the Halting Problem
Alan Turing in 1936 proved: no algorithm exists that, given an arbitrary program and input, determines whether the program will halt. This was the first formally proved limit of computation, obtained simultaneously with Goedel's theorems using the same diagonal method.
What method does Turing use to prove that HALT is undecidable?
Turing uses the diagonal argument: builds machine D that does the opposite of what hypothetical H predicts when run on itself, creating a logical contradiction analogous to the liar paradox as an algorithm.
Undecidability Hierarchy and Rice Theorem
Not all undecidable problems are equally complex. The Kleene-Mostowski arithmetical hierarchy classifies subsets of natural numbers by the complexity of their definitions: Sigma^0_1 (semi-decidable), Pi^0_1 (co-semi-decidable), Sigma^0_2, and so on. HALT is in Sigma^0_1 - semi-decidable but not decidable.
Rice theorem is a powerful tool for proving undecidability. Any nontrivial property P of the sets of words accepted by Turing machines is undecidable. 'Nontrivial' means: some machines have this property and others do not. Consequence: automatic verification of arbitrary programs is impossible.
What does the Rice theorem state?
Rice theorem: if P is a nontrivial property (P subset RE, P nonempty, P ne RE), then {<M> : L(M) in P} is undecidable. This makes complete automatic program verification impossible.
Итоги
- Turing machine: formal model of computation, equivalent to modern computers (Church-Turing thesis)
- HALT is undecidable: diagonal argument - assuming a decider H yields machine D with self-contradictory behavior
- Semi-decidability: HALT is in RE (semi-decidable) - the machine halts on 'yes' but need not halt on 'no'
- Rice theorem: any nontrivial semantic property of TM languages is undecidable - full automatic verification is impossible
- m-reducibility A <=_m B: decidability of B implies decidability of A; HALT is Sigma^0_1-complete
- Arithmetical hierarchy: levels Sigma^0_n, Pi^0_n, Delta^0_n classify the complexity of computational problems