Đặt vấn đề

Có những chương trình không bị lỗi.

Chúng chỉ… không bao giờ về nhà.

Giả sử mình viết đoạn Python cực kỳ hiền lành này:

1while True:
2    print("Xin chào")

Chạy nó lên.

Máy tính sẽ in:

1Xin chào
2Xin chào
3Xin chào
4Xin chào
5...

cho tới khi mình tắt máy, cúp điện, hoặc con mèo đi ngang đạp vào nút nguồn.

Nhìn đoạn code, một đứa trẻ 6 tuổi cũng có thể đoán:

Cái này chạy mãi.

Quá dễ.

Nhưng bây giờ mình đưa cho bạn một chương trình dài 20 triệu dòng, gọi thêm 800 thư viện, đọc dữ liệu từ một file, chạy hàng nghìn vòng lặp, gọi đệ quy lung tung và hỏi:

Chương trình này cuối cùng có dừng không?

Nghe thì vẫn giống một câu hỏi kỹ thuật rất bình thường.

Chúng ta có debugger.

Có static analyzer.

Có AI đọc code.

Có CPU hàng tỷ transistor.

Có những con chip thực hiện hàng nghìn tỷ phép toán mỗi giây.

Vậy chắc chỉ cần viết một chương trình đủ thông minh để kiểm tra tất cả những chương trình khác?

Ví dụ:

1def will_halt(program, input):
2    if program_sẽ_dừng:
3        return True
4    else:
5        return False

Ta đưa bất kỳ chương trình nào vào.

Nó trả lời:

1DỪNG

hoặc:

1CHẠY MÃI

Xong thuật toán, quá dễ.

Chỉ có một vấn đề nhỏ.

Chương trình đó không thể tồn tại.

Không phải vì máy tính hiện nay chưa đủ mạnh.

Không phải vì thiếu GPU.

Không phải vì chưa có AI đủ thông minh.

Không phải vì cần thêm 100 năm nghiên cứu.

Mà theo nghĩa toán học mạnh hơn rất nhiều:

Không tồn tại một thuật toán tổng quát có thể luôn xác định chính xác một chương trình bất kỳ có dừng hay không.

Đây là bài toán dừng (Halting Problem).

Và nó là một trong những khoảnh khắc kỳ lạ nhất của khoa học máy tính: con người chưa kịp chế tạo máy tính điện tử hiện đại thì Alan Turing đã chỉ ra rằng có những thứ máy tính, dù mạnh tới đâu, cũng không thể làm được.

Trước tiên: “không giải được” nghĩa là gì?

Đây là chỗ rất dễ hiểu nhầm.

Có ít nhất ba kiểu “khó”.

Kiểu 1: Máy tính của tôi yếu quá

Ví dụ tính:

$$ 2 + 2 $$

Laptop làm được.

Máy tính bỏ túi làm được.

Cục khoai tây nối dây điện chắc cố gắng một chút cũng được.

Không có vấn đề gì.

Kiểu 2: Bài toán giải được nhưng quá lớn

Ví dụ thử tất cả khả năng của một bài toán tổ hợp khổng lồ.

Về nguyên tắc có thuật toán.

Nhưng nếu chạy mất:

110^30 năm

thì xét về đời người cũng xem như bó tay.

Đây là vấn đề về độ phức tạp tính toán (computational complexity).

Kiểu 3: Không có thuật toán tổng quát

Halting Problem thuộc loại này.

Ngay cả khi cho bạn:

• RAM vô hạn,
• CPU chạy nhanh vô hạn,
• datacenter to bằng Mặt Trăng,
• điện kéo thẳng từ Mặt Trời,
• và một ông DevOps không bao giờ xin nghỉ,

thì vẫn không thể viết một thuật toán luôn trả lời đúng cho mọi chương trình.

Đây không phải:

“Tính lâu quá.”

Mà là:

“Không tồn tại công thức tính tổng quát.”

Khác nhau rất xa.

Một bên là có cánh cửa nhưng đường tới đó dài quá.

