Tại sao các hệ thống hình thức không thể tự đọc được đầu ra của chính chúng?

Bài viết đi sâu vào hiện tượng phổ biến giữa ba lĩnh vực tưởng như khác biệt: toán học tổ hợp, thực hành toán học và mô hình ngôn ngữ. Tất cả đều đối mặt với nghịch lý: quá trình đánh giá (evaluation) trong các hệ thống hình thức là quá trình mất mát thông tin, khiến chúng không thể tái hiện ý định ban đầu của người tạo biểu thức chỉ dựa trên nội quy của chính hệ thống đó.

Đánh giá trong chương trình tổ hợp liên kết (Concatenative Combinator Evaluation)

Giả sử một ngôn ngữ tổ hợp đơn giản dựa trên ngăn xếp với các thao tác nguyên thủy như swap, drop, dip, call. Ta có thể định nghĩa các từ mới trong từ điển, ví dụ:

true  := [ swap drop ]
false := [ drop ]
not   := [ [ swap drop ] [ drop ] ] dip call

Khi trình đánh giá thực thi, nó thay thế các từ bằng định nghĩa tương ứng và áp dụng quy tắc rút gọn. Kết quả là biểu thức được rút gọn hoàn toàn thành tổ hợp các thao tác nguyên thủy.

Tuy nhiên, một khi biểu thức đã được rút gọn, chẳng còn dấu vết nào cho thấy nó từng chứa từ not — nó chỉ là ngăn xếp các thao tác rời rạc. Đây là quy luật bình thường của trình đánh giá: nó chỉ rút gọn, không có khả năng "rút ngược" lại thành biểu thức ban đầu.

Vấn đề phản chiếu (Reflection Problem)

Giả sử ta muốn cho hệ thống có khả năng phản chiếu, tức là chương trình có thể tự xem xét cấu trúc của chính nó để kiểm tra xem phần nào đó có trùng khớp với từ trong từ điển không. Đây không phải là thao tác bên ngoài mà phải thực hiện ngay trong phép tính tổ hợp.

Ví dụ, với biểu thức:

[ [ [ swap drop ] [ drop ] ] dip call ]

Ta có thể đọc nó theo 3 cách khác nhau, cùng đúng song không thể phân biệt "đúng cách nào":

• Cấp 0: chỉ nhìn bản thân các thao tác nguyên thủy.
• Cấp 1: nhận dạng một phần như [ [ true false ] dip call ]
• Cấp 2: nhận dạng đầy đủ là [ not ]

Tất cả đều hợp lệ cùng lúc, nhưng hệ thống hình thức không thể tự quyết định cách đọc nào là "chính xác" hay "đúng ý đồ" của người viết.

One expression, three readings — the same reduced form interpreted at different abstraction levels

Tính mơ hồ không phải là chuyện lạ

Tình trạng này tương tự cách ngôn ngữ tự nhiên vận hành. Câu “She is cold” có thể mang nghĩa:

• Cô ấy lạnh nhạt, ít thể hiện cảm xúc hơn người khác.
• Nhiệt độ cơ thể cô ấy thấp hơn bình thường.

Cả hai đều đúng về cấu trúc và ngữ nghĩa nhưng không thể tách bạch chỉ dựa trên câu. Muốn hiểu đúng, ta cần ngữ cảnh, kinh nghiệm, và kiến thức bên ngoài câu chữ.

Tương tự trong hệ thống tổ hợp: biểu thức cho phép nhiều cách hiểu, việc chọn cách hiểu đúng đòi hỏi kiến thức và kinh nghiệm bên ngoài formalism thuần túy.

Giải pháp kỹ thuật và bài toán học máy

Một cách đơn giản là hệ thống không được để mất thông tin gốc: ghi lại toàn bộ quá trình mở rộng từ điển, giữ dấu vết đâu là từ nào.

Nhưng trong thực tế, điều này không khả thi vì:

• Biểu thức đến từ nguồn ngoài không có lịch sử.
• Thuật toán trung gian loại bỏ nhãn hiệu.
• Kích thước dữ liệu gốc quá lớn.
• Các hệ thống cũ không hỗ trợ kiểu theo dõi này.

Khi thông tin gốc không còn, cách duy nhất để giải quyết là dựa vào mô hình học máy có giám sát.

Quy trình là:

1. Hệ thống liệt kê tất cả các cách hiểu hợp lệ, sắp xếp theo heuristic.
2. Người dùng chọn cách hiểu mong muốn trong ngữ cảnh.
3. Mô hình học từ các lựa chọn này.
4. Theo thời gian, mô hình tự dự đoán được lựa chọn mà không cần hỏi lại.

Đây chính là cách hoạt động của các mô hình ngôn ngữ — dự đoán cách hiểu khả thi nhất dựa trên các ví dụ đã học.

Góc nhìn lý thuyết thông tin

Đánh giá là một hàm nhiều vào một ra (many-to-one). Nhiều biểu thức khác nhau khi đánh giá có thể cho cùng kết quả rút gọn. Ví dụ:

