Final problems with the algorithm ?

  Cứ mỗi lần họp với Prof xong thì mình lại có cảm giác như bị kiệt sức. Ngày hôm nay meeting cũng khá vui, dù tôi đã chuẩn bị hết tất cả mọi thứ cần thiết như chuẩn bị sẵn slide, các ghi chú cần thiêt cho buổi họp, bật sẵn chương trình thu âm nội dung cuộc họp ….

  Thông thường tôi đến trước buổi họp 5 phút, lần này cũng vậy, nhưng khi bật cái máy lên thì hỡi ôi, không ăn thua. Máy treo, chương trình đứng, không show lên màn hình lớn được. Trong khi thời gian họp chỉ được 30 phút thôi. Sau khi tắt máy cứng tôi đành phải trình bày chay 1 đoạn trong lúc chờ đợi máy restart lại xong.
  Sở dĩ tôi đề nghị họp vào thời điểm này là do tôi đang muốn Prof. có thể đưa ra một vài góp ý cho công việc của tôi, vốn đang bị dậm chân tại chỗ. Tôi vẫn chưa tìm ra được một cách chứng minh cụ thể và thuyết phục để có thể trình bày trước Prof. Thông thường tôi sẽ dành thời gian để ngồi suy nghĩ và tìm mọi cách để giải quyết. Sau 3 ngày không suy nghĩ ra thì tôi sẽ trình bày với Prof để ông có thể gợi ý cho tôi tìm hiểu thêm.

   Tuy nhiên lần này thì thời gian tôi chỉ còn 4 tuần để hoàn tất mọi thứ, nên tôi đành phải rút ngắn xuống 2 ngày thôi. Nhờ vậy mà hôm nay tôi đã có thể nắm rõ được vấn đề tôi cần giải quyết là gì và nên áp dụng phương pháp nào. 

1.    Trước tiên là vấn đề về thuật toán: Tôi đã xây dựng được thuật toán hoàn chỉnh cho bài toán view-maintenance. Đó là điều đáng mừng.
   1. Tôi cần chứng minh tính đúng đắn của thuật toán đề xuất, bằng phương pháp toán học. Hiện tại, thuật toán được trình bày ở dạng cài đặt, tức là phương pháp thực hiện thuật toán giống như phương pháp cài đặt. Khi đó thì việc chứng minh sẽ không thể trọn vẹn và đầy đủ được.
   2. Bài toán đặt ra hiện nay là làm thế nào để trừu tượng hóa thuật toán ???
2. Như thế nào là trừu tượng hóa ? Ví dụ đơn giản về cách tiếp cận của thuật toán. 
   1. Giả sử tôi cần tìm cây con chung của 2 cây. Hiện tại trong thuật toán thì tôi dùng phương pháp tách từ nút ngọn đến nút lá của cây thành từng cây đơn, và gom những cây đơn này lại chung với nhau trong một danh sách gọi là danh sách cây đơn.
   2. Về mặt cài đặt thì cách trình bày trên sẽ ổn thỏa, nhưng nếu về mặt tổng quát thì không thể hiện đầy đủ. Người phản biện có thể đặt câu hỏi rằng "Nếu mình đã sử dụng phương pháp TREE-MATCHING thì tại sao phải tách thành từng cây con".
   3. Do vậy về mặt tổng quát trình bày, thì phải sửa lại cách tiếp cận là dùng phương pháp tree-matching để lấy ra cây con chung hoặc lấy thông tin cần thiết gì đó. Tuy nhiên, nếu chỉ sửa đổi như vậy, thuật toán vẫn chưa ở mức tổng quát được. Từ thông tin tree-matching đó, tôi phải thay đổi và thiết kế lại thuật toán với dữ liệu và phương pháp tree-matching để kết quả được thống nhất với nhau.
3. Sau khi đã chỉnh sửa và thay đổi thuật toán từ mức cài đặt về mức tổng quát thì lúc này tôi có thể suy nghĩ về phương pháp chứng minh tính đúng đắn của thuật toán. Thực ra mà nói thì phương pháp đã có rồi, vấn đề là áp dụng phương pháp chứng minh vào bài toán của tôi như thế nào thôi.
   1. Trước khi nghe những góp ý và gợi ý của các GS, tôi vẫn còn mơ hồ về khái niệm chứng minh quy nạp trên CSDL. Vì lý do là mình không có được công thức tổng quát, nhưng hôm nay, sau khi họp với GS thì tôi mới biết thêm được rằng không phải dựa trên những câu truy vấn trên CSDL đó để chứng minh. Mà thực ra là cần chứng minh biểu thức (g f $db = f g' $db), chỉ vậy là đủ.
   2. Khi này với các trường hợp $db khác nhau, ta có thể áp dụng thuật toán để chứng minh qui nạp một cách dễ dàng.

   Kết luận: tóm tắt lại những khó khăn và trình bày trên là phần công việc chính yếu cần phải làm. Đầu tiên là:

1. Xây dựng lại thuật toán với mức tổng quát hóa và trừu tượng hóa cao.


2. Dựa vào biểu thức (g f $db = f g' $db) để chứng minh tính đúng đắn của thuật toán.


3. Vừa cài đặt vừa suy nghĩ cách chứng minh.