Introduction:
- There are some problems for which there does not exist an algorithm that can guarantee to return a correct (ex. yes or no) answer. These are called “Undecidable” problems.
- The problems for which there does exist an algorithm that can guarantee to return a correct (ex. yes or no) answer are called “Decidable” problems.
Halting Problem:
- To understand this concept further we will look at a classic undecidable problem known as the Halting problem.
- The Halting problem involves two computer programs:
- Oracle_Program
- Recursive_Program
- The Oracle_Program is a program that predicts whether a program, will halt on a given input, or loop forever. Note: this program grantees (promises) to give us the correct answer, and never the wrong answer. (We will prove that no such program exists.) The oracle program takes in a program, returns “Halt” if the program halts and “Loops Forever” if the program loops forever.
- Function Oracle_Program(Program)
- If(Program) = “Halt”)
- Return “Halt”
- Else
- Return “Loops Forever”
- If(Program) = “Halt”)
- Consider the following Recursive_Program, which loops forever if a given program with a given input is predicted to halt by the Oracle_Program, and returns “Halt” if a given program loops forever.
- Function Recursive_Program(Program, Input)
- If(Oracle_Program(Program(Input)) == “Halt”)
- LoopForever()
- Else
- Return “Halt”
- If(Oracle_Program(Program(Input)) == “Halt”)
- Note that a contradiction is found if this Recursive_Program is then passed into itself. If the Oracle_Program predicts that the Recusive_Program will “Halt”, then the Recursive_Program will “Loop Forever”; which is a logical contradiction. If the Oracle_Program predicts that the Recusive_Program will “Loop Forever”, then the Recursive_Program will “Halt”; which is also a logical contradiction. These contradictions prove that there is not a generalizable algorithm that will always tell if a program will halt.
- Function Recursive_Program(Recursive_Program, Input)
- If(Oracle_Program(Recursive_Program(Input)) == “Halt”)
- LoopForever()
- Else
- Return “Halt”
- If(Oracle_Program(Recursive_Program(Input)) == “Halt”)
- Decidability has large implications for formal systems. For example, it is undecidable whether a first-order logic system formal valid (that is true under all interpretations).
- Example: ∀B∀A( A ∧ ¬B )
- This is TRUE if in the ‘domain of discourse’ A = 1, B = 2
- This is FALSE if in the ‘domain of discourse’ A = 4 = 4
- Therefore, the FOL expression itself is not decidable. One would need additional interpretation of the domain of discourse.
- However; it turns that it is decidable whether Zero-Order (propositional) logic formals are valid (True). There exist algorithms for deciding this. A nice quality of SAT problems is that they are always decidable, even if they are NP-Hard.
- Algorithms that make SAT decidable:
- Truth Table assignments
- DPLL
- DFS
- Etc…