Logic bậc nhất và truy vấn giao

Bài trước: Siêu đồ thị phi chu trình và đồ thị dây cung.
Bài sau: bài toán định trị phép truy vấn giao.

Bài trước lược khảo các khái niệm và kết quả liên quan đến siêu đồ thị phi chu trình và đồ thị dây cung. Bài sau chúng ta sẽ dùng cái khái niệm và kết quả này để thảo luận thuật toán cổ điển của Yannakakis định trị các phép truy vấn giao (conjunctive queries). Mục tiêu của bài này là để giới thiệu các khái niệm của logic bậc nhất dùng để định nghĩa phép truy vấn giao. Ngoài ra, ta sẽ rảo qua một vài ứng dụng của truy vấn giao. Do đằng nào cũng nói về ngữ pháp và ngữ nghĩa của logic bậc nhất, ta cũng sẽ đi vòng và điểm qua vài kết quả cơ bản của logic bậc nhất. Lưu ý rằng một số sách viết về logic trong khoa học máy tính dùng “ngôn ngữ” và “diễn dịch” thay vì “từ vựng” và “cấu trúc” như ta dùng ở đây, theo thuật ngữ của logic học cổ điển.

1. Logic bậc nhất

Trước hết, ta duyệt qua vài khái niệm cơ bản của logic bậc nhất (first order logic). Hiển nhiên trong một bài viết ngắn ta chỉ có thể cưỡi ngựa xem hoa và giới thiệu những khái niệm tuyệt đối cần. Bạn có thể tham khảo quyển A Mathematical Introduction to Logic, Second Edition, hoặc quyển sách cơ sở dữ liệu (miễn phí) của Serge Abiteboul, Richard Hull, và Victor Vianu. Ta sẽ bắt đầu bằng một bộ từ vựng, ngữ pháp kết nối các từ vựng lại thành các câu hoặc công thức, cách gán ngữ nghĩa cho cách từ, câu, và công thức.

1.1. Từ vựng và cấu trúc

Một bộ từ vựng (vocabulary) là một tập hữu hạn không rỗng, bao gồm các ký hiệu quan hệ (relation symbols hoặc predicate symbols) và các ký hiệu hằng số. Ta sẽ dùng chữ in cho các ký hiệu quan hệ, như ${R, S, P, Q, \dots}$ , và chữ thường cho các ký hiệu hằng số, như ${a,b,c, d, \dots}$ . Một bộ từ vựng không có ký hiệu hằng số thì gọi là bộ từ vựng quan hệ (relational vocabulary). Mỗi ký hiệu quan hệ có một bậc (arity) là một số nguyên dương. Ta sẽ thường dùng ${\tau, \sigma}$ để chỉ các bộ từ vựng.

Một bộ từ vựng chứa các ký hiệu để mô tả một nội dung nào đó. Để thật sự có nội dung thì ta cần phần “dữ liệu” mà các ký hiệu này trỏ tới. Phần dữ liệu này chứa trong cái gọi là “cấu trúc” (structure) của một bộ từ vựng.

Một cấu trúc ${\mathcal A}$ của một bộ từ vựng ${\tau}$ (tiếng Anh gọi là ${\tau}$ -structure) bao gồm những thành tố sau đây: (1) một miền (domain hoặc universe) ${A}$ là một tập không rỗng, (2) một quan hệ ${R^{\mathcal A}}$ ${n}$ -chiều cho mỗi ký hiệu quan hệ ${n}$ -chiều ${R}$ của bộ từ vựng, and (3) một phần tử ${c^{\mathcal A} \in A}$ cho mỗi ký hiệu hằng số ${c}$ của bộ từ vựng. Nói cách khác, một cấu trúc là một phép gán các ký hiệu trong bộ từ vựng đến dữ liệu cụ thể. Một quan hệ ${n}$ -chiều chẳng qua là một bảng dữ liệu gồm ${n}$ cột, hoặc ta cũng hiểu một quan hệ ${n}$ -chiều là một tập hợp của một số vectors ${n}$ chiều nào đó. Ta thường viết ${R^{\mathcal A}a_1\dots a_n}$ thay vì viết ${a_1\dots a_n \in R^{\mathcal A}}$ .

Trong nhiều trường hợp người ta thêm vào các ký hiệu hàm (function symbols), đại diện cho các hàm từ ${A}$ vào ${A}$ ; tuy nhiên ta có thể mô hình hoá một hàm số dùng một quan hệ. Ngoài ra ta cũng có thể bỏ các hằng số và thay chúng bằng các quan hệ bậc nhất. Do mục tiêu của ta là giới thiệu phần ngôn ngữ bậc nhất để mô tả các truy cập vào cơ sở dữ liệu (CSDL), nên ta dùng một định nghĩa ngôn ngữ bậc nhất đơn giản để biểu thị các truy vấn vào CSDL.

Ví dụ 1 Xét bộ từ vựng ${\tau = \{E\}}$ , chỉ có một ký hiệu quan hệ ${E}$ bậc 2. Một cấu trúc ${\mathcal A = (V, E^{\mathcal A})}$ của bộ từ vựng này được gọi là một đồ thị đơn nếu nó thoả điều kiện: ${(u,v) \in E^{\mathcal A}}$ nếu và chỉ nếu ${(v,u) \in E^{\mathcal A}}$ , và ${(u,u) \notin E^{\mathcal A}}$ với mọi ${u,v \in V}$ . Ở đây, ${V}$ là miền của cấu trúc.

Ví dụ 2 Dễ thấy là một tập các quan hệ trong một shema của một CSDL quan hệ (relational database) là một cấu trúc của một bộ từ vựng bao gồm tên các quan hệ trong CSDL này.

1.2. Ngữ pháp (syntax) của logic bậc nhất

Trước hết hãy nói về phần ngữ pháp của logic bậc nhất. Xét một bộ từ vựng ${\tau}$ cho trước. Một công thức (formula) của logic bậc nhất là một chuỗi ký hiệu bao gồm các ký hiệu sau đây: các ký hiệu trong ${\tau}$ , một số đếm được (countable) các ký hiệu biến (như ${x,y,z,v_1,v_2,v_3,\dots}$ ), các ký hiệu kết nối logic (logical connectives) như ký hiệu phủ định ${\neg}$ , ký hiệu hoặc ${\vee}$ , phép lượng hoá tồn tại ${\exists}$ (existential quantifier), dấu bằng ${=}$ , và các dấu đóng mở ngoặc ${),(}$ .

Một hạng tử (term) là một biến hoặc một hằng số của ${\tau}$ . Một công thức của logic bậc nhất là một chuỗi ký hiệu như liệt kê ở trên được xây dựng một cách đệ quy bằng cách áp dụng một số hữu hạn lần các phép xây dựng cơ bản sau đây:

Nếu ${t_1}$ và ${t_2}$ là các hạng tử thì ${t_1 = t_2}$ là một công thức.
Nếu ${R}$ là một ký hiệu quan hệ ${n}$ -chiều và ${t_1,\dots,t_n}$ là ${n}$ hạng tử thì ${Rt_1\dots t_n}$ là một công thức. Các công thức dạng này và dạng ${t_1=t_2}$ ở trên được gọi là công thức nguyên tử (atomic formula, còn gọi là các atoms).
Nếu ${\varphi}$ là một công thức thì ${\neg \varphi}$ là một công thức.
Nếu ${\varphi}$ và ${\psi}$ là hai công thức thì ${(\varphi \vee \psi)}$ là một công thức.
Nếu ${\varphi}$ là một công thức và ${x}$ là một biến thì ${\exists x \varphi}$ là một công thức.

Lưu ý rằng ở trên ta không cần các ký hiệu với mọi ${\forall}$ , tương đương ${\leftrightarrow}$ , suy ra ${\rightarrow}$ , ký hiệu “và” ${\wedge}$ , tại vì ta có thể định nghĩa ${\leftrightarrow}$ , ${\rightarrow}$ , ${\forall}$ , hay ${\wedge}$ dùng ${\neg}$ và ${\exists}$ . Ví dụ như ${\forall x \varphi}$ thì tương đương với ${\neg \exists x \neg \varphi}$ .

Bài tập 1 Viết lại các công thức ${(\varphi \leftrightarrow \psi)}$ , ${(\varphi \rightarrow \psi)}$ , và ${(\varphi \wedge \psi)}$ mà chỉ dùng ${\neg}$ và ${\exists}$ .

Biến ${x}$ nằm ngay sau ${\forall}$ và ${\exists}$ là biến bị giới hạn (bounded variable) bởi phép lượng hoá phổ dụng (universal quantifier) hoặc phép lượng hoá tồn tại. Trong một công thức bậc nhất thì các biến không bị giới hạn được gọi là các biến tự do (free variables). Nếu một công thức ${\varphi}$ có ${n}$ biến ${x_1,\dots, x_n}$ (bị giới hạn hoặc tự do) thì ta thường ghi thêm ${\varphi(x_1,\cdots, x_n)}$ cho rõ. Còn ${\text{free}(\varphi)}$ dùng để chỉ tập các biến tự do của công thức ${\varphi}$ .

Một công thức không có biến tự do thì gọi là một câu (hiểu là một khẳng định, có thể đúng, có thể sai). Ví dụ, trong định nghĩa đồ thị đơn ở trên ta có thể dùng hai câu ${\forall x \neg Exx}$ và ${\forall x\forall y (Exy \rightarrow Eyx)}$ .

1.3. Ngữ nghĩa (semantic) của logic bậc nhất

Để cho các công thức có ý nghĩa thì ta cần gán ý nghĩa cho các biến dựa trên một cấu trúc nào đó của bộ từ vựng ${\tau}$ . Gọi ${\mathcal A}$ là một cấu trúc của bộ từ vựng ${\tau}$ . Để cho đơn giản, trong phần này ta chỉ nói đến các câu và các kết quả liên quan. Đề mục tiếp theo sẽ dùng đến các công thức có biến tự do.

Gọi ${\varphi}$ là một câu bậc nhất. Cấu trúc ${\mathcal A}$ thoả mãn câu ${\varphi}$ nếu ${\varphi}$ đúng dưới cấu trúc này; khi đó ta viết ${\mathcal A \models \varphi}$ . Một thuật ngữ hay được dùng khác để mô tả ${\mathcal A \models \varphi}$ là ${\mathcal A}$ là mô hình của ${\varphi}$ .

Một tập các câu bậc nhất được gọi là một lý thuyết bậc nhất (first-order theory), hay đơn thuần là lý thuyết cho gọn. Gọi ${\Phi}$ là một lý thuyết. Nếu cấu trúc ${\mathcal A}$ là mô hình của tất cả các câu trong ${\Phi}$ thì ta viết ${\mathcal A \models \Phi}$ , và gọi ${\mathcal A}$ là mô hình của ${\Phi}$ . Tập ${\Phi}$ là thoả mãn được (satisfiable) nếu có một mô hình cho nó.

Câu ${\varphi}$ là một hệ quả của tập công thức ${\Phi}$ , ký hiệu là ${\Phi \models \varphi}$ , nếu ${\mathcal A \models \Phi}$ suy ra ${\mathcal A \models \varphi}$ , với mọi cấu trúc ${\mathcal A}$ .

1.4. Vài kết quả cơ bản của logic bậc nhất

Thế làm thế nào để kiểm chứng rằng một câu ${\varphi}$ là hệ quả của một lý thuyết ${\Phi}$ ? Trong định nghĩa ở trên thì “hệ quả” là hệ quả ngữ nghĩa, buộc phải đúng với mọi cấu trúc. Ví dụ, nếu áp dụng máy móc định nghĩa trên thì để chứng minh rằng ${\varphi}$ là một hệ quả của lý thuyết ${\Phi}$ (hoặc hệ tiên đề ${\Phi}$ ) thì ta phải kiểm tra tất cả các mô hình của ${\Phi}$ . Điều này không tưởng. May mà trên thực tế ta không cần phải làm vậy, mà ta có thể “chứng minh” rằng ${\Phi}$ dẫn đến ${\varphi}$ chỉ bằng các thao tác hình thức, dùng các luật suy dẫn của logic bậc nhất. Nếu ${\varphi}$ là hệ quả hình thức của ${\Phi}$ (thay vì hệ quả ngữ nghĩa như định nghĩa ở trên) thì ta viết ${\Phi \vdash \varphi}$ .

Như đã viết, định lý sự toàn vẹn của Godel (completeness theorem) nói rằng ${\Phi \vdash \varphi}$ nếu ${\Phi \models \varphi}$ . Ngược lại, định lý tính hợp lý (soundness theorem) của Godel cho ta biết chiều ngược lại cũng đúng: nếu ${\Phi \vdash \varphi}$ thì ${\Phi \models \varphi}$ .

Lý thuyết về các chứng minh hình thức (proof theory) cần trả lời câu hỏi: “liệu ta có chứng minh được ${\varphi}$ từ ${\Phi}$ không?” Còn lý thuyết mô hình (model theory) thì quan tâm đến tác động của các cấu trúc cụ thể đến các phát biểu logic. Định lý tính hợp lý và định lý tính toàn vẹn của Godel kết nối hai lý thuyết này: ${\Phi \vdash \varphi}$ nếu và chỉ nếu ${\Phi \models \varphi}$ .

Ngoài ra, từ định lý Löwenheim-Skolem, ta cũng chứng minh được rằng ${\Phi \models \varphi}$ nếu và chỉ nếu mọi cấu trúc đếm được (countable structures) ${\mathcal A}$ thoả mãn ${\Phi}$ đều thoả mãn ${\varphi}$ . Nói cách khác, để kiểm tra ${\Phi \models \varphi}$ ta không cần phải xét mọi cấu trúc mà chỉ cần xét mọi cấu trúc đếm được mà thôi.

Một kết quả rất quan trọng nữa của logic bậc nhất là định lý compắc (compactness theorem). Định lý này nói rằng nếu ${\Phi \models \varphi}$ thì tồn tại một tập con hữu hạn ${\Phi'}$ của ${\Phi}$ sao cho ${\Phi' \models \varphi}$ . Một cách nôm na, nếu ta chứng minh được một phát biểu ${\phi}$ từ một hệ tiên đề ${\Phi}$ nào đó thì tồn tại một hệ tiên đề hữu hạn ${\Phi'}$ mà từ đó ta cũng suy ra ${\varphi}$ được. Ta có thể chứng minh định lý compắc dùng định lý toàn vẹn của Godel. Một cách khác, có lẽ phổ dụng hơn, để phát biểu định lý compắc là: ${\Phi}$ thoả mãn được nếu và chỉ nếu mọi tập con hữu hạn của ${\Phi}$ đều thoả mãn được. Terry Tao có một bài về định lý toàn vẹn của Godel và định lý compắc, bạn có thể tham khảo thêm. Đặc biệt là bài của Tao viết nhiều phát biểu tương đương của định lý toàn vẹn và định lý compắc.

Kết quả nổi tiếng và quan trọng nhất của logic bậc nhất là hai định lý bất toàn (incompleteness theorems) của Godel mà ta sẽ thảo luận vào dịp khác. Chúng cũng không liên quan mấy đến CSDL.

2. Truy vấn giao

2.1. Các cấu trúc hữu hạn

Liên hệ giữa CSDL và lý thuyết mô hình hữu hạn (finite model theory) rất rõ ràng: mỗi cấu trúc đại diện cho phần dữ liệu của một CSDL quan hệ, còn các phát biểu logic có thể dùng để mô tả các phép truy vấn (xem cụ thể dưới đây). Còn liên hệ giữa CSDL và lý thuyết chứng minh thì sẽ xuất hiện khi ta nghiên cứu về các phụ thuộc hàm (functional dependency) trong một CSDL. Nói tóm lại, liên hệ giữa logic và CSDL là cực kỳ mật thiết. Trong 40 năm đổ lại đây, rất nhiều nhà logic học có đóng góp cơ bản cho CSDL và ngược lại. Quyển Finite Model Theory Của Ebbinghaus và Flum là một tham khảo tốt. Chợt nhớ hồi năm 1999, tôi tham dự một nhóm đọc sách của giáo sư Wayne Richter ở Minnesota về lý thuyết mô hình hữu hạn dùng quyển sách này. Hồi đó chỉ đọc cho biết. Nhóm đọc gồm 3 người: Wayne, một cậu khoa Toán, và tôi. Không ngờ 13 năm sau lại đọc lại quyển này! Trên trang nhà của G.S. Richter có câu “nhất sư nhì phụ.” Ông là học trò cuối cùng của Alonzo Church.

Khi dùng khái niệm cấu trúc của logic bậc nhất để mô tả một CSDL thì các cấu trúc với miền hữu hạn là các đối tượng chính, tại vì hiển nhiên một CSDL không thể có kích thước vô hạn. Không may (hay may cho các nhà nghiên cứu lý thuyết mô hình hữu hạn) là một số kết quả cơ bản nhất của logic bậc nhất không còn đúng nếu ta chỉ được phép dùng các cấu trúc hữu hạn. Ví dụ, khi viết ${\Phi \models \varphi}$ thì theo định nghĩa mọi cấu trúc ${\mathcal A}$ thoả ${\Phi}$ đều thoả ${\varphi}$ , kể cả các cấu trúc vô hạn ${\mathcal A}$ . (Một cấu trúc là vô hạn nếu miền của nó vô hạn.) Bây giờ, nếu ta chỉ cần xét các cấu trúc hữu hạn thì ta cũng định nghĩa tương tự, và viết ${\Phi \models_{\text{fin}} \varphi}$ . Tất nhiên ${\Phi \models \varphi}$ suy ra ${\Phi \models_\text{fin} \varphi}$ . Nhưng điều ngược lại không đúng. Cả định lý compắc và định lý toàn vẹn đều không đúng trong môi trường hữu hạn.

Ví dụ, xét lý thuyết ${\Phi = \{ \varphi_{\geq n} \ | \ n \geq 1 \}}$ , trong đó ${\varphi_{\geq n}}$ là một câu bậc nhất khẳng định rằng miền của cấu trúc có kích thước ít nhất là ${n}$ . (Ví dụ, ${\varphi_{\geq 3} = \exists x, y, z (x \neq y \wedge x \neq z \wedge y \neq z)}$ .) Thì một tập con hữu hạn bất kỳ của ${\Phi}$ có một mô hình hữu hạn, nhưng ${\Phi}$ không có mô hình hữu hạn nào. Do đó, định lý compắc không đúng với các mô hình hữu hạn. Câu ${\varphi}$ được gọi là hợp lệ (logically valid) nếu ${\emptyset \models \varphi}$ , nghĩa là ${\varphi}$ đúng với mọi cấu trúc và mọi phép gán. Từ định lý toàn vẹn, ta có thể liệt kê tất cả các câu hợp lệ bằng một thuật toán, áp dụng luận suy diễn bậc nhất. Do đó, tập tất cả các câu bậc nhất hợp lệ là tập liệt kê đệ qui (recursively enumerable). Nhưng định lý Trakhtenbrot cho ta biết rằng tập các câu bậc nhất hợp lệ với mọi cấu trúc hữu hạn lại không phải là tập đếm được đệ qui. Vì thế, định lý toàn vẹn của Godel cũng không còn đúng trong môi trường hữu hạn.

Vì các lý do trên, lý thuyết mô hình hữu hạn phát triển theo một hướng rất khác với lý thuyết mô hình cổ điển. Lý thuyết mô hình hữu hạn gần với lý thuyết độ phức tạp của khoa học máy tính và được khác nhà khoa học máy tính nghiên cứu kỹ lưỡng mấy chục năm đổ lại.

2.2. Ngôn ngữ truy vấn bậc nhất và truy vấn giao

Khi ta xem các cấu trúc (hữu hạn) như một CSDL thì các công thức bậc nhất có thể dùng để đặt câu hỏi về CSDL nọ. Ví dụ, xét cấu trúc đồ thị đơn ${\mathcal A = (V, E^{\mathcal A})}$ như trong Ví Dụ 1. Nếu câu ${\forall x \forall y (x \neq y \rightarrow Exy)}$ là đúng thì đồ thị là đồ thị đầy đủ (complete graph). Xét công thức:

$\displaystyle \varphi(x,y) = Exy \vee \exists z (Exz \wedge Ezy).$

Công thức này có hai biến tự do ${x,y}$ . Công thức này đúng với một phép gán ${\alpha}$ gán các biến tự do các giá trị cụ thể nào đó nếu như phép gán ${\alpha}$ gán ${x,y}$ một cặp đỉnh cách nhau nhiều nhất là ${2}$ chặng. Công thức ${\varphi(x,y)}$ như trên có thể xem là một truy vấn vào CSDL đồ thị. Bài toán định trị phép truy vấn là bài toán tìm tất cả các phép gán ${\alpha}$ vào ${x,y}$ sao cho ${\varphi(\alpha(x), \alpha(y)}$ được thoả mãn.

Một lớp các truy vấn rất quan trọng là lớp các truy vấn giao (conjunctive queries). Đây là lớp các truy vấn có dạng

$\displaystyle \varphi(x_1,\dots,x_k) = \exists x_{k+1},\dots, x_n A_1 \wedge A_2 \wedge \cdots \wedge A_r,$

trong đó ${x_1,\dots,x_k}$ là các biến tự do, ${x_{k+1},\dots,x_n}$ là các biến bị giới hạn, và ${A_1,\dots, A_r}$ là các công thức nguyên tử. Các truy vấn giao tương đương với các phát biểu SQL dạng \texttt{select … from … where} mà phần \texttt{where} là giao của các đẳng thức đơn giản. Các truy vấn giao đóng góp phần lớn các truy vấn vào CSDL hiện đại.

Để thấy sức mạnh của truy vấn giao, ta xét thêm vài ví dụ trên các cấu trúc đồ thị. Để liệt kê các tam giác trong một đồ thị ta có thể viết

$\displaystyle \phi(x,y,z) = Exy \wedge Eyz \wedge Ezx.$

Dùng nguyên tắc tương tự, ta dễ dàng ghi lại được các truy vấn giao hỏi liệt kê tất cả các đồ thị con với một cấu trúc cho trước (tam giác, clique ${K_5}$ , v.v.) của một đồ thị lớn. Những bài toán loại này rất quan trọng trong phân tích các mạng phức tạp (complex networks) như các mạng tương tác protein trong sinh học hoặc các mạng xã hội. Ví dụ khi đếm tổng số tam giác trong một mạng xã hội, ta tính được các hệ số cluster (clustering coefficients), còn khi liệt kê các đồ thị con với cấu trúc cho trước của mạng sinh học ta có thể tìm các motif.

Một câu hỏi cực kỳ quan trọng là, thiết kế một thuật toán hiệu quả với inputs là một cấu trúc và một phép truy vấn (giao), in ra các phép gán thoả mãn truy vấn. Đây là bài toán định trị phép truy vấn giao, đề tài của bài viết tiếp theo trong chuỗi.

Link to full article