Một bên là cánh cửa chưa từng tồn tại.

Bài toán dừng là gì?

Ta có một chương trình $P$ và một input $x$.

Ta muốn xây dựng chương trình:

$$ HALT(P, x) $$

sao cho:

$$ HALT(P,x)= \begin{cases} TRUE & \text{nếu P(x) cuối cùng dừng}
FALSE & \text{nếu P(x) chạy mãi mãi} \end{cases} $$

Quan trọng nhất là chữ:

mọi

Nó phải hoạt động với mọi chương trình hợp lệ và mọi input.

Không được nói:

“99,99% case em xử lý được rồi anh.”

Không.

Toán học ở đây rất khó tính.

Chỉ cần tồn tại một chương trình khiến HALT trả lời sai thì HALT không phải lời giải tổng quát.

Turing và các kết quả phát triển từ công trình năm 1936 cho thấy những bài toán quyết định kiểu này có giới hạn căn bản. Về mặt lịch sử, bài báo gốc của Turing tập trung vào các bài toán rất gần với phiên bản Halting Problem hiện đại và dùng chúng để chứng minh Entscheidungsproblem không có thủ tục quyết định tổng quát. (Stanford Encyclopedia of Philosophy)

Nhưng cứ chạy thử chương trình là biết mà?

Đây thường là phản ứng đầu tiên.

Giả sử ta cần kiểm tra:

1def program():
2    for i in range(1000):
3        print(i)

Ta chạy.

Một lúc sau chương trình kết thúc.

Vậy ta biết:

1HALT = TRUE

Không có vấn đề.

Nhưng thử chương trình này:

1def mystery():
2    while something():
3        do_something()

Sau một phút chưa dừng.

Có phải nó chạy mãi?

Chưa chắc.

Một tiếng?

Chưa chắc.

Một năm?

Vẫn chưa chắc.

Nó có thể dừng vào đúng:

1năm thứ 1.000.000.000

Nếu chương trình đã dừng, ta biết chắc nó dừng.

Nhưng nếu nó chưa dừng, ta không thể chỉ nhìn vào việc chờ đợi mà biết nó sẽ không bao giờ dừng.

Đó là sự bất đối xứng rất thú vị.

Giống như đứng trước một hang động.

Nếu con thỏ chạy ra, bạn biết:

“À, trong hang có thỏ.”

Nhưng nếu ngồi 20 phút chưa thấy con nào chạy ra, bạn không thể kết luận:

“Trong hang tuyệt đối không có thỏ.”

Có thể con thỏ đang ngủ.

Hoặc đang ăn cà rốt.

Hoặc nó là một con thỏ rất hướng nội.

Turing tung ra một cú tự tham chiếu

Bây giờ mới tới đoạn ngáo nhất.

Giả sử ta không tin Turing.

Ta tuyên bố:

Tôi đã viết được HALT.

Nó thần thánh như sau:

1def halt(program, input):
2    """
3    True  nếu program(input) sẽ dừng.
4    False nếu program(input) sẽ chạy mãi.
5    """

Và đặc biệt:

1halt() không bao giờ sai.

Được.

Turing nói đại ý:

Cho tôi mượn cái chương trình đó một chút.

Từ halt, ta tạo một chương trình mới.

Gọi nó là weird.

1def weird(program):
2    if halt(program, program):
3        while True:
4            pass
5    else:
6        return

Nhìn kỹ.

weird(program) hỏi:

Nếu chương trình program, khi nhận chính nó làm input, sẽ dừng thì sao?

Nếu halt nói:

1Có, nó sẽ dừng.

thì weird cố tình:

1while True:
2    pass

tức là chạy mãi.

Còn nếu halt nói:

1Không, nó sẽ chạy mãi.

thì weird lập tức:

1return

tức là dừng.

Nói cách khác, weird là một đứa trẻ nghịch ngợm:

Bạn nói tôi dừng thì tôi chạy mãi.

Bạn nói tôi chạy mãi thì tôi dừng.

Cho tới đây vẫn chưa có vụ nổ nào.

