Tài liệu Ngu_nghia_cua_chuong_trinh_logic_1_gioi_thieu

The semantics of constraint logic programs Ngữ nghĩa của các chương trình logic có ràng buộc Abstract Tóm tắt The Constraint Logic Programming (CLP) Scheme was introduced by Ja€ar and Lassez. The scheme gave a formal framework, based on constraints, for the basic operational, logical and algebraic semantics of an extended class of logic programs. This paper presents for the first time the semantic foundations of CLP in a self-contained and complete package. The main contributions are threefold. First, we extend the original conference paper by presenting definitions and basic semantic constructs from first principles, giving new and complete proofs for the main lemmas. Importantly, we clarify which theorems depend on conditions such as solution compactness, satisfaction completeness and independence of constraints. Second, we generalize the original results to allow for incompleteness of the constraint solver. This is important since almost all CLP systems use an incomplete solver. Third, we give conditions on the (possibly incomplete) solver which ensure that the operational semantics is con¯uent, that is, has independence of literal scheduling. constraint solver: Trình giải quyết. (“chương trình giải” có vẻ hợp lí hơn) operational semantics: Ngữ nghĩa thủ tục (đa số các tác giả khác dùng từ “ngữ nghĩa tác vụ”) Phương pháp lập trình logic có ràng buộc (CLP) do Jaffar và Lassez đưa ra. Phương pháp này dựa trên các ràng buộc, đưa ra một chương trình khung hình thức cho các ngữ nghĩa đại số và logic, tác vụ của một lớp mở rộng các chương trình logic. Lần đầu, bài báo này giới thiệu cơ sở ngữ nghĩa của CLP dưới dạng gói độc lập và hoàn chỉnh. Bài báo này bổ sung thêm ba điểm chính. Thứ nhất, chúng tôi mở rộng bài báo hội nghị ban đầu bằng cách đưa vào các định nghĩa và các cấu trúc ngữ nghĩa cơ bản từ các nguyên lý ban đầu, các chứng minh mới và hoàn chỉnh cho các bổ đề chính. Quan trọng nhất, chúng tôi làm rõ định lí nào phụ thuộc vào các điều kiện chẳng hạn như tính compact của nghiệm, đầy đủ thõa mãn và sự độc lập của các ràng buộc. Thứ hai, chúng tôi tổng quát hóa các kết quả ban đầu có tính đến sự chưa hoàn thiện của các chương trình giải ràng buộc. Điều này là quan trọng bởi vì đa số các hệ CLP dùng một chương trình giải không hoàn chỉnh. Thứ ba, chúng tôi đưa ra các điều kiện cho chương trình giải (có thể là không hoàn chỉnh) đảm bảo rằng ngữ nghĩa tác vụ suy biến (hay hợp lưu), tức là không có sự phụ thuộc vào sự lập trình bằng chữ (hay lập trình theo nghĩa đen, lập trình theo ngữ nghĩa). 1. Introduction 1.Giới thiệu The Constraint Logic Programming (CLP) Scheme was introduced by Ja €ar and Lassez [8]. The scheme gave a formal framework, based on constraints, for the basic operational, logical and algebraic semantics of an extended class of logic programs. This framework extended traditional logic programming in a natural way by gener-alizing the term equations of logic programming to constraints from any pre-defined Phương pháp lập trình logic có ràng buộc (CLP) được đưa ra bởi Jaffar và Lassez [8]. Dựa trên các ràng buộc, phương pháp này đưa ra một chương trình khung hình thức cho các ngữ nghĩa đại số và logic, tác vụ của một lớp mở rộng các chương trình logic. Chương trình khung này đã mở rộng lập trình logic truyền thống theo cách tự nhiên bằng cách tổng quát hóa các phương trình số hạng của lập trình logic cho các ràng buộc từ bất kỳ computation domain. Di€erent classes of constraints give rise to di€erent programming languages with di€erent areas of application. Since then there has been consid-erable interest in the semantics and implementation of CLP languages, in part because they have proven remarkably useful, for systems modeling and for solving complex combinatorial optimization problems [11,20]. miền tính toán được định nghĩa trước. Các lớp ràng buộc khác nhau làm nảy sinh các ngôn ngữ lập trình khác nhau với phạm vi ứng dụng khác nhau. Bởi vì thế nên có sự quan tâm đáng kể đến ngữ nghĩa và sự thực thi các ngôn ngữ CLP, một phần bởi vì chúng rất có ích cho việc mô hình hóa các hệ thống và giải các bài toán tối ưu tổ hợp phức [11,20]. CLP languages have a rich semantic theory which generalizes earlier research into semantics for logic programs. In the context of logic programs, van Emden and Ko-walski [4] gave a simple and elegant fixpoint and model theoretic semantics for def-inite clause logic programs based on the least Herbrand model of a program. Apt and van Emden [1] extended this work to establish the soundness and completeness of the operational semantics (SLD resolution) with respect to success and to charac-terize finite failure. Clark [2] introduced the program completion as a logical seman-tics for finite failure and proved soundness of the operational semantics with respect to the completion. Ja€ar et al. [9] proved completeness of the operational semantics with respect to the completion. Together these results provide an elegant algebraic, fixpoint and logical semantics for pure logic programs. The book of Lloyd [17] pro-vides a detailed introduction to the semantics of logic programs. Fixpoint: điểm bất động (điểm bất động, điểm mốc hay điểm cố định cũng là như nhau thôi) Các ngôn ngữ CLP có lí thuyết ngữ nghĩa phong phú, nó tổng quát hóa những nghiên cứu trước đây thành ngữ nghĩa cho các chương trình logic. Trong khuôn khổ của các chương trình logic, van Emden và Ko-walski [4] đã đưa ra một điểm mốc đơn giản và tinh tế và các ngữ nghĩa lí thuyết mô hình cho các chương trình logic mệnh đề xác định dựa trên mô hình Herbrand nhỏ nhất của một chương trình. Apt và van Emden [1] đã mở rộng công trình này để thiết lập thành công tính đúng đắn và hoàn chỉnh của các ngữ nghĩa tác vụ (phân giải SLD) và xác định lỗi hữu hạn. Clark [2] đã hoàn chỉnh chương trình dưới dạng ngữ nghĩa logic cho lỗi hữu hạn và đã chứng minh tính đúng đắn của ngữ nghĩa logic đối với phần bổ sung. Jaffar và các cộng sự [9] đã chứng minh tính đầy đủ của các ngữ nghĩa tác vụ đối với phần bổ sung. Các kết quả này cùng nhau cung cấp một phép toán đại số tinh tế, điểm mốc và các ngữ nghĩa logic cho các chương trình logic thuần túy. Sách của Lloyd [17] giới thiệu chi tiết về ngữ nghĩa của các chương trình logic. One natural generalization of logic programs is to allow di€erent uni®cation mechanisms in the operational semantics. Such a generalization was welcomed since it promised the integration of the functional and logical programming paradigms. Ja€ar et al. [10] generalized the theory of pure logic programs to a logic program-ming scheme which was parametric in the underlying equality theory, and proved that the main semantic results continued to hold. However, the theory of logic pro-grams with equality was still not powerful enough to handle logic languages which provided more than equations. In particular, Prolog II [3] provided inequations over the rational trees. Ja€ar and Stuckey [13] showed that the standard semantic results still held for Prolog II in the presence of inequations. The CLP Scheme generalized these two strands of work to provide a scheme over arbitrary constraints which could be equations, inequations or whatever. Somewhat surprisingly, the key results for the logic programming semantics continue to hold in this much more general set-ting. Indeed, as we shall show, presenting the standard logic programming results in terms of CLP actually results in a more direct and elegant formalization and pro-vides deeper insight into why the results hold for logic programming. Sự tổng quát hóa tự nhiên các chương trình logic cho phép các cơ chế hợp nhất khác nhau trong ngữ nghĩa tác vụ. Một sự tổng quát hóa như thế được hoan nghênh bởi vì nó hứa hẹn sự tích hợp của các mô hình lập trình chức năng và logic. Jaffar và các cộng sự [10] đã tổng quát hóa lí thuyết của các chương trình logic thuần túy cho phương pháp lập trình logic là tham số trong lí thuyết phương trình cơ bản, và đã chứng minh các kết quả ngữ nghĩa chính vẫn còn đúng. Tuy nhiên, lí thuyết chương trình logic với đẳng thức vẫn chưa đủ mạnh để xử lí các chương trình logic cung cấp nhiều chương trình hơn. Đặc biệt, Prolog II [3] đã cung cấp các bất phương trình trên các cây hữu tỉ. Jaffar và Stuckey [13] đã chứng tỏ rằng các kết quả ngữ nghĩa tiêu chuẩn vẫn còn đúng đối với Prolog II khi có các bất phương trình. Phương pháp CLP đã tổng quát hóa hai phần này của công trình để đưa ra một Phương pháp trên các ràng buộc tùy ý có thể là các phương trình, các bất phương trình hay bất cứ thứ gì. Khá ngạc nhiên, các kết quả then chốt của ngữ nghĩa lập trình logic tiếp tục đúng trong thiết lập tổng quát hóa hơn nhiều. Thực sự, như chúng ta sẽ chứng minh, đưa vào các kết quả logic lặp trình tiêu chuẩn theo CLP thực sự dẫn đến hình thức luận trực tiếp và tinh tế hơn và giúp chúng ta hiểu sâu hơn tại sao các kết quả đúng cho lập trình logic. This paper presents for the ®rst time the semantic foundations of CLP in a selfcontained and complete package. The original presentation of the CLP scheme was in the form of an extended abstract [8], referring much of the technical details, including all formal proofs, to an unpublished report [7]. The conference paper of Maher [18] provided a stronger completeness result. Subsequent papers on CLP semantics have either been partial in the sense that they focus on certain aspects only, or they have been informal, being part of a tutorial or survey. Indeed, Ja€ar and Maher's comprehensive survey of CLP [11] did not present the semantics in a formal way, nor include any important proofs. The main contributions of the present paper are: Trước hết, bài báo này đưa vào cơ sở ngữ nghĩa của CLP dưới dạng gói độc lập và hoàn chỉnh. Ban đầu, Phương pháp CLP được đưa ra dưới dạng một báo cáo tóm tắt mở rộng [8], đề cập đến nhiều chi tiết kỹ thuật, bao gồm tất cả các chứng minh hình thức, của một báo cáo chưa xuấn bản [7]. Bài báo hội nghị của Maher [18] đã cung cấp một kết quả hoàn chỉnh mạnh hơn. Các bài báo tiếp theo về ngữ nghĩa CLP hoặc là cục bộ, tức là họ chỉ tập trung vào những khía cạnh nào đó, hoặc không chính thức, là một phần của bài giảng hoặc cuộc khảo sát. Thực sự, khảo sát hoàn chỉnh của Jaffar và Maher về CLP [11] không đưa vào các ngữ nghĩa dưới dạng hình thức, cũng không đề cập đến các chứng minh quan trọng. Các đóng góp chính của bài báo này là như sau: We extend the original conference papers by presenting de®nitions and basic semantic constructs from ®rst principles, with motivating discussions and examples, and give new and complete proofs for the main lemmas. Importantly, we clarify which theorems depend on conditions such as solution compactness, satisfaction completeness and independence of constraints. Chúng tôi mở rộng các bài báo hội nghị ban đầu bằng cách đưa vào các định nghĩa và các cấu trúc ngữ nghĩa chính từ các nguyên lý thứ nhất, chú trọng các thảo luận và ví dụ, và đưa ra các chứng minh mới và hoàn chỉnh các bổ đề chính. Quan trọng là, chúng tôi làm rõ định lí nào phụ thuộc vào các điều kiện chẳng hạn như tính compact của nghiệm, đầy đủ thõa mãn và sự độc lập của các ràng buộc. We generalize the original results to allow for incompleteness of the constraint solver. This is important since almost all CLP systems use an incomplete solver. Chúng tôi tổng quát hóa các kết quả ban đầu có tính đến sự chưa hoàn thiện của các chương trình giải ràng buộc. Điều này là quan trọng bởi vì đa số các hệ CLP dùng một chương trình giải không hoàn chỉnh. We give conditions on the (possibly incomplete) solver which ensure that the operational semantics is con¯uent, that is, has independence of literal scheduling. Chúng tôi đưa ra các điều kiện cho chương trình giải (có thể là không hoàn chỉnh) đảm bảo rằng ngữ nghĩa tác vụ suy biến (hay hợp lưu), tức là không phụ thuộc vào sự lập trình theo nghĩa đen. A synopsis is as follows. In Section 2 we introduce the notions of constraints, solvers and constraint domains. In Section 3 the operational semantics of CLP is in-troduced, together with breadth-®rst derivations. In Section 4, soundness and com-pleteness results for successful derivations are derived. Also, two ®xpoint semantics are introduced. In Section 5 we give soundness and completeness results for ®nite failure. Section 6 summarizes our main results and relates them to the standard re-sults for logic programming. . Also, two ®xpoint semantics are introduced.: câu này chưa dịch soundness and completeness: cần và đủ như vậy “soundness and com-pleteness results” phải dịch là “các kết quả cần và đủ” ????? Thường chúng ta chỉ nghe nói “ điều kiện cần và đủ” chứ ai lại nói “các kết quả cần và đủ”. Nội dung bài báo như sau. Trong phần 2 chúng tôi giới thiệu khái niệm ràng buộc, các chương trình giải và các vùng ràng buộc. Trong phần 3, ngữ nghĩa tác vụ của CLP được giới thiệu, cùng với các suy diễn theo chiều rộng. Trong phần 4, các kết quả đúng đắn và hoàn chỉnh của những suy luận thành công được rút ra. Trong phần 5, chúng tôi đưa ra các kết quả đúng đắn và hoàn chỉnh đối với lỗi xác định. Phần 6 tóm tắt các kết quả chính của chúng tôi và làm rõ mối quan hệ của chúng với các kết quả tiêu chuẩn đối với lập trình logic.