Quelle  Halting.thy   Sprache: Isabelle

(*
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