def f ( n ): while n > 1 : if n % 2 == 0 : n = n / 2 else : n = 3 * n + 1

ในวิทยาการคอมพิวเตอร์การวิเคราะห์การสิ้นสุดการทำงานคือการวิเคราะห์โปรแกรมที่พยายามตรวจสอบว่าการประเมินผลของโปรแกรม ที่กำหนด หยุดลงสำหรับแต่ละอินพุตหรือไม่ ซึ่งหมายถึงการตรวจสอบว่าโปรแกรมอินพุตคำนวณฟังก์ชันทั้งหมด ได้หรือไม่

ปัญหา นี้มีความเกี่ยวข้องอย่างใกล้ชิดกับปัญหาการหยุดทำงาน (halting problem)ซึ่งเป็นการพิจารณาว่าโปรแกรมที่กำหนดจะหยุดทำงานสำหรับ อินพุต ที่กำหนด หรือ ไม่ และเป็น ปัญหา ที่ไม่สามารถตัดสินได้การวิเคราะห์การสิ้นสุด (termination analysis) นั้นยากยิ่งกว่าปัญหาการหยุดทำงานเสียอีก: การวิเคราะห์การสิ้นสุดในแบบจำลองของเครื่องจักรทัวริง (Turing machine)ในฐานะแบบจำลองของโปรแกรมที่ใช้ฟังก์ชันที่คำนวณได้นั้น มีเป้าหมายเพื่อตัดสินว่าเครื่องจักรทัวริงที่กำหนดให้เป็นเครื่องจักรทัวริงแบบสมบูรณ์ หรือไม่ และปัญหานี้อยู่ในระดับที่สูงกว่า${\displaystyle \Pi _{2}^{0}}$เนื่องจากอยู่ในลำดับชั้นทางคณิตศาสตร์จึงมีความยากกว่าปัญหาการหยุดทำงานอย่างเห็นได้ชัด

เนื่องจากคำถามที่ว่าฟังก์ชันที่คำนวณได้เป็นฟังก์ชันสมบูรณ์หรือไม่นั้นไม่ สามารถตัดสินได้ แบบกึ่งสมบูรณ์^{[ 1 ]} ตัววิเคราะห์การสิ้นสุด เสียงแต่ละตัว(กล่าวคือ จะไม่มีการให้คำตอบยืนยันสำหรับโปรแกรมที่ไม่สิ้นสุด) จึงไม่สมบูรณ์ กล่าว คือ จะต้องล้มเหลวในการพิจารณาการสิ้นสุดสำหรับโปรแกรมที่สิ้นสุดจำนวนอนันต์ ไม่ว่าจะโดยการทำงานตลอดไปหรือหยุดด้วยคำตอบที่ไม่แน่นอน

การพิสูจน์การสิ้นสุดเป็นรูปแบบหนึ่งของการพิสูจน์ทางคณิตศาสตร์ที่มีบทบาทสำคัญในการตรวจสอบอย่างเป็นทางการเนื่องจากความถูกต้องสมบูรณ์ของอัลกอริทึมขึ้นอยู่กับการสิ้นสุด

วิธีการทั่วไปที่ง่ายสำหรับการสร้างบทพิสูจน์การสิ้นสุดเกี่ยวข้องกับการเชื่อมโยงมาตรวัดกับแต่ละขั้นตอนของอัลกอริทึม มาตรวัดนั้นได้มาจากโดเมนของความสัมพันธ์ที่มีรากฐานที่ดีเช่น จากจำนวนเชิงอันดับหากมาตรวัด "ลดลง" ตามความสัมพันธ์นั้นในทุกขั้นตอนที่เป็นไปได้ของอัลกอริทึม แสดงว่าอัลกอริทึมนั้นต้องสิ้นสุด เพราะไม่มีสายโซ่ที่ลดลงอย่างไม่มีที่สิ้นสุดเมื่อเทียบกับความสัมพันธ์ที่มีรากฐานที่ดี

การวิเคราะห์การยุติสัญญาบางประเภทสามารถสร้างหรือบ่งชี้ถึงหลักฐานการยุติสัญญาได้โดยอัตโนมัติ

ตัวอย่างหนึ่งของ โครงสร้าง ภาษาโปรแกรมที่อาจจะสิ้นสุดหรือไม่สิ้นสุดก็ได้คือลูปเนื่องจากสามารถทำงานซ้ำได้หลายครั้ง ลูปที่ใช้ตัวแปรนับจำนวนซึ่งมักพบใน อัลก อริธึมการประมวลผลข้อมูล มักจะสิ้นสุดการทำงาน ดัง ตัวอย่าง รหัสเทียมด้านล่าง:

i := 0 วนลูปจนกว่า i จะเท่ากับขนาดของข้อมูล process_data(data[i])) // ประมวลผลข้อมูลส่วนที่ตำแหน่ง i i := i + 1 // ย้ายไปยังข้อมูลส่วนถัดไปที่จะประมวลผล

