Chung qui chỉ tại Cantor (7)

 

"Không. Hồi đó khoa Triết Học không có ai quan tâm đến mấy thứ ấy."

[Alonzo Church trả lời khi được hỏi có quan hệ gì giữa khoa Toán và khoa Triết ở Princeton thời cuối 1920, đầu 1930.]

Bản chất của bài toán Hilbert số 10 nằm ở các câu hỏi: "các hàm nào có thể tính toán được ?", và "thế nào là một giải thuật tính một hàm, hay nói cách khác: tính toán là gì ?". Từ đầu thế kỷ 20, các nhà logic học đã nhận ra rằng một số rất lớn các hàm toán học đều có thể được định nghĩa bằng phương pháp đệ qui (và vài luật đơn giản khác). Tuy vậy, có một số hàm không định nghĩa được theo cách đệ qui sơ đẳng này (primitive recursive), ví dụ như hàm Ackermann vì nó tăng siêu nhanh. Thế là các nhà logic học tập trung đi tìm các hệ thống tạo hàm mạnh hơn, với mục tiêu tối hậu là hệ thống ấy có thể tạo được tất cả các hàm tính toán được.

Alonzo Church (1903-1995) sáng tạo ra hệ thống giải tích lambda (lambda calculus) cho mục tiêu này. Church và Gödel thảo luận về giải tích lambda ở đại học tổng hợp Princton. Lúc đầu Gödel không thích món giải tích này lắm vì Gödel nghĩ hệ thống của Church thiếu động cơ triết học. Church thách thức Gödel sáng tạo ra hệ thống tạo hàm khác mạnh hơn giải tích lambda. Vài tháng sau Gödel nghĩ ra cách cải tiến một ý tưởng của Jacques Herbrand (1908-1931) để tạo nên các hàm đệ qui Herbrand-Gödel, hay gọi ngắn gọi là các hàm đệ qui ( recursive functions). Hóa ra là hai hệ thống này tương đương nhau, nhờ vào các nghiên cứu của Stephen C. Kleene (1909-1994), một học trò của Church. Với kết quả này, Church tin rằng các hàm tính toán được đều là các hàm đệ qui. Niềm tin này thường được gọi là luận đề Church (Church thesis).

Một giải thuật thật ra cũng là một hàm số (hay ánh xạ), ví dụ như giải thuật xếp thứ tự chuyển một dãy số thành dãy có thứ tự. Khi nói đến "tính toán được", ta thực sự muốn nói là "có giải thuật để tính". Vì thế, luận đề Church cũng có thể được phát biểu là: "cái gì tính được bằng một giải thuật thì tính được bằng giải tích lambda". Chú ý rằng "luận đề" có ý nghĩa như một định nghĩa, một tiên đề, không cần phải chứng minh. Vấn đề là ta có tin rằng giải tích lambda nắm bắt được mấu chốt của khái niệm "giải thuật" hay không mà thôi. Năm 1936, Church dùng luận đề này để giải quyết entscheidungsproblem của Hilbert. Ông thiết kế hai biểu thức trong giải tích lambda mà sự tương đương của chúng không thể tính được bằng một hàm đệ qui. Nói cách khác, có các phát biểu toán học không thể chứng minh được một cách cơ bắp (bằng giải thuật).

Giải tích lambda và các hàm đệ qui có ảnh hưởng sâu sắc đến ngành trí tuệ nhân tạo. Các ngôn ngữ hàm (functional languages) thuộc họ Lisp (như Scheme và Common Lisp) đều dựa trên giải tích lambda và định nghĩa đệ qui. (Xem thêm trang nhà của giáo sư John McCarthy.) Bản thân tôi có học một năm về logic với giáo sư Wayne Richter ở đại học Minnesota và dự vài buổi họp nhóm của ông. Một hôm ông tiết lộ rằng ông là một trong các học trò của Alonzo Church! Trong trang nhà của Richter có để cụm từ tiếng Việt: "nhất sư nhì phụ". Hồi đó tôi gặm nhấm các chi tiết thú vị này mất vài hôm.