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
|
1
2
3
4
5
|
reverse :: [ a ] -> [ a ]
reverse [ ] = [ ] ( 1 )
reverse ( x : xs ) = reverse xs ++ [ x ] ( 2 )
|
Trong đó hàm ++ được định nghĩa như sau
|
1
2
3
4
5
|
++ :: [ 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 []) = []
|
1
2
3
4
5
|
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ổ đề
|
1
2
3
|
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
|
1
2
3
4
5
6
7
8
|
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
|
1
2
3
4
5
6
|
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
|
1
2
3
4
5
6
7
8
|
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 đó.
Có thể bạn quan tâm:
Hướng dẫn lập trình nhận dạng hình ảnh với Opencv
Sách hướng dẫn lập trình game trên Android, Beginning Android 4 ...
Hướng dẫn lập trình smart TV SamSung
Thực tập lập trình C++ và Objective-C
Tài liệu lập trình mạng xã hội với Open Social
Nhân viên lập trình Android và iOS
Nhân viên lập trình game mobile
Nhân viên lập trình website asp.net
IoT là gì? ứng dụng của IoT trong cuộc sống hiện đại
Lập trình viên và chuyện học ngoại ngữ
Có thể bạn chưa biết:
TUYỂN THỰC TẬP REACT NATIVE
* Trang bị kỹ năng về JS, lập trình hybrid app, sử dụng những công cụ hỗ trợ (VScode, github, sourcetree, ...)
* Thành quả mong muốn là các bạn tham gia sẽ có được kỹ năng lập trình hybrid app
Biểu mẫu đăng ký training tại đây >> http://bit.ly/2NK9YWd
TEAM MOBILE APPS - CTY DVMS