Bây giờ ta làm một việc cực kỳ tà đạo.

Ta đưa:

1weird

vào chính:

1weird

Tức là chạy:

1weird(weird)

Và vũ trụ bắt đầu phát ra tiếng rẹt rẹt.

Nghịch lý xuất hiện

Ta hỏi:

weird(weird) có dừng không?

Có hai khả năng.

Khả năng 1: HALT nói nó sẽ dừng

Giả sử:

1halt(weird, weird) == True

Theo định nghĩa của weird:

1while True:
2    pass

Nó chạy mãi.

Vậy HALT nói:

Nó dừng.

Nhưng nó không dừng.

HALT sai.

Khả năng 2: HALT nói nó sẽ không dừng

Giả sử:

1halt(weird, weird) == False

Theo định nghĩa:

1return

weird lập tức dừng.

HALT lại sai.

Ta có:

1HALT nói DỪNG
2→ chương trình KHÔNG DỪNG
3
4HALT nói KHÔNG DỪNG
5→ chương trình DỪNG

Không còn lựa chọn thứ ba.

Vậy giả định ban đầu:

tồn tại một HALT luôn đúng

phải sai.

Hay nói theo kiểu toán học:

$$ \boxed{\text{Halting Problem là undecidable}} $$

Không tồn tại thuật toán tổng quát giải nó cho mọi chương trình và mọi input. Đây là dạng chứng minh phản chứng kết hợp với tự tham chiếu/diagonalization thường được dùng để trình bày tính không quyết định được của Halting Problem. (Stanford Encyclopedia of Philosophy)

Một hình dễ nhớ

Ta có thể hình dung toàn bộ chứng minh bằng sơ đồ:

 1                 ┌─────────────────┐
 2 program ───────▶│      HALT       │
 3                 │                 │
 4                 │ chương trình có │
 5                 │ dừng hay không? │
 6                 └────────┬────────┘
 7                          │
 8                ┌─────────┴─────────┐
 9                │                   │
10             DỪNG                KHÔNG DỪNG
11                │                   │
12                ▼                   ▼
13          ┌───────────┐        ┌───────────┐
14          │ chạy mãi  │        │   dừng    │
15          └───────────┘        └───────────┘
16                │                   │
17                └─────────┬─────────┘
18                          ▼
19                     MÂU THUẪN

Ta dựng một chương trình cố tình làm ngược lại lời tiên tri.

Rồi bắt lời tiên tri dự đoán chính chương trình đó.

Và lời tiên tri tự cắn vào đuôi mình.

Một phiên bản đời thường

Tưởng tượng có một ông thầy bói máy tính tên HALT.

Ông tuyên bố:

Tôi nhìn bất kỳ chương trình nào cũng biết nó sẽ dừng hay chạy mãi.

Một đứa trẻ tên Weird xuất hiện.

Weird nói:

Nếu ông bảo cháu ngồi xuống, cháu sẽ đứng mãi.

Nếu ông bảo cháu đứng mãi, cháu sẽ ngồi xuống.

Bây giờ hỏi ông thầy bói:

Weird sẽ làm gì khi nghe chính lời tiên đoán của ông?

Ông nói:

Nó sẽ ngồi.

Weird đứng.

Ông nói:

Nó sẽ đứng.

Weird ngồi.

Thầy bói bắt đầu nhìn xa xăm ra cửa sổ.

Không phải vì ông chưa đủ thông minh.

Mà vì yêu cầu đặt ra cho ông chứa một mâu thuẫn tự tham chiếu.

Đó chính là linh hồn của chứng minh.

Máy Turing là gì mà ghê vậy?

Turing không cần laptop.

Không cần Python.

Không cần CPU x86.

Ông tưởng tượng ra một chiếc máy cực kỳ đơn giản gồm:

• một dải băng dài tùy ý,
• các ô chứa ký hiệu,
• một đầu đọc/ghi,
• một tập trạng thái,
• vài luật kiểu “đọc ký hiệu này thì ghi ký hiệu kia rồi đi trái/phải”.

