(* 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\<open>A simple program that does not halt:\<close> 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'" thenshow False by (induction loop s s' rule: big_step_induct) (simp_all add: loop_def) qed
section \<open>Halting Problem\<close>
text\<open>
Given any encoding \<open>f\<close> (of programs to states), there is no Program \<open>H\<close> such that for all programs \<open>c\<close>, \<open>H\<close> terminates in a state \<open>s'\<close> which has at variable \<open>x\<close> the
answer whether \<open>c\<close> halts.\<close>
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"
\<comment> \<open>inverted H: loops if input halts\<close> let ?inv_H = "H ;; IF Less (V x) (N 1) THEN SKIP ELSE loop"
\<comment> \<open>compute in \<open>s'\<close> whether inverted \<open>H\<close> halts when applied to itself\<close> 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
\<comment> \<open>contradiction: if it terminates, loop must have terminated; if not, SKIP must have looped!\<close> show False proof(cases "halts ?inv_H (f ?inv_H)") case True
thenhave"halts (IF Less (V x) (N 1) THEN SKIP ELSE loop) s'" unfolding halts_def using big_step_determ s'_def by fast
thenhave"halts loop s'" using s'_halts True halts_def by auto
thenshow False by auto next case False
thenhave"\ halts SKIP s'" using s'_def s'_halts halts_def by force
thenshow False using halts_def by auto qed qed
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
