Tài liệu Nghiên cứu một số khía cạnh lý thuyết của lập trình Logic và lập trình Logic Modal

T f" ' ĐẠI HỌC Qưóc Gỉ A HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Đ Ỗ T H A N H TH Ủ Y NGHIÊN CỨU MỘT SỐ KHÍA CẠNH LÝ THUYẾT CỦA LẬP TRÌNH LỎGIC VÀ LẬP TRÌNH LOGIC MODAL Chuyên ngành: Mã số: Công nghệ thông tin 1.0U 0 LU ẬN VẦN TH ẠC s ĩ • ■ N gười hướng dẫn khoa học: PGS.TS. Hồ Thuần o ạ : h ọ c QUOC G i- ' . : 'RUNG ĨẢ M t h o n g t in thì, r V- lo I lộĩ I ir r; í ) h > Hà Nội - 2 0 0 5 ( M ụ■ c lục ■ Lời cảm ơn................................................................................................................1 Mục lục.................................................................................................................... 2 Mở đầu..................................................................................................................... 4 Chương 1. Tổng quan về lập trình logic............................................................... 6 1.1. Giới thiệu về lập trình logic....................................................................... 6 1.2. Lập trình logic - các nội dung đang đượcnghiên cứu............................. 7 1.3. Lập trình logic trone tương la i................................................................ 10 Chương 2. Các nguyên lý cơ s ờ .......................................................................... 11 2 . 1 . C h ư ơ n g t r i n h l o g i c ................................................................................................................................11 2.1.1. Câu logic............................................................................................. 11 2.1.2. Câu chương trình............................................................................... 12 2.1.3. Chương trình logic............................................................................. 13 2.2. Hệ quá logic và các mô hình....................................................................13 2 . 2 . 1 . H ệ q u ả l o g i c ....................................................................................................................................1 5 2.2.2. Mô hình Herbranđ nhỏ nhất............................................................. 16 2.2.3. Xây dựng mô hình Herbrand nhò nhất............................................19 2.3. Điểm bất động.......................................................................................... 20 2.4. Thuật giải SL D ......................................................................................... 23 2.4.1. Nội dung thuật giải........................................................................... 23 2.4.2. Tính dúng đắn của thuật giải........................................................... 27 2.4.3. Tính đầy đủ cùa thuật giải............................................................... 27 2.4.4. Cây SLD (SLD-tree)......................................................................... 28 2.5. Lập trình logic và các lĩnh vực liên quan.............................................. 30 2.5.1. Hệ chuyên gia (Expert System - ES).............................................. 30 2.5.2. Cơ sờ dừ liệu (CSDL) suy diễn (deductive database)...................33 Chương 3. Ngôn ngừ Prolog.............................................................................. 36 2 3.1. Các khái niệm cơ bàn............................................................................... 36 3.1.1. Hạng thức (Term)..............................................................................36 3.1.2. Câu Hom ............................................................................................38 3.1.3. Phép toán............................................................................................39 3.1.4. Danh sách...........................................................................................40 3.1.5. Đệ quy................................................................................................42 3.1.6. Chưtmg trình Prolog......................................................................... 42 3.2. Chứng minh cùa Prolog........................................................................... 44 3.2.1. Phép hợp nhất.................................................................................... 45 3.2.2. Cây tìm kiếm..................................................................................... 45 Chương 4. Lập trinh logic modal (Modal logic programming)......................49 4.1. Tổng quan về lập trình logic modal........................................................ 49 4.2. Khung làm việc của lập trình logic modal............................................ 50 4.2.1. Logic modal cấp một........................................................................ 50 4.2.2. Ngôn ngừ MProlog............................................................................ 51 4.2.3. Mô hình và khung làm việc (Model & frame)...............................53 4.2.4. Điểm bất động................................................................................... 59 4.2.5. Thuật giải SL D ..................................................................................60 4.3. Ví dụ áp dụng............................................................................................61 4.4. Kết luận về lập trình logic modal........................................................... 64 Kết luận.................................................................................................................. 65 Phụ lục................................................................................................................... 66 Tài liệu tham khảo................................................................................................75 3 M ở đầu Lịch sử ỉập trình logic được bắt đầu từ logic ký hiệu (symbolic logic). Sau đó, logic vị từ cấp một ra dời trên cơ sờ loeic ký hiệu và là một nhánh nghiên cứu của logic ký hiệu. Logic vị từ cấp một đã trở thành nền tảng của lập trình logic và có những bước phát triển mạnh trong thế kỷ 20. Theo Salah al-Fadhli [13] cỏ thể chia lịch sử cùa lập trình logic thành ba giai đoạn: Giai đoạn thứ nhất là việc tìm ra ngôn ngừ ký hiệu cùa logic. Người có ảnh hưởng lớn nhất trong giai đoạn này là Aristotle, ông là người đầu tiên đưa ra phương pháp suy diễn thành công “tam đoạn luận”. Sau này, các học trò của Aristotle đã phát triển phương pháp suy diễn này thành các luật suy diễn. Giai đoạn thứ hai là giai đoạn phát triển thực sự của logic ký hiệu và giai đoạn thứ ba là giai đoạn đưa logic ký hiệu vào lập trình logic. Điểm bắt đầu cùa lập trình logic là thuật giải tuyến tính của Robinson (trong những năm 1960) và các nghiên cứu cùa các tác già Kowalski, Colmerauer (trong những năm 1970) [3). Thuật giải cùa Robinson dùng để suy diễn trong chứng minh định lý tự động. Trong khi đó, Kowalski đã công thức hóa các thể hiện dạng thủ tục (câu lệnh chương trinh) của câu logic Hom và cho rằng câu “A nếu B ị và B2 và ... Bn” có thể đọc là: '‘để thực thi A, cản thực thi B ị và thực thi B2 và ... thực thỉ Bn”. Colmerauer đặc tả bộ chứng minh định lý tự động sử dụng các câu chương trình. Đó chính là cơ sờ đầu tiên cho khẳng định logic có thể được sử dụng như một ngôn ngữ lập trình. Logic cung cấp một ngữ nghĩa hình thức đơn giản và ngôn ngữ giải quyết vấn đề đa năng cho các lĩnh vực thuộc ngành khoa học máy tính đồng thời nó cũng là cơ sở cho các hệ cơ sở dừ liệu suy diễn, hệ chuvên gia [3]. Như vậy, suy luận logic là phương pháp nhận thức đã được biết đến từ rất sớm (thời Aristotle thế kỷ thứ 4 trước Công Nguyên) và cho đến những năm 70 của thế kỷ 20 lập trình logic (logic programming) mới được hình thành trên cơ sở của các thuật giải áp dụng trong chứng minh định lý tự động. Ban đầu, lập trình logic được xem như một bộ phận trong nghiên cứu về trí tuệ nhân tạo. Và sau này với nhiều nồ lực của các nehiên cứu (trên cả lý thuyết và thực hành), phạm vi ứng dụng cùa lập trình loaic đã rộng lớn, hiệu quả hơn. Lập trình logic đã được tách ra nghiên cứu độc lập trong ngành khoa học máy tính. 4 Lập trình logic ngày nay đã được ứns dụng trong nhiêu lĩnh vực của ngành khoa học máy tính như: trí tuệ nhân tạo. xử lý ngôn ngữ tự nhiên, hệ thong đa tác tử (multiagent), hệ thống tác tử thông minh, hệ chuyên gia, máy học, hệ hỗ trợ quyết định,... Với khả năng và phạm vi ứng dụng trong hầu hết các lĩnh vực thuộc nghành khoa học máy tính, lập trình logic đã và sẽ có nhữne bước phát triển vững chắc. Bởi vậy, nahiên cứu về lập trình logic và một số hướng phát triển của nó là điều mà người viết rất quan tâm. Nội dung trình bày của luận vãn bao gồm: tổng quan về lập trình logic; hệ thống các nguyên lý cơ sờ, quan trọng nhất trong lập trình logic; giới thiệu về Prolog - ngôn ngừ dùng trong lập trình logic thông qua các chương trình Prolog minh họa. Phần cuối của tài liệu trình bày về một hướng tiếp cận hiện đại cùa lập trình logic đó là lập trình logic modal. Chi tiết nội dung trình bày như sau: Chương 1 : Giới thiệu về lập trình logic, khái quát về hướng nghiên cứu này ở trong và ngoài nước, các hướng mở rộng của lập trình logic. Chưong 2: Hệ thống các nguyên iý cơ sở trong lập trinh logic. Đó ỉà lý thuyết các mô hình; lý thuyết điểm bất động; thuật giải SLD (Linear resolution with Selection function for Definite clause). Chương 3: Trình bày về ngôn ngữ Prolog trong mối quan hệ với lập trinh logic. Chương 4: Giới thiệu về lập trinh logic modal (dạng thức) (modal logic programming) - một mở rộng của lập trình logic cổ điển với việc thêm vào các toán tử modal (modal operator). Phần kết luận trình bày các nội dung mà đề tài đã làm được và đưa ra hướng phát triển trong tương lai của đề tài. Phần phụ lục trình bày các toán tử và một số chương trinh Prolog minh họa đà được kiểm thừ. 5 C hư ơng 1. Tổng quan về lập trình logic 1.1. Giới thiệu về lập trình logic Lập trình logic đã được nghiên cứu từ những năm đầu cùa thập kỷ 70 thế kỷ 20 và được xem như có nguồn gốc tự nhiên từ việc nghiên cứu chứng minh định lý tự động và trí tuệ nhân tạo [3]. Năm 1972, Kowalski và Colmerauer đã đưa ra ý tường nền tảng cho rằng logic có thể được sử dụng như một ngôn ngữ lập trình. Theo Kowalski thuật toán của lập trình gồm hai phần riêng biệt: phần logic và phần điều khiển. Phần logic là câu lệnh (phát biểu) chi ra vấn đề cần giải quyết; phần điều khiển là câu lệnh chi ra phải giải quvết vấn đề như thế nào. Trong lập trình truyền thống, người lập trình phải định nghĩa các thao tác cần thực hiện để giải bài toán. Nghĩa ỉà, phải chi ra cho máy tính biết cách thức giải quyết vấn đề như thế nào. đó là cách tiếp cận thủ tục (procedural). Các giả thiết thường là ẩn (không được viết trong chương trình). Đối với lập trình logic, người la xây dựng chương trình bàng cách mô tả lĩnh vực ứng dụng của nó. Nghĩa là đưa ra những khẳng định đúng, đó là cách tiếp cận khai bảo (declarative). Các già thiết là hiện còn việc chọn lựa thao tác là ẩn. Nếu theo quan điểm của Kowalski thì người lập trình cần phải khai báo phần logic của chương trình còn phần điều khiển hệ thống sẽ tự cung cấp - đó chính là thủ tục suy diễn độc lập với ứng dụng. Bằng cách tiếp cận khai báo, lập trình logic đă giải quyết tổt nhiều vấn đề có bản chất suy luận logic như hệ chuyên gia, hệ thống suy luận dựa trên mẫu đã có, hệ hỗ trợ quyết định, trí tuệ nhân tạo... và hỗ trợ hiệu quà dưới dạng module cho các bài toán khác. Trong lập trình logic, các vấn đề được đặt ra là: biểu diễn tri thức (bằng logic, khung tri thức - frame, mạng ngữ nghĩa - semantic network); xây dựng cơ sở tri thức:; xây dựng thủ tục suy diễn (thủ tục suy diễn phải độc lập với cơ sở tri thức). Một hệ lập trình logic về cơ bản gồm các thành phần: + Bộ phận giao tiếp với ngirời dùng: thu nhận câu hòi của người dùng và chuyển câu hỏi này cho thù tục suy diễn. + Thủ tục suy diễn: suy diễn ra các kết luận cho câu hòi dựa trên các sự kiện và luật đã được định nghĩa trong cơ sở tri thức. 6 + Cơ sở tri thức: bao gồm các sự kiện và các luật mô tả micn ứng dụng. Trune tâm của một hệ lập trình logic là thù tục suy diễn độc lập ứng dụng. Nó phải được định nghĩa và cài đặt dùng chuna cho mọi chương trình logic. Trong các hệ lập trình logic hiện nav, thủ tục suy diễn chủ yếu dựa trên thuật giải SLD. Thủ tục suy diễn được dùng bởi một chươne trình logic là độc lập ứng dụng. Do đó, việc triển khai một chương trinh chính là việc biểu diễn tri thức và triển khai nột cơ sở tri thức thích hợp với miền ứng dụng. Cách biểu diễn tri thức thông thường nhất là sử dụng các câu Horn. Việc mô tà lĩnh vực ứng dụng là mô tả các đối tượng và mối quan hệ giữa chúng được giả định tồn tại trong miền bài toán. Bài toán quan trọne, nhất của ỉập trình logic là: cho một chương trình logic p, một câu G vấn đề đặt ra là xét xem G có suy diễn được từ p hay không? Để giải bài toán đó, về lý thuyết có hai cách tiếp cận là mô hình Herbrand nhò nhất và điêm bất động nhò nhất của ánh xạ T từ tập các thể hiện Herbrand vào tập các thể hiện Herbrand. Cà hai cách trên đều có chung một mục đích là tìm ra mô hình Herbrand nhỏ nhất của p và nếu G có thể được suy diễn từ p thì G phải thuộc mô hình Herbrand nhỏ nhất của p. Tuy nhiên, các phương pháp để đạt được mục đích chung đó là khác nhau. Với cách tiếp cận xây dựng mô hình Herbrand nhò nhất vấn đề tập trung là các sự kiện nền, các luật trong p và các phép thế biến. Trong khi đó cách tiếp cận điểm bất động lại tập trung vào các mô hình và điểm bất động nhỏ nhất cùa ánh xạ T chính là mô hình Herbrend nhò nhất của p. Trong thực hành suy diễn để tìm lời giải cho bài toán trên, một thủ tục suy diễn lùi đã được xây dựng trên cơ sở của thuật giải SLD. Thuật giải SLD tìm ra các câu trả lời đúng cho bài toán dựa trên các câu đích và các biến. Các câu trả lời đúng ở đây cũng phải thuộc mô hình Herbrand nhỏ nhất của p. 1.2. Lập trình logic - c á c nội dung đang đ ư ợc nghiên cứu Trên thế giới, lập trình logic đã và đang thu hút nhiều nghiên cứu của các nhà khoa học bởi tính hiệu quả và phạm vi áp dụng rộng lớn của nó. Lập trình logic cổ điển (classical logic programming) đã mang lại nhiều thành tựu quan trọng và khảng định vị trí độc lập cùa lập trình logic trong ngành khoa học máy tính. Trong lập trình logic cổ điển, một chươns trình logic được định nghĩa là tập hữu hạn các câu Horn (câu có dạng: A<- Bị, Bn; n > 0. Trong đó, A, Bj, j = 1, 2, n là các công thức nguyên tố. A có thể ià rỗng). Dể chứng minh một câu G có được suy diễn từ chương trình p hay không về lý thuyết cần phải chứng minh G có là hệ quả logic của p hay không, và trone thực hành điều đó được thực hiện bằng phép hợp nhất và phép thế. Đó là những nguyên tấc cơ bản của lập trình logic cổ điển. Dựa trên nguyên tắc này, việc xây dựng mô tơ suy diễn đã bớt phức tạp và hiệu quả hơn (thuật giải SLD là đúng đắn và đầy đù). Bời lẽ, nếu câu chương trình có phần đầu không chứa đúng một nguyên tố như câu Hom thì vấn đề sẽ trờ nên phức tạp. Lập trình logic cổ điển đã có những bước phát triển và khả năng ứng dụng đáng kể, tuy nhiên, còn chưa hoàn thiện: các phương pháp suy diễn chưa thích đáng, chưa rút ra được kết luận từ dừ liệu không đầy đủ. Chính những thành công và giới hạn của lập trình logic cổ điển đã thúc đẩy việc phát triển các hướng mở rộng nhàm gia tăng khả năng và phạm vi ứng dụng cùa lập trình logic. Logic vị từ nguyên thủy không đủ khả năng để biểu diễn các kháiniệm thời gian, khả năng (độ tin cậy, tri thúc, ...)• Do đó, lập trình logic modal (modal logic programming) là một mở rộng cùa lập trình logic cổ điển với việc thêm vào các phép toán modal (modal operator) đề biểu diễn các tri thức phụ thuộc thời gian, không gian, một cách tổng quát là phụ thuộc ngữ cảnh. Lập trình logic temporal dựa trên yếu tổ thời gian, có thể xem là trường hợp riêng cùa lập trình logic modal. Lập trình logic modal đã được sử dụng hiệu quả trong việc biểu diễn tri thức, suy diễn, lập kế hoạch theo thời gian, mô phỏng, xác nhận dựa trên thời gian vàquantrọng hơn cả ỉà mô tả các hệ thống tác tử (agent). Lập trình logic dạng tuyến (Disjunctive Logic Programming - DLP) là một mở rộng cùa lập trình logic cổ điển với các yếu tố bất định ở phần đầu (head) của câu chương trình. Câu chương trình DLP có dạng: H| V H2 ... V Hm<- B| A B 2 ... Bn được gọi là lệnh tuyển (disjunctive rule). Với DLP, nhiều vấn đề thực tế đã được biểu diễn tốt hơn dưới dạng câu không phải câu Horn (non - Hom clause). Lập trình logic ràng buộc (Constraint Logic Programming - CLP) là sự kết hợp tự nhiên giữa lập trình ỉogic và ràng buộc trên ý tưởng nền tảng chung là tiếp cận khai báo. Câu chương trình CLP là câu có dạng Ao <- Cị, m > 0; C|, c m, Bi, Bn (n, c mlà các ràng buộc). Các ràng buộc được thêm vào phần thân (body) của câu chương trình. Lập trình logic ràng buộc tạo ra môi trường khai báo thuận lợi 8 trone việc giải quyết vấn đề bằng các phương tiện cùa ràng buộc và tỏ ra thích hợp với các ứng dụng lập kế hoạch, thời khóa biểu (vấn đề khó của lập lịch đã được giải quyết bằng cách sử dụng CLP trong nhĩme, miền hữu hạn), thiết kế hệ chuyên gia, xử lý ngôn ngữ tự nhiên... Tuy nhiên, hầu hết các bài toán trong lĩnh vực này là thuộc lớp NP - khó, nên hiệu quả của các chương trinh ràng buộc chưa thể dự đoán được mà dựa trên trực giác là một yếu tố quan trọng trong việc quyết định khi nào và cách thức sử dụng ràng buộc. Với một chương trình logic, khi tỉm lời giải cho câu hòi, hệ thống áp dụng chiến lược quay lui trên cây SLD để đảm bảo vét cạn tất cả các nhánh có thể. Việc duyệt cây có thể được thi hành song song (thường được gọi là OR-parallelism) và mọi cố gắng duvệt cây tìm lời giải cho một đích con phải dừng lại ngay khi nó hợp nhất được với đầu cùa một câu bất kỳ. Đó là ý tưởng của toán tử ủy thác (commit operator). Phép toán này chia thân câu chương trình thành hai phần: phần có gác (guarded part) và phần thân (bodv part). Có thể xem toán tử ủy thác như một nhát cắt. Khi một đích con đã có lời giải (ờ một nhánh nào đó của cây), nhát cẳt sẽ cắt bỏ (không tiếp tục duyệt) tất cả các nhánh khác của cây có gốc là đích con đó. Đó là những ý tưởng cơ bàn cho một lóp ngôn ngữ lập trình dựa trên lập trình logic và được gọi là ngôn ngữ lập trình logic tương tranh (concurrent logic programming language). Một câu chương trình ở đây là một câu có gác (guarded clause). Câu chương trình có dạng H <- G|, GmI B], Bn. Trong đó, n , m >0; G|, Gmlà các gác; I là ký hiệu phân tách phần gác và phần thân câu và được gọi là toán tử ủy thác (commit operator). Chương trình là một tập hữu hạn các câu có gác. Mỗi câu chương trình phải chứa chính xác một toán tử ủy thác. Toán tử này chia vế phải của câu chương trình thành hai phần, được giải quyết theo một trật tự nhất định. Phần gác được thi hành trước, sau đó là phần thân. Do đó, các literal trong các phần này có thể được thi hành một cách song song. Vậy nên, một đích không thể có nhiều hơn một lời giải và đó cũng là nhược điểm chính của lớp ngôn ngữ lập trình này. Lập trình logic tương tranh thích hợp với các hệ thống song song và phân tán. Như vậy, có thể thấy các hướng mở rộng dù theo cách tiếp cận nào cũng đều tập trung vào việc mở rộng phần tử cơ bản xây dựng chương trình logic đó là câu Hom. Mồi cách mở rộng đều có cơ sở, phạm vi áp dụng và khiếm khuyết riêng nhưng tất cả đã góp phần quan trọng vào việc đưa lập trình logic đến gần với các úma dụng thực tể hơn. 9 Hiện tại, trên thế giới các nghiên cứu tập trung nhiều vào lập trình logic ràng buộc; lập trình tập lời giải (answer set programming) và các kiểu khác (alternative paradigms). 1.3. Lập trình logic trong tương lai Vấn đề đặt ra trong tương lai của lập trình logic là xây dựng các trình biên dịch, thông dịch suy diễn hiệu quả hơn với sự hỗ trợ tiến bộ của nền tảng phần cứng. Trình dịch trong quá trình họp nhất có thể lựa chọn các luật một cách thông minh dựa trên chiến lược heuristic hay điều khiển của người dùng. Các trình dịch hiện nay chi chù yếu dựa trên thuật giải SLD tìm kiếm theo chiều sâu và cách lựa chọn luật là theo thứ tự khai báo nên trong một số trường hợp bài toán thực tế là có lời eiải nhưng chương trình lại không tìm được vi sa vào nhánh vô hạn đầu tiên trên cây tim kiếm (trong khi đó lời giải ờ nhánh khác của cây). Từ những nội dung đang được quan tâm nehiên cứu và phạm vi ứng dụng của ỉập trình logic, chúng tôi nhận thấy trong tương lai: + Lập trình logic cổ điển giữ vai trò trung tâm cho các nghiên cứu mở rộng. + Các hướng mở rộng tiếp tục được nghiên cứu hoàn thiện và ứng dụng, đặc biệt là lập trình logic ràng buộc cho lập lịch công nghiệp và lập trình logic modal trong việc xây dựng hệ thống đa tác tử và hệ thống các tác từ thông minh. Lập trình logic sẽ không thay thế hoàn toàn các phương pháp lập trình truyền thổng. Tuy nhiên, lập trình logic sẽ trở thành phương pháp lập trình cùa thế kỷ 21 bởi tính ưu việt và phạm vi ứng dụng của nó. 10 t Chương 2. Các nguyên lý c ơ s ở Trong lập trình logic, ngữ nehĩa mô hình, neừ nghĩa điểm bất động và thuật giải SLD là những nền tảng cơ bản. quan trọng nhất. Phần này sẽ trình bày một cách cô đọng tất cà các nền tảng đó. 2.1. Chương trình logic 2.1.1. Câu logic Định nghĩa: (Câu logic (clause) [3]) Một cảu là một công (hức có dạng: V x,... Vxs (Lị Trong đó: Moi Lj là một V . . . V L m. Literal đã được định Ví dụ: V... literal và X|, ... x s là cá c biến xuất hiện irong L| nghĩa trong [3]. công thức Vx Vy (p(x, y) V -q(x )) L à m ột câu vì X, y là các biến xuất hiện trong V í dụ: vLJ công thức (p(x, yjV -iq(x)) \/x Vy (p(x, y) V -q(x ) V r(z)V r(a) ) với a là một hằng , là một câu. Ví d ụ : công thức Vx Vy (p(x, y) V -q{x ) V r(z)) ichông là m ột câu logic vì c á c biển X, y xuất hiện trong (p(x, y ) V - q ( x ) V r(z ). Tuy nhiên, bien z có một xuất hiện tự do trong (p(X, v) V -q (x ) V r(z). Do các câu rất phổ biển trong lập trình logic nên để thuận tiện chúng ta ký hiệu câu sau đây: VX|... V x s (A| V ... V Ak V -iB| V ...V - i B n) T rone đó: A ị, A k, B|, B n là các nguyên tổ và X(, . . . x s là các biến xuất hiện trong các nguyên tổ đó. bằng: A|, .... Ak <—B], Bn Như vậy, trong ký hiệu câu, mọi biến đều được già định là có lượng từ phổ dụng, các dấu phẩy ở vế phải ký hiệu phép hội, các dấu phẩy ờ vế trái ký hiệu phép tuyển. 2.1.2. Câu chương trinh Đ ị n h n g h ĩa : ( C â u c h ư ơ n g t r ìn h ( p r o g r a m c la u s e ) h a y c â u H o m [3 ]) Một câu chương trình là một câu có dạng: A<—Bi, Bn (n > 0) Trong câu chương trình chỉ có đúng một nguyên tố (là A). A được gọi là đầu (head) và B j, B n được gọi ià thân {body) của câu chương trình. Ví dụ: câu parent (X, Y, Z) <—father (X, Z), mother (Y, Z). (với X, Y, z là các biến) là một câu chương trình. Ý nghĩa của câu này là “nếu X là cha của z và Y là mẹ của z thì X và Y là cha mẹ của Z”. Dạng công thức logic cùa công thức trên được biểu diễn như sau: vx, VY, vz ( parent(X, Y, Z) v-father(X, Z) v^mother(Y, Z)) Ví dụ: câu parent (X, Y, Z), wife (Y, X) <—father (X, Z), mother (Y, Z). (với X, Y, z là các biến) không phải là một câu chương trình vì phần đầu có hai nguyên tố parent(X, Y, Z) và wife(Y, X) Nếu n = 0 câu chương trinh trở thành A<- và được gọi là câu đơn vị (unit clause). Ví dụ: câu male(ann) 0 câu chương trình trở thành: <—Bị, Bn và được gọi là câu đích (goal clause). Mồi Bj (i = 1, ...n) được gọi là một đích con của câu đích. Nếu y], yrlà các biến của câu đích <- B 1s . . Bnthì ký hiệu dạng câu đó là dạng ngắn gọn của: V y i, Hay: V y r (- .B ï V ... V -nBn) - > 3 y i , 3 y r (Bj A ... A B n) Ví dụ: câu < -parent(mai, long, Ai), (mai, long là hàng, Ai là biến) là một câu đích. Ỷ nghĩa của công thức này là “mai và long là cha mẹ của Ai ?” 12 Biểu diễn câu đích này dưới dạng công thức logic ta có: - 73Ai parentịmai, long, Ai) hay VAi-iparent(mai, long, Ai). Ví dụ: câu <— parent(mai, long, lan), (các tham số đều là hằng) là một câu đích với V nghĩa là ”eó phải mai và long là cha mẹ của lan không?”. 2.1.3. Chương trình logic Định nghĩa: (Chương trình logic (logic program) [3]) Một chương trình logic là một tập hữu hạn các câu chương trình. Ví dụ: Chương trình gồm các câu sau: min(A, B, C) <- A >= B, c = B. min(A, B, C) <- A < B, c = A. Là một chương trình logic. Chương trình này sẽ tìm ra số nhỏ nhất trong 2 số A và B, kết quả đặt trong biến c. Để chạy chương trình, ta phải nạp đoạn mã trên vào máy tính theo cú pháp của một trình dịch nào đó hỗ trợ lập trình logic (chẳng hạn là Prolog). Sau đó, ta đưa vào một đích. Ví dụ để tìm số nhỏ nhất trong 2 số 100 và200ta đưavào đích <- min(10Q, 200, C). Kết quả ta sẽ nhận được c ~ 100 làsố nhỏnhấttrong hai số đó. 2.2. Hệ quả logic và c á c mô hỉnh Để xét tính đúng, sai của một công thức, đầu tiên ta cần phải gán ý nghĩa cho mỗi ký hiệu trong công thức đó. Các phép liên kết logic và các lượng từ đều có ý nghĩa cố định, nhưng các hằng, ký hiệu hàm, ký hiệu vị từ thì có ý nghĩa thay đổi với từng miền thể hiện của chúng. Một thể hiện đơn giản bao gồm một miền nào đó, mà trên miền này: + Xác định phạm vi của các biến, + Phép gán mỗi hằng là một phần tử của miền, + Phép gán mỗi ký hiệu hàm là một ánh xạ trên miền + Và phép gán mỗi ký hiệu vị từ là một quan hệ trên miền. 13 Do vậy, một thể hiện chi rõ ý nehĩa cho mồi kv hiệu trong công thức. Chúng ta đặc biệt quan tâm đến các thể hiện mà ờ đó cône thức nhận giá trị logic “true”. Thể hiện như vậy được gọi ỉà mô hình của công thức. Định nghĩa: (Thể hiện (interpretation) [3]) M ột th ể h iện ỉ (in terpretation ) cù a m ột n gôn ngữ c ấ p m ột L h a o g ồm : + Một tập khác rỗng D, gọi là miền thế hiện. + Với mỗi hằng trong L, gán một phần tử trong D. + Với mối hàm n - ngôi trong L, gán một ánh xạ từ ữ' vào D. + Với mỗi vị từ n - ngôi trong L, gán một ánh xạ từ ữ' vào tập (true, false} (hay tương đương một quan hệ trên ơ'). Ví du: « A B c Cho cấu trúc sẳp xếp như sau: Xét thể hiện I với các phép gán như sau: + Miền D íà tập các hộp A, B. c trong thế giới thực: D = {A, B, C} + Các hằng a, b, c gán tương ứng cho các hộp A, B, c. + Các quan hệ xác định như sau: ở trên đinh”, ở trên ở bên dưới ...” tương ứng với các vị từ: on_top/ỉ, above/2, below/2. Và các tân từ thuộc thể hiện I là: on_top(a), above(a, b), above(b, c), above(c), below(c, b), below(b, a). Công thức: VX3Y aboveịX, Y) Ý nghĩa không hình thức là “Với mọi cái hộp, luôn tồn tại một cải hộp khác để nó ở bên trên cái hộp khác đó ” Công thức trên là false (sai) trong thể hiện l (vì c không ờ trẽn bất kỳ hộp nào) Công thức: 3XVY -,above(X, Y) 14 í Ý nghĩa không hình thức của là: “Với mọi cái hộp, không phải lúc nào cũng tồn tại một cái hộp khác ở bên trên nó” Hay “Không phải với mọi cái hộp, luôn tồn tại một cái hộp khác để nỏ ở bên trên cái hộp khác đó ” Công thức trên là true (đúng) trong thế hiện ỉ (vì a không có cái hộp nào ở trên nó). Dựa trên định nghĩa côns thức và công thức đóng trong [3], chúng ta có: Định nghĩa: (Mô hình của một công thức (model for fomulas) [3]) Gọi Ị là một thể hiện của một ngôn ngữ cấp một L, giả sử F ỉà một công thức đóng của /. Khi đó, ỉ là mô hình cho F nếu giá trị chân lý của F đối với ỉ là đúng. Với tập các công thức đóng s, Ị ỉà mô hình cho s nếu nó ỉà mô hình cho mọi công thức trong s. Ví dụ: Xét công thức Vx3yp(x,y) và thể hiện I như sau: + Miền D là miền các số nguyên chẵn, không âm. x,y G D + p là quan hệ “chia hết cho”. Như vậy, I là mô hình cho p vì Vx3yp(x,y) luôn đúng đối với I. Phát biểu của công thức p trong I là: “với mọi số nguyên X e D, luôn tồn tại một số nguyên y e D để X chia hết cho y” . Sau đây là định nghĩa về tính thôa được và tính xác đáng của công thức dựa trên các mô hình. Định nghĩa: (Tính thỏa được, xác đáng, không thỏa được của công thức [3]) Gọi s là tập các công thức đóng của ngôn ngữ cắp một L. Ta nói + s ìà thỏa được (satisfaction) nếu L có một thể hiện là mô hình cho s. + s là xác đáng (validity) nếu mọi thể hiện của L đều là mô hình cho s. + s là không thỏa được nếu nó không có mô hình. 2.2.1. Hệ quả logic Định nghĩa: (Hệ quà logic (logical consequence) [3]) 15 Glà sir S là một tập các công thức đóng của một ngón ngừ cấp một L. Ta nói, F là hệ quà logic của s nếu với mọi thể hiện Ị cùa L, 1 là mô hình của s kéo theo I là mô hình cùa F. Ví dụ: Cho s = {p(a), Vxp(x) -» q(x)}. F = q(a). Gọi 1 ỉà một mô hình bất kỳ của S; a là một hằng thuộc miền thể hiện của I. Khi đó, ta có p(a) đúng với I và Vxp(x) -» q(x) đúng với I => q(a) đúng => I cũng là mô hình của F. Như vậy, F là hệ quà logic của s. Như vậv, với một chương trình p và một câu đích G = <- B|, Bn(n >0), ta cần chứng minh P u {G} là không thỏa được. Điều đỏ tương đương với việc chứna minh 3yJ ... 3 y m (B| A ...B n) (với y 1, y m là cá c biến xuất hiện trong B ), ..., Bn) là hệ quả logic của p. Như vậy, bài toán quan trọng là xác định tính không thỏa được (hay thỏa được) của p u {G}. Theo định nghĩa, ta phải chi ra mọi thế hiện của p u {G} khôngphài là mô hình. Đó là một điều dường như không thể!. Tuy nhiên, cỏ một lớp các thể hiện nhỏ hơn, thuận lợi hơn, đáp ứng đủ yêu cầu để khảo sát và chtmg minh tỉnh không thỏa được của p u {G}. Đó là các thê hiện Herbrand mà chúng ta sẽ khảo sát sau đây. 2.2.2. Mô hình Herbrand nhỏ nhất Từ các định nghĩa vũ trụ Herbrand, cơ sở Herbrand trong [3], chúng ta có: Định nghĩa: (Mô hình Herbrand của một tập các công thức [3]) Gọi L là một ngôn ngừ cấp một và s là một tập các công thức đóng của L. Một mô hình Herbrand cho s là một thể hiện Herbrand cho L đồng thời thể hiện Herbrand đó cũng là một mô hình cho s. Cơ sở Herbrand Bp của một chương trình hữu hạn p là mô hình Herbrand M của chương trình đó. Và mô hình Herbrand M của một chương trình hữu hạn p ỉà tập con của cơ sở Herbrand B[. của chương trình đó. Nghĩa là M c Bp. Vì mọi chương trình hừu hạn p đều có cơ sở Herbrand Bp cũng là một mô hình Herbrand (một chương trình có thể có nhiều mô hình Herbrand) nên tập tất cả các mô hình Herbrand cùa p là khác rỗng. Do vậy, giao cùa tất các mô hình Herbrand của p là một mô hình Herbrand [3] và được gọi là mô hình Herbrand nhỏ nhất của p, ký hiệu là Mp. 16 Các thể hiện Herbrand và mô hình Herbrand có hai thuộc tính quan trọng. Thứ nhất là tính thực tế, đó là đề xác định xem thể hiện Herbrand I có là mô hình Herbrand của công thức VxF hav không ta chỉ cần kiểm tra xem tất cả các kết thế nền của F có đúng trong I hay không. Ví dụ, để kiểm tra luật A <- A|, đúng trong I hay không, ta chỉ cần chi ra nếu (A <—A|, A <- A|, An và A[9, A29, An có An)0 là kết thế nền của An9 e ỉ thì A9 e I. Thứ hai là mặt lý thuyết, đối với một chương trình hữu hạn p, để xác định một công thức nguyên tổ A có là hệ quả logic cùa p hay không, ta chi cần kiểm tra xem mọi mô hình Herbrand của p có là mô hình của A hay không. Neu đúng thì A là hệ quả logic của p. Ví dụ: Cho một chương trình p gồm các cône thức sau: odd(s(0)). odd(s(s(X))) <- odd(X). Vũ trụ Herbrand của p bao gồm hằng 0 và hàm s. U|> = {0, s(0), s(s(0)), Cơ sờ Herband của p chứa vị từ odd của các hạng thức nền trong Up. Bp = {odd(0), odd(s(0)), odd(s(s(0))),...} Các thể hiện Herbrand của p là: 1, = { 0 }. I2 ={odd(s( 0))}. I3 = { odd(s(0)), odd(s(s(0)))} ỉ4 = {odd(s"(0)) I n e {1,3, 5, 7 ,...}} I5 = B p Các thể hiện Herbrand Ịà các tập con của cơ sở Herbrand. Il không phải là một mô hình của p vì nó không là mô hình Herbrand của odd(s(0)). Còn I2, 13, Ỉ4, Is là các mô hình của odd(s(0)) vì ođd(s(0)) e Ij (i = 2, 3, 4, 5). Tuy nhiên, I2 không phải là mô hình của p vì trong kết thế nền odd(s(s(s(0)))) <- odd(s(0)), phần giả thiết odđ(s(0)) e I2 nhưng kết luận odd(s(s(s(0)))) Ể I2 (phần kết luận sai trong I2). Tương tự, I3cũng không là mô hình của p. __________________ ! 0 '' I Mo c QL!Ỏc GIA I iRvJỉv>-> ÍA M T H O N G i!í'] ’ >•>■ ■ í - i c f n ì > : £ 17 I4 là mô hình của p vì odd(s(0)) e I4 và ta xét luật odd(s(s(t))) <- odd(t) là một kết thế nền bất kỳ cùa luật o d d (s(s(X ))) < - od d (X ) với t G Up. Rõ ràng ođd(s(s(t))) <- odd(t) đúng nếu odd(t) £ I4. Hơn thế nữa, nếu odd(t) e I4 thì ođd{s(s(t))) € I4 và do đó, odd(s(s(t))) <- odd(t) đúnẹ trong I4. Tương tự I5 cũng là mô hình cùa p. Như vậy, các thể hiện Herbrand I4,1 5 đồng thời là mô hỉnh Herbrand của p. Định lý: [10] Mô hình Herbrand nhỏ nhất (The least Herbrand model) Gọi p là một chương trình hữu hạn. Khi đó Mp = {A € Bp I A là hệ quả logic của P}. ở đây, Bp là cơ sở Herbrand của p. Chứng minh: Trước hết, cần chứng minh: Mp ID {A e Bp I p Ị= A}. Dễ thấy mọi nguyên tố nền A là hệ quà logic của p đều thuộc Mp. Thực vậy, theo định nghĩa hệ quả logic A phải đúng trong Mp. Mặt khác, theo định nghĩa về thể hiện Herbrand phát biểu rằng A đúng trong M|> khi và chi khi A € M[>. Tiếp theo, cần chứng minh Mp Ç {A € Bp Ị p 1=A}. Giả sử A e M|>. Do đó, A đúng trong mọi mô hình Herbrand của p. Giả sử 31’ là mô hình (không phải mô hình Herbrand) của p sao cho A sai trong r . Ta đã biết tập I gồm tất cà các công thức nguyên tố (các công thức này đúng trong I) là một mô hình Herbrand cùa p. Do đỏ, A không thể thuộc I. Điều này mâu thuẫn với aiả định rằne tồn tại một mô hình cùa p mà trong đó A sai. Do vậy, A đúng trong p, nghĩa là p 1= A. Như vậy, với một chương trình p, cơ sờ Herbrand của p là một mô hình Herbrand cùa p. Hơn nữa, luôn có một mô hình Herbranđ nhỏ nhất của p, đó là tập tất cả các nguyên tố nền là hệ quả logic của p. Ví dụ: Với chương trình p của ví dụ trên, mô hình Herbrand nhỏ nhất của p là I 4 vi 1 4 0 1 5 = I4. Để chứng minh một câu A là một hệ quả logic của P ( P u {-thì p u {G} thỏa được và do đó G là hệ quả logic của p. 2.2.3. Xây dựng mô hình Herbrand nhỏ nhát Có thể xem một chương trình hữu hạn là tập các sự kiện (fact) và các luật (rule). Tiếp cận theo điểm bất động nhò nhất ta có thể xây dựng mô hình Herbrand nhỏ nhất (một cách trực giác) như sau: + Tất cả các kết thế nền (ground instance) của các sự kiện phải thuộc mô hình Herbrand. Vì nếu một thể hiện Herbranđ 1 không chứa kết thế nền của một sự kiện A thì A không đúng trong I và như vậy ĩ không là một mô hình. + Xét luật A0 0) lấy bất kỳ kết thể nền nào (A0 <- Aj, An)9 cùa luật. Nếu I chứa A|0, ...A n0 thì nó phải chứa Ao0 để I là còn một mô hình. Ở đây 8 là một phép thế biến bất kỳ. Ví dụ: Xét chương trình p gồm các câu sau: p(f(x)) < - q(x, g(x)). q(a, g(b)). q(b,(g(b)). Ở đây: + a, b là các hăng, X là biến thuộc bảng chữ cái ngôn ngừ cấp một. + f(), g() là hàm, p(), q() là các vị từ thuộc ngôn ngữ cấp một. Ta xây dựng mô hình Herbrand nhỏ nhất cho chương trình trên như sau: + Các kết thế nền cùa các sự kiện là: q(a, g(b)), q(b,(g(b)) => Mp = {q(a, g(b)), q(b,(g(b))}. + Xét luật: p(f(x)) <- q(x, g(x)) -Dùng phép thế biến: 0 = {x/a}, ía cỏ: q(a, g(a)) Ể Mp nên p(f(a)) Ể Mp. -Dùng phép thế biến: 9 = {x/b}, ta có: q(b, g(b)) e Mị» nên p(f(b)) e Mp. Như vậy, mô hình Herbrand nhỏ nhất cho chương trình trên là: Mp = {q(a, g(b)), q(b,(g(b)), p(f(b))}. Ở đây, nếu ta bò đi bất kỳ phần tử nào trong Mpthì nó không còn là mô hình cho chương trình p nữa. 19 2.3. Điểm bất động Như đã đề cập, bài toán quan trọne nhất tron a lập trình logic là xác định tính không thỏa được cùa p u {G} (P là một chươne trinh logic và G là một đích). Với mô hình Herbrand nhỏ nhất, chúng ta đã có một cách tiếp cận cho lời giải bài toán. Đó là cách tiếp cận chù yếu dựa trên các sự kiện nền, các luật trong p và các phép thế biến. Điểm bất động là một cách tiếp cận khác để tìm lời giải cho bài toán trên, mục tiêu vẫn là tìm ra mô hình Herbrand nhỏ nhất nhưng cách tiếp cận này lại tập trung vào các mô hình và điểm bất động nhò nhất của ánh xạ liên kết với chương trình p. Trong phần này, chúng ta sẽ đề cập chủ yếu đến điểm bất động nhỏ nhất bởi có thể tìm ra lời giải cho bài toán “xác định tính không thỏa được của p u {G }” (G là một đích) thông qua điểm bất động nhò nhất. Trước hếl ta hãy xem xét các định nghĩa liên quan đến điểm bất động (íìxpoint) Định nghĩa: (Cận trên và cận dưới của tập hợp [l]) Cho S là một tập với thứ tự bộ phận < Khi đó, a e s là mộtcận trên của tập con X ç s nếu - Xem thêm -