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…