Điểm bất động đối với chương trình logic diễn giải

Thông báo Khoa học và Công nghệ * Số 1-2015 114 ĐIỂM BẤT ĐỘNG ĐỐI VỚI CHƢƠNG TRÌNH LOGIC DIỄN GIẢI ThS. Trần Thái Sơn Trung Tâm Ngoại ngữ - Tin học, Trường Đại học Xây dựng Miền Trung Tóm tắt: Chương trình logic diễn giải và chương trình logic dạng tuyển đều là những mở rộng của chương trình logic. Bài báo này trình bày ngữ nghĩa điểm bất động đối với chương trình logic diễn giải. Đầu tiên, nghiên cứu ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương, trên cơ sở đó xây dựng các phép chuyển đổi chương trình logic, chương trình Horn diễn giải và chương trình logic diễn giải về chương trình logic dạng tuyển không chứa ký hiệu phủ định. Cuối cùng, xác định ngữ nghĩa điểm bất động thông qua chương trình được chuyển đổi. Từ khóa: Abductive Logic Programs; Logic Programming; Fixpoint Semantics; Disjunctive Logic Programs. 1. Ngữ nghĩa điểm bất động đối với chương trình logic dạng tuyển dương Định nghĩa 1.1 Một chương trình logic là một tập hữu hạn các mệnh đề có dạng sau: p ← q1  ...  qm  qm+1  ...  qn (1.1) hoặc ← q1  ...  qm  qm+1  ...  qn (1.2) trong đó n  m  0, p và qi là các nguyên tố. Trong mệnh đề (1.1), vế trái của ← được gọi là đầu mệnh đề và vế phải của ← được gọi là thân mệnh đề. Mỗi mệnh đề dạng (1.2) được gọi là một ràng buộc toàn vẹn, với ý nghĩa không thể tất cả q1,,qm là đúng và đồng thời tất cả qm+1,,qn là sai. Một ràng buộc toàn vẹn còn được gọi là một mệnh đề âm nếu nó không chứa ký hiệu phủ định (tức là m = n) Chương trình logic không chứa ký hiệu phủ định được gọi là chương trình Horn. Chương trình Horn không chứa ràng buộc toàn vẹn được gọi là chương trình logic xác định. Định nghĩa 1.2 Chương trình logic dạng tuyển dương P là tập hữu hạn các mệnh đề có dạng p1  pl  q1   qm (l, m  0) trong đó pi và qj là các nguyên tố. Thể hiện I thỏa mãn mệnh đề nền p1  pl  q1   qm nếu {q1,...,qm}  I kéo theo pi  I với mọi i ( 1 i  l ). I là mô hình cực tiểu của P nếu nó là thể hiện cực tiểu thỏa mãn tất cả các mệnh đề nền từ P. Định nghĩa 1.3 [8] Cho P là một chương trình logic dạng tuyển dương và I là một tập của các thể hiện. Ánh xạ TP: HBHB 22 2 2  được xác định như sau:  I I )()(   I IPP TT Trong đó ánh xạ TP: HB2HB 2 2  được xác định như sau: Thông báo Khoa học và Công nghệ * Số 1-2015 115 Ø, Nếu {q1,...,qm}  I đối với mệnh đề âm nền  q1  ...  qm của P; TP(I) = { J với mỗi mệnh đề nền Ci: ii m11 ...... qqpp l  của P sao cho },...,{ im1 qq  I và },...,{ il1 pp  I =  J = I   i }{ j C p )1( ilj  } Đặc biệt, TP() =  Theo định nghĩa này, nếu một thể hiện I không thỏa mãn một số mệnh đề âm nền thì TP(I) = . Ngược lại, nếu có một mệnh đề nền không âm Ci mà không thỏa mãn bởi I (tức là I thỏa mãn phần thân của Ci nhưng không thỏa mãn phần đầu Ci) thì I được mở rộng bằng cách bổ sung mỗi phần tuyển từ các phần đầu của mọi Ci. Định nghĩa 1.4 [8] Thứ tự lũy thừa của toán tử TP được xác định như sau. TP ↑ 0 = {}, TP ↑ n +1 = TP ↑ (TP ↑ n), TP ↑  =    n TP ↑ n trong đó n là thứ tự kế tiếp và  là thứ tự giới hạn. Ví dụ 2.1 Cho chương trình logic dạng tuyển dương P gồm các mệnh đề: p  q  r , s  r , r  ,  q  s , TP ↑  đạt được từ P như sau: TP ↑ 1 = {{r}}, TP ↑ 2 = {{r, s, p}, {r, s, q}}, TP ↑ 3 = {{r, s, p}} = TP ↑  Định lý 1.1 [8] Cho P là một chương trình logic dạng tuyển dương. Lúc đó: (a) TP ↑  là một điểm bất động của P. (b) Mỗi phần tử trong TP ↑  là một mô hình của P. (c) Gọi MMP là tập của tất cả các mô hình cực tiểu của P. MMP = min(TP ↑ ) trong đó min(I) = { I  I  J  I sao cho J  I } Chứng minh: (a) Khi I  TP ↑ , giả sử không có thể hiện J trong TP ↑  sao cho I  TP({J}). Trong trường hợp này với  bất kỳ, có n (  n  ) sao cho J không được bao hàm trong TP ↑ n. Lúc đó, I  TP ↑ n+1, mâu thuẫn với thực tế I  TP ↑ . Vì vậy J  TP ↑ , I  TP (TP ↑ ). Do đó I  TP↑n với bất kỳ +1  n   suy ra I  TP ↑ . (b) Với bất kỳ I  TP ↑ , I thỏa mãn mỗi mệnh đề nền âm từ P, với bất kỳ mệnh đề nền p1  ...  pl  q1  ...  qm từ P, {q1,,qm }  I kéo theo và Ai  I với mọi i ( Thông báo Khoa học và Công nghệ * Số 1-2015 116 1  i  l. Do đó, I là một mô hình của P. (c) Vì MMP  min(TP ↑ ) là hiển nhiên từ (b). Cho I là mô hình cực tiểu của P, với mỗi nguyên tố A trong I có một mệnh đề nền p1 ...  pl  q1  ...  qm từ P sao cho {q1,...,qm}  I và A = pi với mọi i ( 1  i  l ). Theo định nghĩa cấu trúc điểm bất động, I được chứa trong TP ↑ . Vì mỗi phần tử trong TP ↑  là một mô hình của P, I là một phần tử cực tiểu của TP ↑ . Do đó I  min(TP ↑ ). Theo định nghĩa, điểm bất động TP ↑  luôn luôn tồn tại đối với bất kỳ chương trình logic dạng tuyển dương P và được xác định duy nhất cho mỗi P. Điểm bất động này được gọi là điểm bất động tuyển chọn của P. Định lý 1.1 (c) mô tả cấu trúc điểm bất động của ngữ nghĩa mô hình cực tiểu đối với các chương trình logic dạng tuyển dương. 2. Ngữ nghĩa điểm bất động đối với chương trình logic Phần này nghiên cứu một phép chuyển đổi để chuyển đổi chương trình logic sang chương trình logic dạng tuyển không chứa ký hiệu phủ định. Ngữ nghĩa điểm bất động được xây dựng dựa trên chương trình logic đã được chuyển đổi. Định nghĩa 2.1 Cho P là một chương trình logic. PK là chương trình nhận được từ P như sau: 1. Mỗi mệnh đề dạng p  q1  ...  qm  ¬qm+1  ...  ¬qn được chuyển đổi thành mệnh đề dạng (p  Kqm+1  ...  Kqn)  Kqm+1 ...  Kqn  q1  ...  qm (2.1) trong P K . 2. Mỗi ràng buộc toàn vẹn được chuyển thành Kqm+1 ...  Kqn  q1  ...  qm 3. Mỗi nguyên tố B trong cơ sở Herbrand (HB), bổ sung vào PK mệnh đề dạng  KB  B (2.2) Trong đó, Kq (t.ư Kq) là một nguyên tố mới mà ký hiệu q là độ tin cậy (t.ư. không tin cậy) Trong phép chuyển đổi, mỗi nguyên tố ¬qi được viết lại Kqi và chuyển sang phần đầu của mệnh đề. Hơn nữa, vì phần đầu p trở thành true khi mỗi Kqi trong phần thân là true nên điều kiện Kqm+1 ... Kqn được thêm vào p. Ràng buộc toàn vẹn  Kq  q cho thấy rằng mỗi nguyên tố q cùng một thời điểm không thể là true và không tin cậy (Kq). Một thể hiện IK của chương trình chuyển đổi bây giờ được xác định như một tập con của cơ sở Herbrand mới HBK: HB K = HB  { Kq | q  HB }  { Kq | q  HB }. Định nghĩa 2.2 Một nguyên tố trong HBK được gọi là mục tiêu nếu nó là trong HB và tập các nguyên tố mục tiêu trong thể hiện IK được ký hiệu bằng obj(IK). Chú ý: Kq và Kq không xem như là công thức mới trong logic hình thức mà xem như các nguyên tố mới được đưa ra trong chương trình mới chuyển đổi. Ý nghĩa của Kq được cho bởi  Kq  q, trong đó Kq chấp nhận ràng buộc chính tắc sau. Thông báo Khoa học và Công nghệ * Số 1-2015 117 Định nghĩa 2.3 [8] Một thể hiện IK là chính tắc nếu nó thỏa mãn điều kiện: Đối với mỗi nguyên tố nền q nếu Kq  IK thì q  IK. Với IK là tập của các thể hiện. Ký hiệu objc(I K ) = { obj(I K ) IK IK và IK là chính tắc } Để sử dụng điểm bất động tuyển chọn đối với ngữ nghĩa của chương trình chuyển đổi, một chương trình mới giống như PK trong định nghĩa 2.1 cho phép một phép tuyển của các phép hội của các nguyên tố trong phần đầu một mệnh đề được xác định như sau. Một mệnh đề có thể được phân tách ra thành một tập của các mệnh đề có dạng p1   pl  q1   qm (l, m 0). Mệnh đề có dạng m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  (2.3) đặt cho k1×k2××kl chuyển đổi thành mệnh đề dạng m1,,2,1 ......21 qqppp lilii  (2.4) với mọi i1 = 1,,k1, i2 = 1,,k2, il = 1,...,kl. Một chương trình gồm các mệnh đề có dạng m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  cũng xem như là một chương trình logic dạng tuyển dương. Ánh xạ có thể được áp dụng cho các mệnh đề dạng m1,,2,1 ......21 qqppp lilii  Ánh xạ được sửa đổi để xử lý một phép tuyển của các phép hội về các nguyên tố trong phần đầu. Đối với một phép hội của các nguyên tố F = p1  ...  pk, ký hiệu tập các phép hội của nó là conj(F) = {p1,,pk}. Định nghĩa 2.4 [8] Cho P là một chương trình logic gồm các mệnh đề có dạng m1,1,,11,1 ...)...(...)...( 1 qqpppp lkllk  và I là một thể hiện. Ánh xạ TP : 2 HB  HB22 được xác định như sau: Ø, Nếu {q1,...,qm}  I đới với mệnh đề âm nền  q1  ...  qm của P; TP(I) = { J đối với mỗi mệnh đề nền Ci : ii m11 ...... qqFF l  từ P sao cho { im1 ,...,qq }  I và conj(Fj) I với j = 1,,li J = I   i )( j C Fconj (1  j  li) }. Định lý sau đây trình bày đặc trưng điểm bất động về ngữ nghĩa mô hình bền vững đối với các chương trình logic. Định lý 2.1 [8] Cho P là một chương trình logic, PK là chương trình chuyển đổi của P và STP là tập tất cả các mô hình bền vững của P. Lúc đó: a) STP = objc( KPT ). b) P không có mô hình bền vững nếu và chỉ nếu objc( KPT ) = . Ví dụ 2.1 Cho P là chương trình logic gồm các mệnh đề: p  ¬q, q  ¬p, Thông báo Khoa học và Công nghệ * Số 1-2015 118 r  q, r  ¬r, P K là chương trình chuyển đổi của P gồm các mệnh đề: P K = { ( p  Kq)  Kq  , q  Kp)  Kp  , r  q, ( r  Kr)  Kr  }  {  KB  B B  HB }. Toán tử KPT được xác định như sau: 0K PT = { } 1K PT = { { p, Kq, q, Kp, r, Kr}, { p, Kq, q, Kp, Kr}, { p, Kq, Kp, r, Kr}, { p, Kp, Kp, Kr}, { Kq, q, Kp, r, Kr}, {Kq, q, Kp, Kr}, {Kq, Kp, r, Kr}, { Kq, Kp, Kr} }, 2K PT = { {p,Kq, Kp,Kr }, { Kq, q,Kp, Kr, r } , { Kq, Kp, Kr} }, 3K PT = 2K PT = KPT . Trong KPT chỉ có phần tử thứ hai { Kq, q,Kp, Kr, r } là chính tắc. Vì vậy, objc( KPT ) = {{ q, r}}và {q, r} là mô hình bền vững duy nhất của P. 3. Ngữ nghĩa điểm bất động đối với chương trình Horn diễn giải Đối với chương trình Horn diễn giải, để áp dụng phép chuyển đổi theo định nghĩa 2.1, một giả thuyết về nguyên tố q được thiết lập để định giá công thức phủ định ¬q. Tính đúng đắn của giả thuyết âm Kq được kiểm tra thông qua ràng buộc toàn vẹn  Kq  q. Trong phép chuyển đổi của chương trình Horn diễn giải, mỗi vị từ diễn giải cũng có thể được coi như là một giả thuyết. Khác nhau duy nhất giữa các giả thuyết từ các vị từ diễn giải và giả thuyết từ công thức phủ định là giả thuyết dương Kr cho mỗi vị từ diễn giải r (rA) luôn luôn cần thỏa mãn ràng buộc chính tắc. Phép chuyển đổi của chương trình Horn diễn giải được định nghĩa như sau. Định nghĩa 3.1 Cho là một chương trình Horn diễn giải. K AP là chương trình nhận được từ như sau: 1. Mỗi mệnh đề dương trong P có dạng p  q1  ...  qm  r1  ...  rn (m, n  0) (3.1) (trong đó qi là các vị từ không diễn giải (qi A) và rj là các vị từ diễn giải (rjA)) được chuyển đổi thành mệnh đề dạng (p  r1   rn)  Kr1  ...  Krn  q1  ...  qm (3.2) trong K AP . 2. Mỗi ràng buộc toàn vẹn trong P được chuyển đổi thành Thông báo Khoa học và Công nghệ * Số 1-2015 119 Kr1 ...  Krn  q1  ...  qm 3. Mỗi vị từ diễn giải r trong A (rA) bổ sung vào K AP mệnh đề  Kr  r Ví dụ 3.1 Cho chương trình Horn diễn giải như sau: P = { p  q  a } A = {a} I = {a} là mô hình bền vững của Nhưng KAP = { ( p  a)  Ka  q,  Ka  a } là chương trình chuyển đổi của và K A T P = {}. Bổ đề 3.1 [8] Cho là một chương trình Horn diễn giải, O là một quan sát. Nếu E  A là một giải thích của O thì có một giải thích E‟ của O sao cho E‟  E và IE‟ = obj(I K) đối mọi IK  K A T P . Ví dụ 3.1 Cho chương trình Horn diễn giải như sau: P = { hắt_hơi(X)  người(X)  cảm_lạnh(X), hắt_hơi(X)  người(X)  nóng_sốt(X), người(Tom)  ,  người(X)  cảm_lạnh(X)  nóng_sốt(X) } A = { cảm_lạnh(X), nóng_sốt(X) } Chương trình Horn diễn giải được chuyển đổi thành chương trình logic dạng tuyển dương K AP gồm các mệnh đề sau: (cảm_lạnh(X)  hắt_hơi(X))  Kcảm_lạnh(X)  người (X), (nóng_sốt(X)  hắt_hơi(X))  Knóng_sốt(X)  người(X), người(Tom)  ,  Kcảm_lạnh(X)  Knóng_sốt(X)  người(X),  Kcảm_lạnh(X)  cảm_lạnh(X),  Knóng_sốt(X)  nóng_sốt(X) Cho O = hắt_hơi(Tom) là một quan sát. Lúc đó: K A T P = { M1, M2, M3 } Trong đó: M1 = { người(Tom), cảm_lạnh(Tom), hắt_hơi(Tom), Knóng_sốt(Tom)}, M2 = { người(Tom), Kcảm_lạnh(Tom), nóng_sốt(Tom), hắt_hơi(Tom) }, M3 = { người(Tom), Kcảm_lạng(Tom), Knóng_sốt(Tom) }. Vậy E1 = {cảm_lạnh(Tom)} và E2 = {nóng_sốt(Tom)} là hai giải thích cho quan sát O sau khi trích lọc các vị từ diễn giải từ M1 và M2. 4. Ngữ nghĩa điểm bất động đối với chương trình logic diễn giải Phần này trình bày một phép chuyển đổi của chương trình logic diễn giải bằng cách kết hợp hai phép chuyển đổi trong mục 2 và 3. Trong đó, mỗi nguyên tố âm ¬q đối với vị từ không diễn giải q (qA) được chuyển đổi theo cách chuyển đổi của Thông báo Khoa học và Công nghệ * Số 1-2015 120 chương trình logic nó được chia ra thành Kq và Kq. Mặt khác, khi một nguyên tố âm ¬r với r là một vị từ diễn giải (rA) xuất hiện bên trong mệnh đề chương trình thì ¬r được chia ra thành Kr và r. Định nghĩa 4.1 Cho là một chương trình logic diễn giải. K AP là chương trình nhận được từ như sau: 1. Mỗi mệnh đề dạng p  q1  ...  qm  ¬qm+1  ...  ¬qs  r1  ...  rn  ¬rn+1  ...  ¬rt (4.1) trong P, (trong đó s  m  0, t  n  0), qj là các vị từ không diễn giải (qj A) và rk là các vị từ diễn giải (rk A)) được chuyển đổi thành mệnh đề dạng (p  r1   rn  ¬Kqm+1   ¬Kqs  ¬Krn+1   ¬Krt)  ¬Kr1   ¬Krn  Kqm+1  Kqs  rn+1   rt ← q1  ...  qm (4.1) trong K AP . 2. Mỗi ràng buộc toàn vẹn trong P được chuyển thành Kr1  Krn  Kqm+1   Kqs  rn+1   rt  q1   qm 3. Mỗi nguyên tố H trong cơ sở Herbrand (HB) được bổ sung vào K AP mệnh đề có dạng  KH  H Chú ý: Chương trình chuyển đổi K AP trong định nghĩa này có thể rút gọn thành chương trình PK (tại mục 2) khi các nguyên tố diễn giải A là rỗng và có thể rút gọn thành chương trình K AP khi P là một chương trình Horn. Định nghĩa 4.2 Cho IK là một tập của các thể hiện, ký hiệu minA(I K) được xác định như sau: minA (I K ) = {IE  I K  JF  I K sao cho F  E} Định lý 4.1 [8] Cho là một chương trình logic diễn giải. Lúc đó: (a) Gọi min-BM là tập của tất cả các mô hình bền vững cực tiểu của , min-BM = minA(objc( K A T P )). (b) Cho E là một tập con của A và O là một quan sát. E là giải thích cực tiểu của O đối với nếu và chỉ nếu IE  minA(objc( ))T K A}) {P(   O . Ví dụ 4.1 Cho chương trình logic diễn giải như sau: P = { p  r  b  ¬q q  a r   ¬p } A = {a, b} Chương trình K AP được chuyển đổi từ là: K AP = { ( p  b  Kq)  Kb  Kq  r, Thông báo Khoa học và Công nghệ * Số 1-2015 121 ( q  a)  Ka , r  , Kq  , }  {  KH  H | H  HB} Lúc đó: {r, p, b, Kq, Ka, Kp } là tập chính tắc duy nhất trong K AP T . Vì vậy, min-BM = {{ r, p, b }} 5. Kết luận Bài báo tập trung nghiên cứu một khuôn khổ đồng nhất cho việc mô tả điểm bất động của các chương trình logic dạng tuyển dương, chương trình Horn diễn giải và chương trình logic diễn giải. Dựa trên toán tử điểm bất động thông qua các tập của các thể hiện, ngữ nghĩa mô hình bền vững của chương trình logic diễn giải có thể được mô tả bởi điểm bất động của chương trình dạng tuyển dương được chuyển đổi phù hợp. So với các cách tiếp cận khác, lý thuyết điểm bất động ở đây cung cấp một cách thức lập luận để đưa ra các giải thích cho các quan sát từ chương trình logic diễn giải. TÀI LIỆU THAM KHẢO [1] Võ Thị Ngọc Huệ. 2009. Nghiên cứu đặc trưng điểm bất động và các kỹ thuật định giá truy vấn đối với cơ sở dữ liệu suy diễn dạng tuyển, luận văn thạc sĩ khoa học Công nghệ thông tin, chuyên ngành Khoa học máy tính, Trường Đại Học Khoa Học Huế. [2] Trần Thái Sơn. 2010. Nghiên cứu ngữ nghĩa và phương pháp định giá truy vấn đối với chương trình logic diễn giải, luận văn thạc sĩ khoa học Công nghệ thông tin, chuyên ngành Khoa học máy tính, Trường Đại Học Khoa Học Huế. [3] Alferes. J, Pereira. L.M and Swift. T. 2003. “Abduction in Well-Founded Semantics and Generalized Stable Models via Tabled Dual Programs”, Under consideration for publication in Theory and Practice of Logic Programming, arXiv:cs/0312057v1 [cs.LO]. [4] Denecker. M and Schreye. D.De. 1997. “SLDNFA an abductive procedure for abductive logic programs”, Journal of Logic Programming 34(2), pp. 111-167. [5] Gelfond. M and Lifschitcz. V. 1988. “The Stable Semantics for Logic Programming”, In Logic Programming: proceeding of the 5th International Conference and Symposium, MIT Press, pp. 1070-1080. [6] Mancarella. P and Terreni. G. 2009. “The CIFF Proof Procedure for Abductive LogicProgramming with Constraints: Theory, Implementation and Experiments”, Under consideration for publication in Theory and Practice of Logic Programming, arXiv:0906.1182v1 [cs.AI]. [7] Sakama. C and Inoue. K. 1994. “On the equivalence between disjunctive and abductive logic Programs”, In Proceeding of the 11th International Conference on Logic Programming, (MIT Press, Cambridge), pp. 489 – 503. [8] Sakama. C and Inoue. K. 1996. “A Fixpoint characterization of Abductive Logic Programs”, Journal of logic Programming 27, pp. 107-136.