Một phiên bản trực quan có thể tưởng tượng như:

1... | 0 | 1 | 1 | 0 | _ | _ | _ | ...
2          ^
3        đầu đọc

Chiếc máy bé tí về ý tưởng này được gọi là Turing Machine.

Điều quan trọng không phải là nó giống máy tính hiện đại.

Nó không giống.

Điều quan trọng là nó mô hình hóa khái niệm:

một quá trình tính toán theo từng bước rõ ràng.

Turing Machine ngày nay là một trong những mô hình nền tảng của lý thuyết computability. (Stanford Encyclopedia of Philosophy)

Nếu một bài toán không thể giải bằng Turing Machine, thì theo cách hiểu chuẩn của Church–Turing thesis, việc thay Python bằng C++, đổi CPU thành GPU hay mua thêm server không tự nhiên làm bài toán đó trở nên tính được. (Stanford Encyclopedia of Philosophy)

Điều đáng sợ: chương trình có thể chứa toán học

Đây là chỗ Halting Problem từ chuyện code bỗng trượt xuống tầng triết học.

Ta có thể viết chương trình:

1def search():
2    for n in range(1, infinity):
3        if found_counterexample(n):
4            return n

Chương trình sẽ:

• dừng nếu tìm được phản ví dụ,
• chạy mãi nếu không tồn tại phản ví dụ.

Vậy câu hỏi:

Chương trình có dừng không?

đôi khi tương đương với:

Một mệnh đề toán học nào đó có đúng không?

Stanford Encyclopedia đưa ra một ví dụ lịch sử tương tự: có thể hình dung một máy tìm phản ví dụ cho Định lý cuối cùng của Fermat và chỉ dừng nếu tìm thấy; trước khi định lý được chứng minh, việc biết máy ấy có dừng gắn trực tiếp với việc giải một bài toán toán học sâu. (Stanford Encyclopedia of Philosophy)

Một chương trình nhỏ bé có thể giấu bên trong nó một câu hỏi toán học khổng lồ.

CPU cứ chạy:

1tick
2tick
3tick
4tick

Nhưng phía sau những tiếng tick đó có thể là câu hỏi mà cả nhân loại chưa biết đáp án.

“Thế AI có giải được không?”

Không, nếu câu hỏi là:

Một AI có thể tạo ra thuật toán giải Halting Problem chính xác cho mọi chương trình không?

Dù AI thông minh tới đâu, nếu nó vẫn thực hiện một quá trình tính toán theo mô hình thông thường, Halting Problem vẫn đứng đó.

AI có thể rất giỏi dự đoán.

Ví dụ nhìn:

1while True:
2    pass

và nói:

99,999999% cái này chạy mãi anh ạ.

Đúng.

AI cũng có thể phân tích được hàng triệu chương trình thực tế.

Compiler cũng có thể phát hiện vô số infinite loop.

Static analyzer cũng có thể chứng minh termination cho nhiều lớp chương trình.

Nhưng:

1giải được rất nhiều trường hợp

không đồng nghĩa với:

1giải được mọi trường hợp.

Halting Problem chỉ cấm điều thứ hai.

Đây là khác biệt cực kỳ quan trọng.

Vậy công cụ kiểm tra code hiện nay làm thế nào?

Nếu Halting Problem không giải được, tại sao IDE vẫn cảnh báo:

1Infinite loop detected

Bởi vì công cụ không cần giải bài toán tổng quát.

Nó có thể sử dụng:

• pattern matching,
• control-flow analysis,
• symbolic execution,
• abstract interpretation,
• theorem proving,
• timeout,
• heuristic,
• giới hạn một tập chương trình cụ thể.

Ví dụ:

1while True:
2    pass

quá dễ phát hiện.

Hoặc:

1x = 10
2
3while x > 0:
4    x -= 1

ta có thể chứng minh rằng sau 10 vòng:

1x = 0

và chương trình dừng.

Một công cụ có thể cực kỳ hữu dụng dù không giải được mọi trường hợp.

Giống bác sĩ không cần chữa được mọi căn bệnh mới được gọi là bác sĩ.