• not
• [ true false ] branch
• [ [ swap drop ] [ drop ] ] dip call

tất cả có cùng dạng đầu ra, dẫn tới không thể suy ngược chính xác biểu thức gốc.

Đây là bài toán nghịch đảo liên quan đến mất mát thông tin, tương tự compression hoặc giải mã phần mềm.

Cấu trúc này được mô hình hóa bằng e-graph và phương pháp equality saturation, như thư viện egg nổi tiếng.

Chọn lựa biểu thức tương đương “tốt nhất” từ e-graph theo một hàm chi phí được chứng minh là NP-hard, có nghĩa là chi phí tính toán rất cao.

Điều này chứng tỏ không chỉ việc lưu trữ nhiều cách diễn giải khả thi mà còn chọn lựa cách diễn giải phù hợp phải dựa vào các mô hình học máy dự đoán, vì các hàm chi phí đơn giản không thể tái hiện được ý định người dùng.

Evaluation is many-to-one — multiple source expressions collapse to the same reduced form

Tương tự ở toán học

Các nhà toán học cũng gặp vấn đề tương tự khi làm việc với các biểu thức đại số và kí hiệu:

• Họ có thể nhìn một biểu thức đã tính và “nhận ra” là đại số Lie, hay có hàm delta Dirac ẩn bên trong.
• Việc nhận ra này không phải là suy diễn logic thuần túy mà dựa vào kinh nghiệm tích lũy qua việc làm bài tập, đọc sách, được giảng viên sửa sai.
• Một biểu thức có thể được hiểu theo nhiều cách khác nhau, và người toán chọn giải thích phù hợp dựa trên ngữ cảnh và trực giác.

Quá trình này cũng tương đương với học có giám sát, một mô hình nhận diện mẫu được huấn luyện qua thực tế và phản hồi.

Một sợi dây nối chung

Ba lĩnh vực:

	Toán tổ hợp (Combinator Reflection)	Toán học	Ngôn ngữ tự nhiên
Hệ thống	Toán tổ hợp	Đại số	Ngữ pháp + từ vựng
Biểu thức	Ngăn xếp rút gọn	Kết quả tính toán	Câu
Từ điển	Định nghĩa từ	Các cấu trúc đã biết	Ý nghĩa từ
Mơ hồ	Nhiều cách đọc hợp lệ	Nhiều mô hình có thể nhận dạng	Nhiều cách hiểu
Giải quyết	Heuristic hoặc mô hình học được huấn luyện	Huấn luyện chính quy + trực giác	Suy luận ngữ cảnh + kiến thức

• Hệ thống hình thức tạo ra biểu thức theo quy tắc
• Việc hiểu/suy luận yêu cầu nhận diện bên ngoài
• Mơ hồ không thể tự giải quyết trong hệ thống
• Giải quyết mơ hồ phụ thuộc vào trải nghiệm, trực giác và mô hình học máy

The information gap — production is deterministic, interpretation is ambiguous

Kết luận

Mọi hệ thống hình thức đủ phức tạp để tự phân tích đầu ra của mình theo cách người dùng hiểu sẽ cần tích hợp thành phần tương tự mô hình ngôn ngữ bên trong.

Đây không phải là tiện ích thêm vào mà là một phần tự nhiên bởi:

• Quá trình sản sinh biểu thức là xác định
• Quá trình giải nghĩa biểu thức là mơ hồ và mất thông tin
• Không có cách nào chỉ dựa trên lý luận hình thức để khôi phục toàn bộ ý định

Chúng ta luôn dựa vào học máy để dự đoán được ý nghĩa dựa trên kinh nghiệm trước đó, từ lập trình đến toán học và ngôn ngữ hàng ngày.

---

Tài liệu tham khảo

• Brent Kerby – The Theory of Concatenative Combinators (2002)
  http://tunes.org/~iepos/joy.html

• Foundations of Dawn: The Untyped Concatenative Calculus (2021) – Dawn language project
  https://www.dawn-lang.org/posts/foundations-ucc/

• Max Willsey et al. – egg: Fast and Extensible Equality Saturation (POPL 2021)
  https://egraphs-good.github.io/

• Douglas Hofstadter – Gödel, Escher, Bach: An Eternal Golden Braid (1979)

• Jacques Hadamard – The Psychology of Invention in the Mathematical Field (1945)

• George Pólya – How to Solve It (1945)

• DeepMind et al. (2021) – Machine learning phát hiện giả thuyết toán học mới
  (Davies et al., Nature)

• Dan Jurafsky & James Martin – Speech and Language Processing
  https://web.stanford.edu/~jurafsky/slp3/

• H.P. Grice – Logic and Conversation (1975)

• Sperber & Wilson – Relevance: Communication and Cognition (1986)

Bạn có thể suy nghĩ sâu hơn về mối liên hệ giữa logic tổ hợp, toán học, và học máy trong việc xử lý thông tin mất mát trong hệ thống hình thức. Hẹn gặp lại trong các chủ đề tiếp theo!