HALT_TM ≤m A_TM

הכיוון ההפוך: כל מופע HALT_TM ניתן למיפוי למופע A_TM עם אותה תשובת כן/לא. יחד עם A_TM ≤m HALT_TM, זה מראה ששתי הבעיות שקולות תחת רדוקציות מיפוי.

שתי הבעיות

HALT_TM

מופע: מכונת טיורינג M ומחרוזת w.

שאלה: האם M עוצרת על w (בכל מצב — קבלה או דחייה)?

A_TM

מופע: מכונת טיורינג M′ ומחרוזת w.

שאלה: האם M′ מקבלת את w?

בהינתן מופע HALT_TM ⟨M, w⟩, בנו מופע A_TM ⟨M′, w⟩ כאשר M′ היא מכונת הטיורינג הבאה:

M' on input x:
  1. Simulate M on x.
  2. If the simulation ever halts (accept or reject), accept.

תיאור M′ ניתן לחישוב מתיאור M, כך שההעתקה ⟨M, w⟩ ↦ ⟨M′, w⟩ היא פונקציה כריעה.

שלב 1 / 4מופע HALT_TM

HALT_TM instance

⟨M, w⟩

→

A_TM instance

⟨M′, w⟩

בניית M′

M' on input x:
  1. Simulate M on x.
  2. If the simulation ever halts (accept or reject), accept.

M on w	M′ on w	⟨M, w⟩ ∈ HALT_TM	⟨M′, w⟩ ∈ A_TM
מקבלת	מקבלת	כן	כן
דוחה	מקבלת	כן	כן
לולאה	לולאה	לא	לא

⟨M, w⟩ ∈ HALT_TM ⟺ ⟨M′, w⟩ ∈ A_TM

קלט ⟨M, w⟩: מכונת טיורינג M ומחרוזת w. שאלת HALT_TM היא האם M עוצרת על w (בכל מצב — קבלה או דחייה).

(⇒) אם M עוצרת על w, אז גם הסימולציה ב־M′ עוצרת, כך ש־M′ מגיעה לצעד 2 ומקבלת. לכן ⟨M′, w⟩ ∈ A_TM.

(⇐) אם M אינה עוצרת על w, אז גם M′ רצה לנצח בהדמיית M ולעולם אינה מגיעה לצעד 2. לכן M′ אינה מקבלת את w, כלומר ⟨M′, w⟩ ∉ A_TM.

לפיכך ⟨M, w⟩ ∈ HALT_TM אם ורק אם ⟨M′, w⟩ ∈ A_TM. יחד עם הרדוקציה בכיוון הישיר זה נותן A_TM ≡m HALT_TM. ∎