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

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 đó

Bình luận


White
{{ comment.user.name }}
Bỏ hay Hay
{{comment.like_count}}
Male avatar
{{ comment_error }}
Hủy
   

Hiển thị thử

Chỉnh sửa

White

kiennt

30 bài viết.
267 người follow
Kipalog
{{userFollowed ? 'Following' : 'Follow'}}
Cùng một tác giả
White
91 18
Mọi chuyện bắt đầu từ nắm 2013 trong quá trình xây dựng chức năng login với Facebook, tôi đã tìm ra một cách để tấn công vào các hệ thống login với...
kiennt viết 2 năm trước
91 18
White
50 4
Trong tuần vừa rồi, mình có đọc chương 7 cuốn sách (Link). Bài viết này nhằm mục đích giúp mình tổng hợp lại những kiến thức đã học được về chương ...
kiennt viết 2 tháng trước
50 4
White
29 5
1. Đặt vấn đề Một trong các vấn đề của một hệ thống backend là bài toán điều phối request tới các nguồn dữ liệu. Xét bài toán với một hệ thống bl...
kiennt viết gần 2 năm trước
29 5
{{like_count}}

kipalog

{{ comment_count }}

bình luận

{{liked ? "Đã kipalog" : "Kipalog"}}


White
{{userFollowed ? 'Following' : 'Follow'}}
30 bài viết.
267 người follow

 Đầu mục bài viết

Vẫn còn nữa! x

Kipalog vẫn còn rất nhiều bài viết hay và chủ đề thú vị chờ bạn khám phá!