Phương pháp suy luận trong lập trình hàm

kiennt viết ngày 26/09/2016

Trong quá trình tìm hiểu về Free Monad, khi đọc các paper tôi gặp một số vấn đề để hiểu về phương pháp chứng minh các giả thuyết. Tìm hiểu kỹ hơn là do bản thân tôi chưa hiểu rõ phương pháp suy luận trong lập trình hàm.
Bài viết này nhằm giới thiệu phương pháp thường dùng trong lập trình hàm: Phương pháp quy nạp (induction)

Phương pháp quy nạp nói lên rằng: nếu bạn muốn chứng minh một giả thuyết P, chúng ta sẽ chứng minh (1) P đúng với một trường hợp cơ sơ, (2) dựa vào giả thuyết quy nạp, chúng ta sẽ chứng minh nếu P đúng với trường N, thì P cũng đúng với trường hợp N'. Việc biến đổi từ N -> N' sẽ là bao hàm toàn bộ tập các dữ liệu của chúng ta.

Ví dụ, xét trường hợp hàm reverse được định nghĩa như sau

reverse :: [a] -> [a]
reverse [] = []                                               (1)
reverse (x:xs) = reverse xs ++ [x]                            (2)

Trong đó hàm ++ được định nghĩa như sau

++ :: [a] -> [a] -> [a]
[] ++ xs = xs                                       (3)                         
(x:xs) ++ ys = x:(xs ++ ys)                         (4)

Giờ, hãy chứng minh rằng reverse(reverse x) = x.

Trường hợp cơ sở là reverse(reverse []) = []

reverse (reverse []) 
    = reverse []                # do (1)
    = []                        # do (1)

Giờ, chúng ta giả sử dùng reverse(reverse xs) = xs (giả thiết quy nạp), chúng ta sẽ chứng minh
reverse(reverse x:xs) = x:xs (5) bằng cách sử dụng một bổ đề

reverse(xs ++ ys) = reverse ys ++ revese xs       (6)

Việc chứng minh (6) sẽ được để lại sau, giờ giả sử rằng (6) đã được chứng minh, chúng sẽ sẽ chứng minh (5) như sau

reverse(reverse x:xs)
  = reverse(reverse xs ++ [x])                # do (2)
  = reverse([x]) ++ reverse(reverse xs)       # áp dụng giả thiết quy nạp
  = [x] ++ reverse(reverse xs)                # do định nghĩa hàm reverse([x])
  = [x] ++ xs                                 # do (4)
  = x:xs                                      # do (3)

Việc chứng minh bổ để (5) cũng được thực hiện bằng phương pháp quy nạp.

Trường hợp cơ sở reverse(xs ++ []) = reverse [] ++ reverse xs

reverse(xs ++ []) 
  = reverse xs
  = [] ++ reverse xs
  = reverse [] ++ reverse xs

Giờ, gỉa sử rằng reverse(xs ++ ys) = reverse ys + reverse xs, ta sẽ chứng minh
reverse(xs ++ (y:ys)) = reverse (y:ys) + reverse xs

reverse(xs ++ y:ys)) 
  = reverse((xs ++ [y]) ++ ys)                 # việc chứng minh điều này coi như là bài tập cho bạn đọc                                   
  = reverse ys + reverse (xs ++ [y])           # do giả thiết quy nạp
  = reverse ys ++ reverse [y] ++ reverse xs    # do giả thiết quy nạp
  = reverse ([y] ++ ys) ++ reverse xs          # do giả thiết quy nạp
  = reverse (y:ys) + reverse xs                    # do 4

Phương pháp quy nạp giúp tôi nhận ra một điều, bản chất của lập trình hàm (functional programming) là toán học. Nghĩa của từ hàm trong lập trình hàm chính là hàm toán học. Chính vì thế, lập trình hàm vừa dễ vừa khó. Dễ theo nghĩa nếu chúng ta hiểu được bản chất toán học của hàm, việc viết code sẽ trở nên rất ngắn gọn và chính xác. Tuy nhiên khó ở chỗ, để viết các hàm chúng ta cần nắm rõ được nền tảng toán học đằng sau đó