# Formal Methods 101: Decidability

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”
• 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”
• 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”
• 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…