Lập trình logic và khai báo

Lập trình logic và khai báo thể hiện các vấn đề dưới dạng các quan hệ, sự kiện và quy tắc, giao việc tìm kiếm giải pháp cho một công cụ suy luận thay vì các hướng dẫn từng bước rõ ràng.

Definition

Lập trình logic là một mô hình khai báo trong đó một chương trình là một tập hợp các mệnh đề logic (sự kiện và quy tắc), và tính toán được tiến hành bằng suy luận tự động, điển hình là phép phân giải với hợp nhất, để trả lời các truy vấn dựa trên tri thức đó.

Scope

Chủ đề này bao gồm lập trình logic dựa trên mệnh đề Horn và phép phân giải (như trong Prolog), lập trình logic ràng buộc, và ý tưởng khai báo rộng hơn về việc chỉ định điều gì nên đúng hơn là cách tính toán nó. Nó bao gồm hợp nhất, tìm kiếm quay lui, ngữ nghĩa lý thuyết mô hình và lý thuyết chứng minh của các chương trình logic, và sự tách biệt giữa đặc tả logic và điều khiển.

Core questions

• Việc tính toán bằng cách chứng minh một mục tiêu từ các mệnh đề logic có nghĩa là gì?
• Hợp nhất và quay lui thực hiện tìm kiếm trên một chương trình quan hệ như thế nào?
• Sự tách biệt giữa logic và điều khiển được làm rõ như thế nào?
• Các ràng buộc mở rộng lập trình logic thuần túy như thế nào?

Key theories

Nguyên lý phân giải

Phép phân giải của Robinson đưa ra một quy tắc suy luận duy nhất, định hướng máy móc cho logic bậc nhất, cung cấp công cụ suy luận giúp lập trình logic khả thi về mặt tính toán.

Logic cộng với điều khiển

Phân tích của Kowalski phân biệt nội dung logic của một chương trình (điều gì là đúng) với thành phần điều khiển của nó (cách tìm kiếm chứng minh), định hình lập trình logic như một cách để thay đổi điều khiển trong khi giữ logic cố định.

Ngữ nghĩa khai báo và thủ tục của các chương trình logic

Lloyd hình thức hóa ngữ nghĩa lý thuyết mô hình, điểm cố định và hoạt động của các chương trình logic xác định và chứng minh sự tương ứng của chúng, làm nền tảng cho ý nghĩa của các chương trình logic.

Clinical relevance

Các kỹ thuật khai báo và dựa trên logic làm nền tảng cho các ngôn ngữ truy vấn cơ sở dữ liệu, bộ giải ràng buộc, biểu diễn tri thức và công cụ quy tắc. Việc chúng nhấn mạnh vào việc chỉ định vấn đề hơn là thuật toán khiến chúng rất phù hợp cho các tác vụ tìm kiếm tổ hợp, cấu hình và suy luận.

History

Nguyên lý phân giải năm 1965 của Robinson đã đặt nền tảng suy luận. Đầu những năm 1970, Colmerauer và Roussel đã tạo ra Prolog, và Kowalski đã trình bày rõ cách diễn giải thủ tục của các mệnh đề Horn. Mô hình này phát triển mạnh mẽ trong suốt những năm 1980, ảnh hưởng đến dự án Thế hệ thứ năm của Nhật Bản, và sau đó mở rộng thành lập trình logic ràng buộc và lập trình tập hợp câu trả lời.

Debates

Sự thuần túy so với điều khiển thực tế

Các ngôn ngữ lập trình logic cân bằng lý tưởng về logic khai báo thuần túy với các nhu cầu thực tế về điều khiển rõ ràng, chẳng hạn như cắt và sắp xếp, giúp cải thiện hiệu quả nhưng làm tổn hại đến sự tách biệt logic/điều khiển rõ ràng.

Key figures

• Robert Kowalski
• Alain Colmerauer
• J. Alan Robinson
• John Lloyd
• Philippe Roussel

Seminal works

• kowalski1979
• robinson1965
• lloyd1987
• colmerauer1993

Frequently asked questions

Lập trình logic khác với lập trình mệnh lệnh như thế nào?

Thay vì chỉ định một chuỗi các thao tác, một chương trình logic khai báo các sự kiện và quy tắc, và một công cụ suy luận tìm kiếm các chứng minh để trả lời các truy vấn, do đó lập trình viên tập trung vào điều gì là đúng hơn là cách tính toán nó.

Hợp nhất là gì?

Hợp nhất là quá trình tìm kiếm một phép thế làm cho hai thuật ngữ logic trở nên giống hệt nhau; nó là cơ chế cốt lõi mà các chương trình logic khớp các mục tiêu với các đầu mệnh đề.