Luận đề Church–Turing

Luận đề Church–Turing khẳng định rằng mọi hàm số có thể tính toán được bằng bất kỳ quy trình hiệu quả nào đều có thể tính toán được bằng máy Turing, qua đó đồng nhất ý tưởng không chính thức về thuật toán với một mô hình toán học chính xác.

Definition

Luận đề Church–Turing là khẳng định rằng các hàm số có thể tính toán một cách trực quan chính là các hàm số có thể tính toán được bằng máy Turing, tương đương với phép tính lambda hoặc các hàm đệ quy tổng quát; đây là một luận đề chứ không phải một định lý vì khái niệm trực quan không được định nghĩa một cách hình thức.

Scope

Chủ đề này bao gồm phát biểu của luận đề, bằng chứng hội tụ từ các mô hình được đề xuất độc lập, sự phân biệt giữa luận đề gốc về khả năng tính toán hiệu quả và các biến thể vật lý hoặc lý thuyết độ phức tạp mạnh hơn, cũng như vai trò của luận đề như một cầu nối giữa trực giác và chứng minh hình thức trong lý thuyết tính toán.

Core questions

• Việc đồng nhất khái niệm thuật toán không chính thức với một mô hình hình thức có ý nghĩa gì?
• Tại sao sự hội tụ của các mô hình độc lập được coi là bằng chứng mạnh mẽ cho luận đề?
• Luận đề này là một định lý toán học, một định nghĩa, hay một khẳng định thực nghiệm?
• Các phiên bản vật lý và lý thuyết độ phức tạp vượt ra ngoài phát biểu gốc như thế nào?

Key theories

Sự hội tụ của các mô hình tính toán

Máy Turing, phép tính lambda của Church, và các hàm đệ quy của Gödel và Herbrand đã được chứng minh là định nghĩa chính xác cùng một lớp hàm số, và sự đồng thuận độc lập này là bằng chứng chính được đưa ra cho luận đề.

Tư cách là một luận đề, không phải một định lý

Vì khái niệm trực quan về quy trình hiệu quả không được hình thức hóa, nên khẳng định này không thể được chứng minh; nó được chấp nhận như một sự đồng nhất nền tảng cho phép các lập luận thuật toán không chính thức thay thế cho các cấu trúc máy Turing hình thức.

Clinical relevance

Luận đề này cho phép thực hành hàng ngày việc mô tả các thuật toán bằng mã giả cấp cao thay vì bằng máy Turing, vì mọi khái niệm hợp lý về quy trình hiệu quả đều được giả định là tương đương Turing; nó cũng định hình các cuộc tranh luận về việc liệu các thiết bị vật lý hoặc lượng tử có thể tính toán vượt ra ngoài khả năng tính toán của Turing hay không.

History

Năm 1936, Church đề xuất đồng nhất khả năng tính toán hiệu quả với khả năng định nghĩa bằng lambda, và Turing độc lập đưa ra lập luận cho mô hình máy của mình, sau đó Turing, Kleene và những người khác đã chứng minh sự tương đương của các mô hình này và các hàm đệ quy. Gödel, ban đầu hoài nghi, sau đó đã coi phân tích của Turing là thuyết phục, và khẳng định tổng hợp này được gọi là luận đề Church–Turing.

Debates

Liệu tính toán vật lý có thể vượt qua giới hạn Turing không?

Luận đề gốc liên quan đến các quy trình hiệu quả, nhưng các phiên bản vật lý mạnh hơn khẳng định rằng không có thiết bị vật lý nào có thể tính toán các hàm không thể tính toán bằng Turing. Các đề xuất về siêu tính toán và ý nghĩa của cơ học lượng tử khiến khẳng định mở rộng này vẫn còn gây tranh cãi, ngay cả khi luận đề cổ điển vẫn không bị thách thức về cơ bản.

Key figures

• Alonzo Church
• Alan Turing
• Kurt Gödel
• Stephen Kleene

Seminal works

• church1936
• turing1937

Frequently asked questions

Tại sao nó được gọi là một luận đề chứ không phải một định lý?

Nó kết nối một mô hình hình thức với ý tưởng không chính thức về một quy trình hiệu quả, và ý tưởng không chính thức đó không có định nghĩa toán học để chứng minh. Bằng chứng mạnh mẽ là mọi nỗ lực độc lập nhằm hình thức hóa tính toán đều cho ra cùng một lớp hàm số, nhưng sự hỗ trợ này mang tính khái niệm hơn là một bằng chứng.

Máy tính lượng tử có bác bỏ luận đề Church–Turing không?

Không. Máy tính lượng tử có thể giải quyết một số vấn đề nhanh hơn, nhưng chúng tính toán chính xác cùng một lớp hàm số như máy Turing, vì vậy luận đề gốc về khả năng tính toán vẫn đúng. Thay vào đó, chúng liên quan đến phiên bản lý thuyết độ phức tạp mạnh hơn, quan tâm đến hiệu quả hơn là khả năng tính toán.