หากค่าของSIZE_OF_DATAเป็นค่าที่ไม่ติดลบ คงที่ และมีค่าจำกัด ลูปจะสิ้นสุดลงในที่สุด โดยสมมติว่าฟังก์ชัน process_dataก็สิ้นสุดลงด้วยเช่นกัน

บางครั้งลูปอาจแสดงให้เห็นว่าสิ้นสุดเสมอหรือไม่มีวันสิ้นสุดได้ด้วยการตรวจสอบโดยมนุษย์ ตัวอย่างเช่น ลูปต่อไปนี้ ในทางทฤษฎีแล้วจะไม่หยุดทำงาน อย่างไรก็ตาม อาจหยุดทำงานเมื่อรันบนเครื่องจริงเนื่องจากค่าเกินขีดจำกัดทางคณิตศาสตร์ (arithmetic overflow ) ซึ่งอาจนำไปสู่ข้อยกเว้นหรือทำให้ตัวนับวนกลับไปที่ค่าลบและทำให้เงื่อนไขของลูปเป็นจริงได้

i := 1 วนลูปจนกว่า i = 0 i := i + 1

ในการวิเคราะห์การยุติการทำงาน เราอาจพยายามหาพฤติกรรมการยุติการทำงานของโปรแกรมบางโปรแกรมโดยขึ้นอยู่กับอินพุตที่ไม่ทราบค่า ตัวอย่างต่อไปนี้แสดงให้เห็นถึงปัญหานี้

i := 1 วนลูปจนกว่า i = UNKNOWN i := i + 1

ในที่นี้ เงื่อนไขของลูปถูกกำหนดโดยใช้ค่าที่ไม่ทราบค่า (UNKNOWN) ซึ่งค่าของ UNKNOWN นั้นไม่เป็นที่ทราบ (เช่น กำหนดโดยข้อมูลที่ผู้ใช้ป้อนเมื่อโปรแกรมทำงาน) การวิเคราะห์การสิ้นสุดของลูปจะต้องพิจารณาค่าที่เป็นไปได้ทั้งหมดของ UNKNOWN และพบว่าในกรณีที่ UNKNOWN = 0 (เช่นเดียวกับในตัวอย่างเดิม) จะไม่สามารถแสดงการสิ้นสุดของลูปได้

อย่างไรก็ตาม ไม่มีขั้นตอนทั่วไปใดที่จะระบุได้ว่านิพจน์ที่เกี่ยวข้องกับคำสั่งวนซ้ำจะหยุดทำงานหรือไม่ แม้ว่ามนุษย์จะเป็นผู้ตรวจสอบก็ตาม เหตุผลทางทฤษฎีสำหรับเรื่องนี้คือความไม่สามารถตัดสินได้ของปัญหาการหยุดทำงาน กล่าวคือ ไม่มีอัลกอริทึมใดที่จะระบุได้ว่าโปรแกรมใด ๆ จะหยุดทำงานหลังจากขั้นตอนการคำนวณจำนวนจำกัดหรือไม่

ในทางปฏิบัติ การแสดงให้เห็นถึงการสิ้นสุด (หรือไม่สิ้นสุด) ของโปรแกรมนั้นทำได้ยาก เพราะอัลกอริทึมแต่ละตัวทำงานโดยใช้ชุดวิธีการที่จำกัด ซึ่งสามารถดึงข้อมูลที่เกี่ยวข้องออกมาจากโปรแกรมที่กำหนดได้ วิธีการหนึ่งอาจตรวจสอบว่าตัวแปรเปลี่ยนแปลงอย่างไรเมื่อเทียบกับเงื่อนไขของลูป (ซึ่งอาจแสดงให้เห็นถึงการสิ้นสุดของลูปนั้น) วิธีการอื่นอาจพยายามแปลงการคำนวณของโปรแกรมไปเป็นโครงสร้างทางคณิตศาสตร์บางอย่างและทำงานกับโครงสร้างนั้น ซึ่งอาจได้รับข้อมูลเกี่ยวกับพฤติกรรมการสิ้นสุดจากคุณสมบัติบางอย่างของแบบจำลองทางคณิตศาสตร์นี้ แต่เนื่องจากแต่ละวิธีสามารถ "มองเห็น" ได้เพียงบางสาเหตุเฉพาะของการสิ้นสุด (หรือไม่สิ้นสุด) เท่านั้น แม้จะใช้การผสมผสานของวิธีการต่างๆ ก็ไม่สามารถครอบคลุมสาเหตุที่เป็นไปได้ทั้งหมดของการสิ้นสุด (หรือไม่สิ้นสุด) ได้

