Chứng minh tính đúng đắn

    Chiều nay họp với Prof. xong, cảm giác hồ hởi ban đầu không còn nữa, thay vào đó là một sự lo lắng. Khi chứng minh tính đúng đắn, một vấn đề nan giải là dựa vào đâu mà biết được chương trình của mình ... đúng đắn. Tức là chọn hệ qui chiếu gì?
   Sau khi dùng một cách gọi nôm na là nông dân nhất, dùng diễn giải thông thường và các testcase để kiểm tra thì không có phương pháp nào khác được trình bày trong báo cáo. Khi này, một phản ví dụ được đưa ra và thế là ... toi :D. Vấn đề rất đơn giản: phải về suy nghĩ cách chứng minh lại.
   Sau khi trao đổi với nhau, bắt đầu bằng một phong cách nói chuyện rất quen thuộc, 'ý tưởng của cậu rất hay, nhưng tôi nghĩ ...', một mẫu câu giao tiếp khá phổ biến trong phong cách Nhật Bản. Vấn đề là cần chứng minh được 2 yếu tố sau đây:
      1. Đầu tiên là vấn đề về primitive function: không cần phải chứng minh quá nhiều với ví dụ quá phức tạp, chỉ cần đưa ra được một mẫu xử lý dạng primitive để từ dạng primitive đó, phát triển lên thành những dạng composition có sẵn.
               Ví dụ: với mẫu xử lý f($g), khi này f($g) sẽ là dạng primitive. Tiếp theo xây dựng một mẫu primitive khác, f(d:$g), đây là dạng constructor của tree. Từ một đỉnh, xây dựng thành một cây (construction), hoặc từ một cây hiện tại, chuyển đổi/hay phân rã thành một dạng cây khác (destruction). Sau khi xây dựng xong dạng primitive này rồi thì sẽ chuyển các dạng phức tạp khác về dạng primitive (các dạng chuyển đổi này đã được xây dựng sẵn).
       2. Sau khi có được primitive function: cần chứng minh thêm về tính tương đương (bisimilar hay similar - theo trực giác - intuitively).
               Trong bài toán hiện tại, tôi cần thực hiện qui trình sau đây: từ đồ thị db ta có:
                                         source --> f-expression  --> view
                                            |                                          |
                                         g-expression                g'-expression
                                            |                                          |
                                         source'--> f-expression  --> view'
               Hiện giờ đã làm được phần view maintenance, tức là thay đổi ở source và update ngược lại ở view. Khi này con đường đi sẽ là g'(view).
               Tôi cần chứng minh liệu với primitive function đã cài đặt, kết quả có giống như .... đi theo con đường bình thường: f( g(source)) = g'( f(source)) ??? Liệu có tương đương với nhau hay không?