Chương trình máy tính và chứng minh toán học tương đương liên kết sâu | Tạp chí Quanta

Một số khám phá khoa học quan trọng vì chúng tiết lộ điều gì đó mới mẻ - chẳng hạn như cấu trúc xoắn kép của DNA hoặc sự tồn tại của các lỗ đen. Tuy nhiên, một số tiết lộ rất sâu sắc vì chúng cho thấy hai khái niệm cũ, từng được cho là khác biệt, thực tế lại giống nhau. Hãy xem các phương trình của James Clerk Maxwell cho thấy điện và từ là hai khía cạnh của một hiện tượng duy nhất, hay thuyết tương đối rộng liên kết lực hấp dẫn với không-thời gian cong.

Sự tương ứng giữa Curry-Howard cũng thực hiện tương tự nhưng ở quy mô lớn hơn, liên kết không chỉ các khái niệm riêng biệt trong một lĩnh vực mà còn toàn bộ các nguyên tắc: Khoa học Máy tính và logic toán học. Còn được gọi là đẳng cấu Curry-Howard (thuật ngữ có nghĩa là tồn tại một số loại tương ứng một-một giữa hai vật), nó thiết lập mối liên hệ giữa chứng minh toán học và chương trình máy tính.

Nói một cách đơn giản, thư từ Curry-Howard thừa nhận rằng hai khái niệm từ khoa học máy tính (loại và chương trình) tương ứng là tương đương với các mệnh đề và bằng chứng - các khái niệm từ logic.

Một phân nhánh của sự tương ứng này là việc lập trình - thường được coi là một nghề thủ công cá nhân - được nâng lên mức lý tưởng hóa của toán học. Viết một chương trình không chỉ là “viết mã”, nó còn trở thành một hành động chứng minh một định lý. Điều này chính thức hóa hoạt động lập trình và cung cấp các cách lập luận toán học về tính đúng đắn của chương trình.

Thư từ này được đặt tên theo hai nhà nghiên cứu đã độc lập phát hiện ra nó. Năm 1934, nhà toán học và logic học Haskell Curry nhận thấy sự tương đồng giữa các hàm số trong toán học và mối quan hệ hàm ý trong logic, mối quan hệ này có dạng câu lệnh “nếu-thì” giữa hai mệnh đề.

Lấy cảm hứng từ quan sát của Curry, nhà logic học toán học William Alvin Howard đã phát hiện ra mối liên hệ sâu sắc hơn giữa tính toán và logic vào năm 1969, cho thấy rằng việc chạy một chương trình máy tính cũng giống như việc đơn giản hóa một chứng minh logic. Khi một chương trình máy tính chạy, mỗi dòng được “đánh giá” để tạo ra một đầu ra duy nhất. Tương tự, trong một chứng minh, bạn bắt đầu bằng những phát biểu phức tạp mà bạn có thể đơn giản hóa (ví dụ: bằng cách loại bỏ các bước dư thừa hoặc thay thế các biểu thức phức tạp bằng những biểu thức đơn giản hơn) cho đến khi bạn đi đến kết luận - một phát biểu cô đọng và ngắn gọn hơn bắt nguồn từ nhiều phát biểu tạm thời. .

Mặc dù mô tả này truyền tải ý nghĩa chung về sự tương ứng, nhưng để hiểu đầy đủ về nó, chúng ta cần tìm hiểu thêm một chút về cái mà các nhà khoa học máy tính gọi là “lý thuyết loại”.

Hãy bắt đầu với một nghịch lý nổi tiếng: Trong một ngôi làng có một người thợ cắt tóc chuyên cạo râu cho tất cả những người đàn ông không tự cạo râu và chỉ họ mà thôi. Thợ cắt tóc có tự cạo râu không? Nếu câu trả lời là có thì anh ta không được tự cạo râu (vì anh ta chỉ cạo cho những người không tự cạo râu). Nếu câu trả lời là không thì anh ta phải tự cạo râu (vì anh ta cạo râu cho tất cả những người đàn ông không tự cạo râu). Đây là phiên bản không chính thức của nghịch lý mà Bertrand Russell đã phát hiện ra khi cố gắng thiết lập nền tảng của toán học bằng cách sử dụng một khái niệm gọi là tập hợp. Nghĩa là, không thể định nghĩa một tập hợp chứa tất cả các tập hợp không chứa chính nó mà không gặp phải mâu thuẫn.

Để tránh nghịch lý này, Russell đã chỉ ra, chúng ta có thể sử dụng “các loại”. Nói một cách đại khái, đây là những danh mục có giá trị cụ thể được gọi là đối tượng. Ví dụ: nếu có một loại tên là “Nat”, nghĩa là số tự nhiên thì đối tượng của nó là 1, 2, 3, v.v. Các nhà nghiên cứu thường sử dụng dấu hai chấm để biểu thị loại đối tượng. Số 7, thuộc loại số nguyên, có thể được viết là “7: Số nguyên”. Bạn có thể có một hàm lấy một đối tượng thuộc loại A và tạo ra một đối tượng thuộc loại B hoặc một hàm kết hợp một cặp đối tượng thuộc loại A và loại B thành một loại mới, được gọi là “A × B”.

