Bài toán dừng

Trong lý thuyết khả tính, bài toán dừng có thể diễn đạt như sau: cho trước một chương trình máy tính, quyết định xem chương trình đó có chạy mãi mãi hay không. Bài toán này tương đương với việc cho trước một chương trình và dữ liệu vào, quyết định xem chương trình đó có dừng với dữ liệu đó hay chạy mãi mãi.
Alan Turing chứng minh năm 1936 rằng không tồn tại thuật toán nào giải quyết bài toán dừng cho mọi cặp chương trình-dữ liệu vào. Một phần quan trọng của chứng minh là định nghĩa của máy tính và chương trình, nay được biết đến là máy Turing. Bài toán dừng là không thể quyết định được trên máy Turing. Nó là một trong những ví dụ đầu tiên của các bài toán quyết định.
Theo Jack Copeland (2004), tên gọi bài toán dừng (tiếng Anh - halting problem) là của Martin Davis.
Giới thiệu.
Bài toán dừng là một bài toán quyết định về tính chất của chương trình máy tính trên một mô hình tính toán Turing-đầy đủ nhất định. Bài toán yêu cầu quyết định xem một chương trình với dữ liệu vào cho trước có dừng hay chạy mãi mãi. Trong mô hình trừu tượng này, không có bất kì một giới hạn nào về bộ nhớ hay thời gian cho máy chạy; máy có thể chạy lâu bao nhiêu cũng được, sử dụng tùy ý bộ nhớ, trước khi dừng. Câu hỏi chỉ là liệu chương trình cuối cùng có dừng hay không trên dữ liệu đã cho.
Ví dụ như chương trình sau dưới dạng mã giả
không bao giờ dừng, nó lặp lại mãi mãi. Trong khi đó, chương trình sau
dừng rất nhanh.
Chương trình càng phức tạp thì càng khó để phân tích. Ta có thể chạy chương trình một thời gian. Tuy nhiên, nếu nó không dừng trong thời gian đó thì cũng không thể biết được nó có chạy mãi mãi hay không. Turing chứng minh rằng không một thuật toán nào có thể quyết định đúng cho mọi cặp chương trình và dữ liệu vào, liệu chương trình có dừng hay không trên dữ liệu đã cho.
Tầm quan trọng và hệ quả.
Bài toán dừng là vô cùng quan trọng trong lịch sử lý thuyết khả tính do nó là một trong những bài toán đầu tiên được chứng minh là không quyết định được.
Biểu diễn bài toán dừng dưới dạng tập hợp.
Cách biểu diễn thông thường của các bài toán quyết định là tập hợp các đối tượng thỏa mãn tính chất đang xét. Tập dừng
đại diện cho bài toán dừng.
Có nhiều định nghĩa tương đương của bài toán dừng. Tất cả các tập có bậc Turing bằng với bài toán dừng là một cách định nghĩa. Sau đây là một vài ví dụ:
Tóm tắt chứng minh.
Sau đây là một chứng minh rằng không tồn tại một hàm khả tính nào quyết định được liệu một chương trình cho trước có dừng trên một dữ liệu vào cho trước hay không. Nói cách khác, nếu định nghĩa hàm "h(i, x)" trả về 1 nếu chương trình thứ "i" dừng trên dữ liệu vào "x" và 0 nếu nó không dừng, thì "h" là không tính được. Ở đây chương trình thứ "i" là theo thứ tự của một cách liệt kê tất cả các chương trình của một mô hình tính toán Turing đầy đủ.
Ý tưởng chính ở đây là chứng minh mọi hàm khả tính đều khác với hàm "h". Thật vậy, xem xét một hàm "f" bất kì. Định nghĩa hàm khả tính "g" như sau:"g(i)" không được định nghĩa khi "f(i,i) = 0" (chẳng hạn bằng cách "g" lặp mãi mãi khi "f(i,i)=0")và bằng 0 trong trường hợp còn lại. Nhận thấy rằng nếu "f" khả tính thì "g" khả tính.
Do "g" khả tính, tồn tại một chương trình "e" trong mô hình tính toán đã định để tính hàm "g". Theo định nghĩa của "g", luôn xảy ra một trong hai trường hợp sau:
Trong cả hai trường hợp, "f" và "h" nhận giá trị khác nhau. Do "f" là một hàm khả tính bất kì, mọi hàm khả tính đều khác với "h".