Halting Problem không nói rằng chúng ta bất lực

Đây cũng là một hiểu lầm phổ biến.

Turing không nói:

Không thể biết chương trình nào dừng.

Rõ ràng ta biết hàng tỷ chương trình dừng.

Ông cũng không nói:

Không có công cụ nào phát hiện infinite loop.

Có đầy.

Điều kết quả nói là:

Không tồn tại một phương pháp thuật toán duy nhất luôn kết thúc và luôn trả lời chính xác cho mọi cặp chương trình-input.

Một vài trường hợp ta chứng minh được.

Một vài trường hợp ta chạy thử được.

Một vài trường hợp ta suy luận được.

Nhưng không có vị thần phần mềm đứng trên tất cả chương trình và luôn phán:

1DỪNG

hoặc:

1KHÔNG DỪNG

mà không bao giờ sai.

Một chi tiết lịch sử nhỏ nhưng quan trọng

Ta thường nghe:

“Turing chứng minh Halting Problem năm 1936.”

Nói vậy để học thì tương đối ổn, nhưng nếu soi kỹ lịch sử thì hơi đơn giản hóa.

Trong bài On Computable Numbers, with an Application to the Entscheidungsproblem, Turing nghiên cứu các máy tính số thực và xây dựng những bài toán như việc xác định một machine có thuộc loại “circle-free” hay không, cùng những bài toán liên quan tới việc machine có in một ký hiệu hay không.

Từ đó ông chứng minh rằng không tồn tại thủ tục quyết định tổng quát cho Entscheidungsproblem.

Phiên bản HALT? hiện đại:

“Cho chương trình $P$ và input $x$, $P(x)$ có dừng không?”

là cách trình bày chuẩn hóa và nổi tiếng sau này, rất gần về bản chất với những kết quả Turing đã xây dựng. (Stanford Encyclopedia of Philosophy)

Chi tiết này không làm kết quả yếu đi.

Ngược lại, nó cho thấy Turing đang nghiên cứu một câu hỏi lớn hơn:

Rốt cuộc cái gì có thể được tính bằng một quy trình máy móc?

Từ Halting Problem tới một ranh giới của tri thức

Đây là phần mình thấy thú vị nhất.

Khi mới học lập trình, ta thường tưởng thế giới chia thành hai loại:

1Bài toán đã có thuật toán.
2Bài toán chưa tìm ra thuật toán.

Nếu chưa giải được thì cứ nghiên cứu tiếp.

CPU nhanh hơn.

RAM nhiều hơn.

AI tốt hơn.

Một ngày nào đó sẽ giải.

Halting Problem thêm vào một loại thứ ba:

1Bài toán mà ta có thể chứng minh rằng
2không có thuật toán tổng quát nào giải được.

Đây là một bước chuyển rất lớn về tư duy.

Không còn hỏi:

Máy tính mạnh tới mức nào?

Mà hỏi:

Khái niệm “tính toán” tự nó có biên giới ở đâu?

Ta đang đứng trước một sinh vật kỳ lạ do chính con người tạo ra.

Nó có thể nhân hàng tỷ số.

Đi xuyên qua hàng petabyte dữ liệu.

Huấn luyện những mạng neural có hàng trăm tỷ tham số.

Mô phỏng protein.

Viết code.

Nói chuyện với con người.

Nhưng ở sâu dưới tất cả silicon, transistor, RAM, GPU và những datacenter đang gầm rú vì quạt làm mát, vẫn có một bức tường vô hình được dựng lên không phải bởi kỹ thuật chế tạo chip, mà bởi logic.

Bạn không thể nâng cấp RAM để đi xuyên qua nó.

Không thể thêm GPU để phá nó.

Không thể overclock logic.

Mối liên hệ kỳ lạ với Gödel và Cantor

Nếu đã từng đọc về Cantor hay Gödel, đoạn chứng minh Halting Problem có một mùi rất quen.

Cantor hỏi về kích thước của vô hạn.