Do đó, một cách để giải quyết nghịch lý là đặt những loại này vào một hệ thống phân cấp, để chúng chỉ có thể chứa các phần tử ở “cấp thấp hơn” so với chính chúng. Khi đó một loại không thể chứa chính nó, điều này tránh được sự tự tham chiếu tạo ra nghịch lý.

Trong thế giới của lý thuyết loại, việc chứng minh một tuyên bố là đúng có thể khác với những gì chúng ta đã quen. Nếu chúng ta muốn chứng minh rằng số nguyên 8 là số chẵn thì vấn đề cần chứng minh rằng 8 thực sự là một đối tượng thuộc một loại cụ thể gọi là “Chẵn”, trong đó quy tắc thành viên được chia hết cho 2. Sau khi xác minh rằng 8 chia hết cho 2 đến 8, chúng ta có thể kết luận rằng XNUMX thực sự là một “cư dân” thuộc loại Chẵn.

Curry và Howard đã chỉ ra rằng các loại về cơ bản tương đương với các mệnh đề logic. Khi một hàm “cung cấp” một loại - nghĩa là khi bạn có thể xác định thành công một hàm là đối tượng của loại đó - bạn đang chứng minh một cách hiệu quả rằng mệnh đề tương ứng là đúng. Vì vậy, các hàm nhận đầu vào loại A và cho đầu ra loại B, ký hiệu là loại A → B, phải tương ứng với hàm ý: “Nếu A thì B”. Ví dụ: lấy mệnh đề “Nếu trời mưa thì mặt đất ướt”. Trong lý thuyết loại, mệnh đề này sẽ được mô hình hóa bằng một hàm có kiểu “Mưa → GroundIsWet”. Các công thức trông khác nhau trên thực tế là giống nhau về mặt toán học.

Mối liên kết đó nghe có vẻ trừu tượng nhưng nó không chỉ thay đổi cách những người thực hành toán và khoa học máy tính nghĩ về công việc của họ mà còn dẫn đến một số ứng dụng thực tế trong cả hai lĩnh vực. Đối với khoa học máy tính, nó cung cấp nền tảng lý thuyết cho việc xác minh phần mềm, quá trình đảm bảo tính đúng đắn của phần mềm. Bằng cách đóng khung các hành vi mong muốn theo các mệnh đề logic, các lập trình viên có thể chứng minh một cách toán học rằng một chương trình hoạt động như mong đợi. Nó cũng cung cấp nền tảng lý thuyết vững chắc để thiết kế các ngôn ngữ lập trình chức năng mạnh mẽ hơn.

Và đối với toán học, sự tương ứng đã dẫn đến sự ra đời của trợ lý bằng chứng, còn được gọi là người chứng minh định lý tương tác. Đây là những công cụ phần mềm hỗ trợ xây dựng các bằng chứng chính thức, chẳng hạn như Coq và Lean. Trong Coq, mỗi bước chứng minh về cơ bản là một chương trình và tính hợp lệ của bằng chứng được kiểm tra bằng thuật toán kiểm tra kiểu. Các nhà toán học cũng đang sử dụng các trợ lý chứng minh - đáng chú ý là Người chứng minh định lý Lean - để chính thức hóa toán học, bao gồm việc biểu diễn các khái niệm, định lý và chứng minh toán học theo một định dạng chặt chẽ, có thể kiểm chứng bằng máy tính. Điều đó cho phép ngôn ngữ toán học đôi khi không chính thức được máy tính kiểm tra.

Các nhà nghiên cứu vẫn đang khám phá hậu quả của mối liên hệ giữa toán học và lập trình. Sự tương ứng Curry-Howard ban đầu hợp nhất việc lập trình với một loại logic gọi là logic trực giác, nhưng hóa ra là nhiều loại logic hơn cũng có thể tuân theo sự thống nhất như vậy.

“Điều đã xảy ra trong thế kỷ kể từ cái nhìn sâu sắc của Curry là chúng ta tiếp tục phát hiện ra ngày càng nhiều trường hợp trong đó 'hệ logic X tương ứng với hệ thống tính toán Y'," nói Michael Clarkson, một nhà khoa học máy tính tại Đại học Cornell. Các nhà nghiên cứu đã kết nối việc lập trình với các loại logic khác như logic tuyến tính, bao gồm khái niệm “tài nguyên” và logic phương thức, liên quan đến các khái niệm về khả năng và sự cần thiết.

Và mặc dù bức thư này mang tên Curry và Howard, nhưng họ không phải là những người duy nhất phát hiện ra nó. Điều này chứng thực bản chất cơ bản của sự trao đổi thư từ: Mọi người liên tục chú ý đến nó. “Dường như không phải ngẫu nhiên mà có mối liên hệ sâu sắc giữa tính toán và logic,” Clarkson nói.