Theory Halting

(*
Undecidability of the special Halting problem:
  Does a program applied to an encoding of itself terminate?
Author: Fabian Huch
*)

theory Halting
  imports "HOL-IMP.Big_Step"
begin

definition "halts c s ≡ (∃s'. (c, s) ⇒ s')"

text ‹A simple program that does not halt:›
definition "loop ≡ WHILE Bc True DO SKIP"

lemma loop_never_halts[simp]: "¬ halts loop s"
  unfolding halts_def
proof clarify
  fix s' assume "(loop, s) ⇒ s'"
  then show False
    by (induction loop s s' rule: big_step_induct) (simp_all add: loop_def)
qed

section ‹Halting Problem›

text ‹
Given any encoding ‹f› (of programs to states), there is no Program ‹H› such that 
for all programs ‹c›, ‹H› terminates in a state ‹s'› which has at variable ‹x› the
answer whether ‹c› halts.›

theorem halting: 
  "∄H. ∀c. ∃s'. (H, f c) ⇒ s' ∧ (halts c (f c) ⟷ s' x > 0)"
  (is "∄H. ?P H")
proof clarify
  fix H assume assm: "?P H"

  ― ‹inverted H: loops if input halts›
  let ?inv_H = "H ;; IF Less (V x) (N 1) THEN SKIP ELSE loop" 

  ― ‹compute in ‹s'› whether inverted ‹H› halts when applied to itself›
  obtain s' where 
    s'_def: "(H, f ?inv_H) ⇒ s'" and 
    s'_halts: "halts ?inv_H (f ?inv_H) ⟷ (s' x > 0)" 
    using assm by blast

  ― ‹contradiction: if it terminates, loop must have terminated; if not, SKIP must have looped!›
  show False
  proof(cases "halts ?inv_H (f ?inv_H)")
    case True

    then have "halts (IF Less (V x) (N 1) THEN SKIP ELSE loop) s'"
      unfolding halts_def using big_step_determ s'_def by fast

    then have "halts loop s'"
      using s'_halts True halts_def by auto

    then show False by auto
  next
    case False

    then have "¬ halts SKIP s'"
      using s'_def s'_halts halts_def by force

    then show False using halts_def by auto
  qed
qed

end