Ông dùng diagonalization để tạo ra một phần tử không thể nằm trong danh sách đang giả định là đầy đủ.

Gödel xây dựng những mệnh đề có khả năng nói về chính khả năng chứng minh của chúng.

Turing làm một trò họ hàng:

Cho chương trình đọc mô tả của chính chương trình.

Rồi đảo hành vi của nó.

Có một mô-típ lặp đi lặp lại:

1Danh sách nói rằng nó chứa tất cả?
2→ dựng thứ nằm ngoài danh sách.
3
4Hệ thống nói rằng nó chứng minh mọi chân lý?
5→ dựng mệnh đề quay lại nói về hệ thống.
6
7Máy nói rằng nó dự đoán mọi chương trình?
8→ dựng chương trình làm ngược lời dự đoán.

Con rắn quay lại cắn đuôi.

Và chính khoảnh khắc tự tham chiếu đó làm xuất hiện giới hạn.

Một ví dụ Python để nghịch

Đương nhiên Python không thể triển khai halt() thật.

Nhưng ta có thể viết pseudo-code để thấy nghịch lý:

 1def halt(program, x):
 2    # Giả sử tồn tại một phép màu
 3    # trả về chính xác program(x) có dừng hay không.
 4    ...
 5
 6def weird(program):
 7    if halt(program, program):
 8        while True:
 9            pass
10    else:
11        return

Bây giờ xét:

1weird(weird)

Nếu:

1halt(weird, weird) == True

thì weird chạy mãi.

Nếu:

1halt(weird, weird) == False

thì weird dừng.

Vậy halt không thể luôn đúng.

Đừng cố chạy code này rồi nhắn mình:

Anh ơi code thiếu implementation của halt.

Đúng.

Đó chính là vấn đề của cả bài.

Nếu viết được phần đó thì chắc chúng ta vừa đập vỡ một mảng lý thuyết tính toán.

Tổng kết

Halting Problem bắt đầu từ một câu hỏi nghe ngây thơ:

Chương trình này có bao giờ chạy xong không?

Nhưng khi yêu cầu một thuật toán phải trả lời câu hỏi đó cho mọi chương trình, mọi thứ sụp xuống.

Ta giả sử tồn tại một máy dự đoán hoàn hảo.

Ta tạo một chương trình làm ngược lời dự đoán.

Ta cho chương trình đó nhìn vào chính nó.

Và mâu thuẫn xuất hiện.

Ý chính có thể gói lại như sau:

1Halting Problem không khó vì máy tính chưa đủ mạnh.
2
3Nó không khó vì chúng ta chưa nghĩ ra thuật toán.
4
5Nó không khó vì thiếu dữ liệu.
6
7Nó không khó vì thiếu thời gian.
8
9Nó không có thuật toán tổng quát.

Turing đã giúp khoa học máy tính nhận ra một điều khá đẹp mà cũng khá đáng sợ:

Trước khi hỏi một bài toán cần bao nhiêu CPU, bao nhiêu RAM và chạy bao lâu, đôi khi ta nên hỏi một câu còn sâu hơn:

Liệu bài toán đó có thể được tính hay không?

Máy tính hiện đại có thể chứa hàng chục tỷ transistor.

Chúng ta có thể nối hàng nghìn GPU thành những cụm máy khổng lồ.

Nhưng giữa biển silicon nóng rực đó vẫn có những câu hỏi nhỏ bé mà không chiếc máy nào có thể luôn trả lời.

Không phải vì máy chưa đủ lớn.

Mà bởi vì đôi khi, logic đã đóng cửa trước khi electron kịp chạy.

Cảm ơn các bạn đã quan tâm và theo dõi bài viết, hẹn gặp lại ở các bài viết tiếp theo.

Tham khảo

• Stanford Encyclopedia of Philosophy, Turing Machines. Turing Machines – Stanford Encyclopedia of Philosophy
• Stanford Encyclopedia of Philosophy, Computability and Complexity. Computability and Complexity
• Stanford Encyclopedia of Philosophy, The Church-Turing Thesis. The Church-Turing Thesis