Lý thuyết tính toán

Lý thuyết tính toán, còn được gọi là lý thuyết đệ quy, là một nhánh của logic toán học, của khoa học máy tính và của lý thuyết tính toán (theory of computation) bắt nguồn từ những năm 1930 với nghiên cứu về các hàm tính toán và độ Turing. Lĩnh vực này đã được mở rộng để bao gồm các nghiên cứu về tính toán tổng quát và tính xác định. Trong các lĩnh vực này, lý thuyết đệ quy trùng lặp với lý thuyết chứng minh và lý thuyết tập hợp mô tả hiệu quả.

Các câu hỏi cơ bản được lý thuyết đệ quy nêu ra bao gồm:

• Đối với một hàm trên các số tự nhiên có thể tính toán được, có ý nghĩa gì?
• Làm thế nào các hàm mà không tính toán được phân loại thành một hệ thống phân cấp dựa trên mức độ không tính toán được của chúng?

Mặc dù có sự chồng chéo đáng kể về kiến thức và phương pháp, các nhà lý thuyết đệ quy toán học nghiên cứu lý thuyết về khả năng tính toán tương đối, các khái niệm giảm thiểu và cấu trúc mức độ; những người trong lĩnh vực khoa học máy tính tập trung vào lý thuyết về thứ bậc phụ, phương pháp chính thức và ngôn ngữ chính thức.

Lý thuyết đệ quy bắt nguồn từ những năm 1930, với công trình của Kurt Gödel, Alonzo Church, Rózsa Péter, Alan Turing, Stephen Kleene và Emil Post.^[1][2]

Các kết quả cơ bản mà các nhà nghiên cứu thu được đã thiết lập tính toán Turing như là sự chính thức hóa chính xác của ý tưởng không chính thức về tính toán hiệu quả. Những kết quả này đã khiến Stephen Kleene (1952) đặt ra hai tên "Luận án của Church" (Kleene 1952: 300) và "Luận án của Turing" (Kleene 1952: 376). Ngày nay, những điều này thường được coi là một giả thuyết duy nhất, luận án Church-Turing, nói rằng bất kỳ hàm nào có thể tính toán được bằng thuật toán là một hàm tính toán được. Mặc dù ban đầu còn hoài nghi, đến năm 1946, Gôdel đã lập luận ủng hộ luận điểm này: