CHƯƠNG I. CƠ SỞ TOÁN HỌC 1. Hệ thống viết lại số hạng (Term Rewiting System – TRS) là gì? Trong toán học, khoa học máy tính và logic học có một phương pháp được xem là một tập hợp mà ở đó nó bao gồm các kỹ thuật toán học, các bộ luật để phát triển phần mềm và các hệ thống phần cứng. Trong công nghệ phần mềm chúng ta có thể sử dụng phương pháp này để khai thác sức mạnh của các ký hiệu và chứng minh toán học.
Phương pháp này chính là Hệ thống viết lại số hạng (Term Rewriting System – TRS), với phương pháp này các quy tắc viết lại được sử dụng để xác định các thuộc tính và yêu cầu của chương trình. Tất cả chúng ta đã từng học từng sử dụng hệ thống viết lại mà chúng ta không hề hay biết, ngay khi chúng ta còn ở trường học. Khi chúng ta đơn giản hóa một phương trình toán học chúng ta có thể làm như sau: (3 + 4) (4 + 2) → 7 (4 + 2) → 7 6 → 42 (1) Cách đơn giản phương trình này là việc sử dụng các phép toán cộng và nhân được bổ sung vào, các luật này giống như: 0 + 1 → 1, 0 + 2 → 2, 0 + 3 → 3, .với việc kết hợp các tổng để rồi tích các tổng đã tính lại với nhau ta tìm ra kết quả. Cũng có thể hiểu rằng TRS là tập các luật được xây dựng bằng các dữ liệu đầu vào, quá trình xây dựng được lặp đi lặp lại với các điều kiện khác nhau cho đến khi thu được kết quả đơn giản nhất.
Ý tưởng của TRS được làm rõ qua ví dụ về “Coffee Can Problem”, ta có hai giống cà phê đen và trắng ta được phép sắp xếp theo thứ tự nào đó (ngẫu nhiên) – đây là đầu vào (Input). white white black black white white black black (2) Các bộ luật (qui tắc) được quy định là: black white→black white black → black (3) black black → white white white → black 3 Bộ qui tắc này là một ví dụ điển hình cho hệ thống viết lại. Mỗi qui tắc đều diễn ra một động thái, một quy phạm đúng, đầu tiên bất kỳ hạt cà phê nào màu trắng khi được kết hợp với hạt đen thì đều cho ra màu đen và ngược lại, tiếp đến nếu hai hạt cùng màu thì sẽ cho ra hạt có màu còn lại. Ví dụ dưới đây là một chuỗi các luật được lặp đi lặp lại trong suốt quá trình tìm lời giải đơn giản nhất.
white white black black white white black black white white black black white black black white white white white black black white white white black black white white black black white black black black black white Mục tiêu của bài toán là tìm ra càng ít hạt cà phê càng tốt, ta có thể thấy rằng với một số lẻ hạt cà phê đen bài toán sẽ luôn tìm ra lời giải cuối cùng là một hạt màu đen. Ví dụ trên cơ bản làm rõ hệ thống viết lại số hạng là gì, nó bao gồm các đầu vào, mô hình xây dựng các bộ luật (qui tắc), và đầu ra là một kết quả đơn giản nhất. Các đặc tính quan trọng của một TRS bao gồm: Không xác định: Sử dụng các luật không xác định, có nghĩa là trong một bài toán, một phép giải chúng ta có thể sử dụng các quy tắc, các luật khác nhau: (3+4) (4+2) → 7 (4+2) → 7 4+7 2→7 4 +14 → 28+14 → 42 (4) Chúng ta có thể nhìn thấy ở mỗi bước của (2) các luật được sử dụng một cách linh hoạt nhưng vẫn tuân thủ đúng quy tắc toán học ta gọi đây là một chuỗi ghi đè hợp lệ. Nói chung, quá trình viết lại là không xác định trước.
Kết quả cuối cùng giống nhau: Tính độc đáo của việc sử dụng các luật một cách không xác định trước nằm ở chỗ chúng đều cho ra một kết quả cuối cùng giống nhau, mặc dù đường đi lời giải khác nhau. Chấm dứt: Mỗi lần viết lại đều có thể được mở rộng ra để dễ dàng tiếp cận kết quả, và cũng có thể loại trừ để kết thúc bài toán. 4 Hợp nhất : Tính hợp nhất có tính chất làm đảm bảo các luật trong cùng hệ thống được viết lại bằng những cách khác nhau nhưng cho ra kết quả tương tự. Hợp nhất thì bao gồm hợp nhất cục bộ và hợp nhất toàn bộ, để làm rõ ta có ví dụ sau: Cho R={ F, R } là một hệ thống viết lại số hạng, chúng ta nói rằng R là : Hợp nhất cục bộ nếu : cho tất cả , , ’ , , bất kỳ khi nào → và → t’, ta có u T(F,X) như vậy t →∗ u và t’ →∗ u.
Hợp nhất toàn bộ nếu : cho tất cả s, t, t’ T(F,X), bất kỳ khi nào s → ∗t và s →∗t’, ta có u T(F,X) như vậy t →∗ u và t’ →∗ u.1 : Tính hợp nhất Để có thể hiểu rõ về hệ thống viết lại số hạng, ta khảo sát hệ thống sau. Hệ thống dùng để đặc tả phép cộng của các số tự nhiên bằng cách sử dụng hằng số 0 và hàm s với tập luật : x+0→x [Luật R1] x + s(y) → s(x+y) [Luật R2] x+y→ y+x [Luật R3] Trong đó, x và y là các biến số. Khi một biểu thức phù hợp với vế trái của một luật, ta có thể viết lại biểu thức đó dưới dạng vế phải. Ví dụ 1: Với biểu thức s(s(0)) + 0, nếu thay x bằng s(s(0)) (vì x là biến số nên có thể được thay bằng các biểu thức) thì biểu thức này theo đúng cấu trúc vế 5 trái của luật R1, nên có thể viết lại thành s(s(0)) (vì áp dụng R1, kết quả là x mà x = s(s(0))).
Quá trình trên có thể được biểu diễn thành: s(s(0)) + 0 → s(s(0)) [R1] Trong hệ thống này, các số tự nhiên được biểu diễn bằng cách đếm số lượng hàm s trong một số hạng. Ví dụ 2: Số 0 được biểu diễn bằng 0, 1 được biểu diễn bằng s(0), 2 được biểu diễn bằng s(s(0)). Phép cộng được thể hiện trong các luật cũng chính là phép cộng hai số tự nhiên. Ví dụ 3: Khi thực hiện phép cộng số 1 (được biểu diễn bằng s(0)) và số 2 (được biểu diễn bằng s(s(0))), ta tìm cách áp dụng các luật để có thể loại bỏ được tất cả các dấu + trong biểu thức được tạo thành: s(0) + s(s(0)) → s(s(0) + s(0)) [R2] → s(s(s(0) + 0) [R2] → s(s(s(0))) [R3] Như vậy kết quả của phép cộng là s(s(s(0))) là biểu diễn của số 3.
Ta cũng có thể áp dụng các luật theo một thứ tự khác để ra được kết quả cuối cùng: s(0) + s(s(0)) → s(s(0)) + s(0) [R3] → s(s(s(0)) + 0) [R2] → s(s(s(0))) [R1] Một hệ thống được đặc tả gồm các luật như trên gọi là hệ thống viết lại số hạng. Việc tìm hiểu về hệ thống viết lại số hạng liên quan đến cách điều hướng các luật này và các điều kiện để đảm bảo hệ thống luật tạo ra có sức mạnh tính toán bằng với hệ thống phương trình mà nó được tạo ra từ trước đó. Các khái niệm cơ bản trong TRS a) Tập chữ kí Một tập chữ kí (Signature) ∑ là một tập các ký hiệu hàm, trong đó mỗi f ∑ được liên kết với một số không âm n là bậc của f. So sánh với khái niệm hàm số trong ngôn ngữ lập trình, tập chữ kí chính là tập chứa tên các hàm số với bậc của một tập chữ kí chính là số lượng thông số của hàm số đó.Tập các phần tử có cùng bậc n của ∑ được ký hiệu là ∑ (n).
Hằng số là tập các phần tử có bậc 0 của ∑: ∑ (0). 6 b) Term Khái niệm Term được xây dựng dựa trên các ký hiệu biến, signature. Cho ∑ là một tập chữ kí và X là một tập các biến sao cho ∑ ∩ X ≠ ∅ (không thể có ký hiệu nào vừa là biến, vừa thuộc tập chữ kí được). Tập tất các các Term được ký hiệu T( ∑, X ) được đặc tả một cách đệ quy: tất cả biến đều là Term: X ⊂ T(∑, X).
Ví dụ 4: 0, s đều là các Term, với f thuộc tập chữ kí (f ∑), nếu t1, t2, … tn đều là các Term thì f( t1, t2, … tn ) là một Term: f( t1, t2, … tn ) ∑. Ví dụ 5: s(s(0)), s(0) + 0 đều là các Term. (Phép + ở đây là một hàm số có 2 thông số. c) Rút gọn → Đây là một quan hệ nhị phân trên tập hợp T( ∑, X ).
Thay vì viết (a, b) ϵ →, ta thường viết dưới dạng a → b. Ta có thể biểu diễn quan hệ trên dưới dạng: {x + 0 → x, x + s(y) →s (x+y), x + y → y + x}. x được gọi là khả rút gọn nếu và chỉ nếu tồn tại một giá trị y để mà x → y. x được gọi là ở dạng chuẩn nếu và chỉ nếu x không khả rút gọn.
y được gọi là một chuẩn của x nếu và chỉ nếu x → y và y ở dạng chuẩn. Ví dụ 7: Để minh họa các khái niệm, ta dùng biểu diễn trực quan của 2 cách áp dụng luật để tính s(0) + s(s(0)) : Hình 1.2 : Ví dụ về khả năng rút gọn về Term. 7 Giải thích: s(0) + s(s(0)) khả rút gọn. s(0) + s(0) không ở dạng chuẩn.
d) Tập biến: Là tập các biến số có mặt trong Term t. Ví dụ 8: Var(0) = vì Term 0 không có biến số; var (x + s(y)) = { x , y } vì có 3 ký hiệu trong term x + s(y) là x, s và y trong đó s là một hàm số: s ∑, x và y là biến: x,y X. e) Luật viết lại: Là là một luật có dạng VT → VP sao cho VT không phải là một biến và Var(VT) ⊇ Var(VP). f) Hệ thống viết lại số hạng: Là một tập hợp gồm các luật viết lại.
Ví dụ 9: Hệ thống gồm các luật {x + 0 → x, x + s(y) → s (x + y), x + y → y + x }, trong đó ∑ = {s, 0}, X = {x, y} là một hệ thống viết lại số hạng. g) Vị trí của term Cho S là một tập chữ kí, X là một tập các biến ( ∑ ∩ X ≠ ∅ ) và s, t là các Term. Tập các vị trí của Term s là tập hợp Pos(s) (Position) là một chuỗi các số dương được định nghĩa một cách đệ quy: Nếu s là biến thì Pos(s) = { }.