ฟังก์ชันเรียกซ้ำและลูปนั้นเทียบเท่ากันในแง่ของการแสดงออก นิพจน์ใดๆ ที่เกี่ยวข้องกับลูปสามารถเขียนได้โดยใช้การเรียกซ้ำ และในทางกลับกัน ดังนั้น โดยทั่วไปแล้ว การสิ้นสุดของนิพจน์เรียกซ้ำจึงไม่สามารถตัดสินได้ นิพจน์เรียกซ้ำส่วนใหญ่ที่พบได้ในการใช้งานทั่วไป (เช่น ไม่ใช่นิพจน์ที่ผิดปกติ ) สามารถแสดงให้เห็นว่าสิ้นสุดได้ด้วยวิธีการต่างๆ ซึ่งโดยปกติจะขึ้นอยู่กับนิยามของนิพจน์นั้นเอง ตัวอย่างเช่น อาร์กิวเมนต์ของฟังก์ชัน ในนิพจน์เรียกซ้ำสำหรับ ฟังก์ชัน แฟกทอเรียลด้านล่างจะลดลงทีละ 1 เสมอ ด้วยคุณสมบัติการเรียงลำดับที่ดีของจำนวนธรรมชาติอาร์กิวเมนต์จะถึง 1 ในที่สุดและการเรียกซ้ำจะสิ้นสุดลง

ฟังก์ชัน factorial (อาร์กิวเมนต์เป็นจำนวนธรรมชาติ) ถ้าอาร์กิวเมนต์เท่ากับ 0 หรือเท่ากับ 1 ให้คืนค่า 1 มิฉะนั้นให้คืนค่าอาร์กิวเมนต์ * factorial(อาร์กิวเมนต์ - 1)

การตรวจสอบการสิ้นสุดมีความสำคัญมากใน ภาษาโปรแกรม แบบพึ่งพาประเภทข้อมูล และระบบพิสูจน์ทฤษฎีบท เช่นRocqและAgdaระบบเหล่านี้ใช้ไอโซมอร์ฟิซึมแบบ Curry-Howardระหว่างโปรแกรมและการพิสูจน์ การพิสูจน์เกี่ยวกับประเภทข้อมูลที่กำหนดโดยอุปนัยนั้นโดยทั่วไปจะอธิบายโดยใช้หลักการอุปนัย อย่างไรก็ตาม ต่อมาพบว่าการอธิบายโปรแกรมผ่านฟังก์ชันที่กำหนดแบบเรียกซ้ำด้วยการจับคู่รูปแบบเป็นวิธีการพิสูจน์ที่เป็นธรรมชาติมากกว่าการใช้หลักการอุปนัยโดยตรง น่าเสียดายที่การอนุญาตให้มีการกำหนดที่ไม่สิ้นสุดนำไปสู่ความไม่สอดคล้องกันทางตรรกะในทฤษฎีประเภทซึ่งเป็นเหตุผลว่าทำไม Agda และ Rocq จึงมีตัวตรวจสอบการสิ้นสุดในตัว

มีทีมวิจัยหลายทีมที่ทำงานเกี่ยวกับวิธีการใหม่ๆ ที่สามารถแสดงให้เห็นถึงการสิ้นสุด (หรือไม่สิ้นสุด) นักวิจัยหลายคนได้รวมวิธีการเหล่านี้ไว้ในโปรแกรม^{[ 2 ]}ที่พยายามวิเคราะห์พฤติกรรมการสิ้นสุดโดยอัตโนมัติ (โดยไม่ต้องมีการโต้ตอบจากมนุษย์) แง่มุมหนึ่งของการวิจัยที่กำลังดำเนินอยู่คือการอนุญาตให้ใช้วิธีการที่มีอยู่เพื่อวิเคราะห์พฤติกรรมการสิ้นสุดของโปรแกรมที่เขียนด้วยภาษาโปรแกรม "โลกแห่งความเป็นจริง" สำหรับภาษาเชิงประกาศ เช่นHaskell , MercuryและPrologมีผลลัพธ์มากมาย^{[ 3 ] [ 4 ] [ 5 ]} (ส่วนใหญ่เป็นเพราะพื้นฐานทางคณิตศาสตร์ที่แข็งแกร่งของภาษาเหล่านี้) ชุมชนวิจัยยังทำงานเกี่ยวกับวิธีการใหม่ๆ เพื่อวิเคราะห์พฤติกรรมการสิ้นสุดของโปรแกรมที่เขียนด้วยภาษาเชิงคำสั่ง เช่น C และ Java

• การวิเคราะห์ความซับซ้อน—ปัญหาของการประมาณเวลาที่จำเป็นในการยุติกระบวนการ
• รูปแบบลูป
• การเขียนโปรแกรมเชิงฟังก์ชันแบบสมบูรณ์ (Total functional programming ) —รูปแบบการเขียนโปรแกรมที่จำกัดขอบเขตของโปรแกรมให้เหลือเฉพาะโปรแกรมที่สามารถพิสูจน์ได้ว่าสิ้นสุดการทำงาน
• การเรียกซ้ำของวอลเธอร์
• หลักการยุติการเปลี่ยนแปลงขนาด

• การวิเคราะห์การยุติการทำงานของโปรแกรมเชิงฟังก์ชันระดับสูง
• รายชื่อผู้รับจดหมายของเครื่องมือการยุติ
• การแข่งขันการยุติสัญญา— ดู คำอธิบายได้ในMarché, Zantema (2007)
• พอร์ทัลการยุติ