Phương pháp suy luận trong lập trình hàm
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ữ
DVMS chuyên:
- Tư vấn, xây dựng, chuyển giao công nghệ Blockchain, mạng xã hội,...
- Tư vấn ứng dụng cho smartphone và máy tính bảng, tư vấn ứng dụng vận tải thông minh, thực tế ảo, game mobile,...
- Tư vấn các hệ thống theo mô hình kinh tế chia sẻ như Uber, Grab, ứng dụng giúp việc,...
- Xây dựng các giải pháp quản lý vận tải, quản lý xe công vụ, quản lý xe doanh nghiệp, phần mềm và ứng dụng logistics, kho vận, vé xe điện tử,...
- Tư vấn và xây dựng mạng xã hội, tư vấn giải pháp CNTT cho doanh nghiệp, startup,...
Vì sao chọn DVMS?
- DVMS nắm vững nhiều công nghệ phần mềm, mạng và viễn thông. Như Payment gateway, SMS gateway, GIS, VOIP, iOS, Android, Blackberry, Windows Phone, cloud computing,…
- DVMS có kinh nghiệm triển khai các hệ thống trên các nền tảng điện toán đám mây nổi tiếng như Google, Amazon, Microsoft,…
- DVMS có kinh nghiệm thực tế tư vấn, xây dựng, triển khai, chuyển giao, gia công các giải pháp phần mềm cho khách hàng Việt Nam, USA, Singapore, Germany, France, các tập đoàn của nước ngoài tại Việt Nam,…
Quý khách xem Hồ sơ năng lực của DVMS tại đây >>
Quý khách gửi yêu cầu tư vấn và báo giá tại đây >>