Tự xây dựng một chương trình Quine từ Định lý Đệ quy thứ hai của Kleene

Quine — chương trình tự in ra chính mã nguồn của mình — từ lâu đã được biết đến như một hệ quả của Định lý Đệ quy thứ hai của Kleene trong lý thuyết tính toán. Câu hỏi thú vị là: liệu có thể biến chứng minh trừu tượng đó thành một chương trình chạy được trong thực tế hay không? Một bài viết kỹ thuật mới đã thử nghiệm điều này bằng cách hình thức hóa toàn bộ lập luận trong lambda calculus không kiểu và kiểm chứng bằng trợ lý chứng minh Rocq.

Góc nhìn cổ điển của Kleene

Cách trình bày quen thuộc của định lý giả định chúng ta làm việc với một cách đánh số hiệu quả các hàm đệ quy bộ phận $\lbrace \varphi_i \rbrace_{i \in \mathbb{N}}$. Khi đó, định lý phát biểu rằng:

Với mọi hàm đệ quy bộ phận $\psi$ có $n+1$ tham số, tồn tại chỉ số $e$ sao cho $\psi(e,\bar{x}) \simeq \varphi_e(\bar{x})$.

Nếu lấy $\psi$ là hàm đồng nhất, ta thu được ngay hệ quả $e = \psi(e) \simeq \varphi_e()$ — một chỉ số $e$ đóng vai trò như "mã nguồn" của chính nó. Đây chính là hình ảnh trừu tượng của một Quine.

Vấn đề là cách trình bày này thường đi kèm rất nhiều thao tác mã hóa thủ công (cặp, danh sách, đối tượng cú pháp đều bị quy về số tự nhiên), khiến người đọc khó thấy được cấu trúc thực sự của chứng minh.

Chuyển sang góc nhìn lập trình hàm

Tác giả chọn lambda calculus không kiểu vì đây là mô hình tính toán gần với lý thuyết chứng minh nhất, đồng thời đủ đơn giản để tự biểu diễn chính nó. Trước tiên, bài viết trình bày một phiên bản có kiểu của định lý, giả định ngôn ngữ $L$ có khả năng tự phản chiếu, gồm:

• Một kiểu $\mathsf{AST}$ biểu diễn cây cú pháp, với phép "trích dẫn" $\lceil t \rceil$;
• Một hàm quasi-quoter $\mathsf{q}$ biến biểu thức được trích dẫn một lần thành trích dẫn hai lần;
• Phép áp dụng hàm ký hiệu bằng toán tử $\cdot$.

Khi đó, chứng minh chỉ gói gọn trong vài bước: định nghĩa $d := \lambda e. P (e \cdot \mathsf{q}\ e)$, rồi điểm bất động chính là $t := d\ \lceil d \rceil$. Phép tính triệt tiêu nhau đẹp đẽ đến mức toàn bộ định lý trở thành một đẳng thức ngắn gọn $P\ \lceil t \rceil = t$.

Điều đáng chú ý là chứng minh này không đòi hỏi ngôn ngữ phải Turing-complete. Nếu đặt $T = \mathsf{Prop}$, ta thu được bổ đề đường chéo — nền tảng của định lý bất toàn Gödel và định lý không định nghĩa được của Tarski. Ví dụ, lấy $P := \neg \circ \mathsf{Prov}$ sẽ cho ra câu Gödel nổi tiếng.

Xây dựng Quine trong lambda calculus không kiểu

Để hiện thực hóa ý tưởng, cần hai thành phần:

• Mã hóa Church cho cây cú pháp, biểu diễn ba cấu trúc biến, áp dụng và trừu tượng lambda thông qua các hàm bậc cao;
• Quasi-quoter $\mathsf{q}$ — phần phức tạp nhất, được mô tả như một phép fold trên cấu trúc cây, và nhờ bản chất của mã hóa Church, có thể viết gọn thành một biểu thức lambda duy nhất.

Toàn bộ lập luận được thực hiện và kiểm chứng trong Rocq (trợ lý chứng minh trước đây mang tên Coq). Kết quả cuối cùng là một chương trình Quine hoàn chỉnh, in ra dưới dạng ký hiệu de Bruijn — một khối biểu thức lambda lồng nhau dày đặc, nhưng chạy đúng như lý thuyết dự đoán.

Vì sao điều này đáng quan tâm?

Với người làm việc trong lĩnh vực khoa học máy tính và hình thức hóa, bài viết mang lại vài bài học đáng chú ý:

• Hình thức hóa không phải là việc sao chép máy móc: chính quá trình viết chứng minh trong Rocq buộc tác giả phải làm rõ các định nghĩa mơ hồ, và từ đó nảy sinh hiểu biết mới;
• Chọn mô hình tính toán phù hợp quan trọng hơn tối ưu hóa ký hiệu: lambda calculus giúp chứng minh ngắn gọn và có cấu trúc hơn nhiều so với cách mã hóa số tự nhiên truyền thống;
• Cầu nối giữa các lĩnh vực: cùng một định lý, khi nhìn qua lăng kính lập trình hàm, kết nối luôn lý thuyết tính toán, logic toán học và lý thuyết chứng minh.

Với cộng đồng lập trình viên Việt Nam quan tâm đến functional programming, lý thuyết kiểu hay chứng minh hình thức, đây là một ví dụ tiêu biểu cho thấy toán học trừu tượng có thể dẫn thẳng tới một chương trình cụ thể — và đôi khi, chỉ vài dòng lambda là đủ để chạm tới những định lý sâu sắc nhất của khoa học máy tính.