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…