- Dependent type (lý thuyết kiểu) có bao gồm các đối tượng chứng minh, nhưng tác giả đánh giá đây là một cấu trúc không cần thiết và kém hiệu quả
- Tác giả từng trực tiếp nghiên cứu các hệ thống dựa trên dependent type trong quá khứ như AUTOMATH và hệ hình thức Martin-Löf, nhưng Isabelle đã phát triển theo hướng một khung logic tổng quát (generic)
- Isabelle/HOL dựa trên lý thuyết kiểu đơn giản (higher-order logic) có thế mạnh về tự động hóa, thư viện quy mô lớn và tính dễ đọc
- Thông qua dự án ALEXANDRIA, tác giả chứng minh rằng chỉ với logic bậc cao cũng có thể hình thức hóa các định lý toán học cao cấp
- Dù các hệ thống dependent type như Lean đã trưởng thành hơn, tác giả vẫn ưu tiên tính thực dụng của cách tiếp cận logic bậc cao vì vấn đề hiệu năng và độ phức tạp
Dependent type và đối tượng chứng minh
- Trong lý thuyết dependent type, đối tượng chứng minh (proof objects) là bắt buộc, nhưng tác giả xem đó là sự lãng phí không gian
- Trong kiến trúc LCF, chỉ những bước chứng minh hợp lệ mới có thể được thực thi thông qua kiểm tra kiểu ở cấp ngôn ngữ triển khai, chứ không phải bên trong logic
- Nhờ trực giác của Robin Milner, khái niệm proof kernel được đưa vào và trở thành nền tảng của Isabelle
- Trước câu hỏi “vì sao không dùng dependent type”, tác giả trả lời rằng mình đã “dùng nó trong một thời gian dài”
Trải nghiệm với AUTOMATH
- Năm 1977 tại Caltech, tác giả đã nghe bài giảng về AUTOMATH của N. G. de Bruijn, nhưng không thể trực tiếp sử dụng hệ thống này
- Khi đó, hệ thống của Đại học Eindhoven chưa kết nối với ARPAnet, và còn cần một máy tính dựa trên ALGOL 60
- AUTOMATH là một hệ thống dependent type nhưng không hiện thực hóa tương ứng Curry–Howard
- Người dùng phải thêm ký hiệu và quy tắc suy luận của logic mình muốn dùng dưới dạng tiên đề
- de Bruijn ví điều này như một “nhà hàng lớn phục vụ mọi món ăn”
- Isabelle kế thừa ý tưởng đó và theo đuổi tính tổng quát như một khung logic
- Tuy nhiên, de Bruijn không ưa lý thuyết tập hợp và xem toán học về bản chất là dựa trên kiểu
- Tác giả từng đặt câu hỏi về việc kiểm chứng tính đúng đắn của AUTOMATH, và de Bruijn đã gửi một sách lý thuyết ngôn ngữ dày 300 trang, nhưng điều đó không làm tác giả hài lòng
Lý thuyết kiểu hình thức Martin-Löf
- Khi nghiên cứu lý thuyết kiểu hình thức Martin-Löf tại Đại học Chalmers ở Göteborg, tác giả bị cuốn hút bởi khả năng tổng hợp chương trình
- Tác giả đánh giá nó rõ ràng là “đúng” vì đã trực tiếp hiện thực hóa các nguyên lý của logic trực giác Heyting
- Trong nhiều năm nghiên cứu, tác giả đã hiện thực hóa phiên bản đầu tiên của Isabelle bằng lý thuyết Martin-Löf
- Hiện nay nó vẫn được phân phối dưới tên Isabelle/CTT
- Tuy nhiên, công trình này sụp đổ vì bầu không khí giáo điều xoay quanh Per Martin-Löf và sự chuyển đổi áp đặt sang intensional equality nội tại
- Các hệ thống xuất hiện sau đó như Calculus of Constructions(CoC), Rocq, Lean cũng để lại cùng một nghi vấn
- CoC trong nhiều thập kỷ đã liên tục tạo ra nhiều biến thể và các tiên đề tùy chọn
Lựa chọn nghiên cứu và hướng đi của Isabelle
- Các nhà nghiên cứu phải lựa chọn giữa phát triển hệ hình thức mới và mở rộng, khai thác các hệ thống hiện có
- Isabelle được thiết kế như một khung tổng quát hóa để chấp nhận nhiều loại logic khác nhau
- Năm 1985, Mike Gordon đã thực hiện kiểm chứng phần cứng bằng lý thuyết kiểu đơn giản của Church
- Sau đó John Harrison đã nghĩ ra cách mã hóa số chiều của vector
- Isabelle/HOL bổ sung cho lý thuyết của Church type class tiên đề hóa và hệ module locale
- Cộng đồng Lean, dựa trên CoC, đã đạt được kho toán học hình thức hóa khổng lồ (mathlib)
Dự án ALEXANDRIA và phép thử giới hạn của logic bậc cao
- Dự án ALEXANDRIA do ERC tài trợ nhấn mạnh vào tự động hóa, thư viện và tính dễ đọc của Isabelle
- Ban đầu người ta dự đoán logic bậc cao sẽ có giới hạn, nhưng trên thực tế ngay cả toán học cao cấp như lược đồ Grothendieck cũng đã được hình thức hóa thành công
- Paulo Emílio de Vilhena và Martin Baillon đã chứng minh rằng mọi trường đều có một mở rộng đóng đại số
- Dự án còn mở rộng tới các kết quả nâng cao như định lý Balog–Szemerédi–Gowers
- Luận điểm “không thể hình thức hóa toán học nếu không có dependent type” đã biến mất, chỉ còn lại lập luận rằng “dependent type gọn gàng hơn”
Lean và quan điểm hiện tại về dependent type
- Tác giả ngưỡng mộ quy mô cộng đồng của Lean và công cụ Blueprint, nhưng vấn đề hiệu năng và độ phức tạp vẫn còn nguyên
- Những va chạm với intensional equality và khó khăn trong việc quyết định khi nào nên dùng dependent type được báo cáo lặp đi lặp lại
- Tác giả ví dependent type như chế độ Full Self-Driving của Tesla, để chỉ ra kỳ vọng quá mức và sự bất tiện trong thực tế
Phụ lục: giới hạn lý thuyết của logic bậc cao
- Một số người cho rằng logic bậc cao yếu về mặt lý thuyết chứng minh, nhưng điều đó chỉ có nghĩa là yếu hơn so với lý thuyết tập hợp ZF
- Theo kết quả của ALEXANDRIA, logic bậc cao vẫn có thể xử lý các cấu trúc toán học phức tạp như lược đồ Grothendieck
- Chỉ có hai chứng minh cần bổ sung tiên đề ZF, và đó là các định lý nhắc trực tiếp đến các đối tượng ZF
Chú thích
- Chủ nghĩa trực giác là một triết lý xem ngôn ngữ như phương tiện ghi chép đơn thuần, và khác với toán học kiến tạo (constructive mathematics) ngày nay
1 bình luận
Ý kiến trên Hacker News
Kiểu phụ thuộc (dependent types) rất hữu ích trong một số tình huống
Ví dụ, sẽ rất tốt nếu Python có thể biểu diễn và kiểm tra kiểu như “ma trận
float32kích thước 10×5” bằng hệ thống kiểuTuy nhiên, các khái niệm như tương ứng Curry–Howard vốn đồng nhất hóa chứng minh và kiểu lại gây bối rối từ góc nhìn con người
Lỗi kiểu chỉ giống như một sai sót có thể sửa được, nhưng lỗi chứng minh thì là vấn đề phức tạp hơn nhiều và đòi hỏi suy nghĩ sâu hơn
Vì thế, tôi cho rằng điểm mạnh thực sự của Lean không phải là hệ thống kiểu mà là cộng đồng và cấu trúc mã nguồn mở của mathlib
Trong khi AFP của Isabelle vận hành giống một tạp chí học thuật, Lean lại có hợp tác dựa trên pull request rất sôi động
Hiện tôi đang phát triển một trình chứng minh định lý mới tên là Acorn(acornprover.org) và muốn kết hợp ưu điểm của Lean và Isabelle
Khả năng biểu đạt kiểu phụ thuộc đơn giản của Lean là tốt, nhưng nếu dùng quá sâu thì rất khó debug
Chỉ là không thể bảo đảm ở thời điểm biên dịch phạm vi của chỉ số chỉ được biết ở runtime
Một ngôn ngữ kiểu phụ thuộc thực thụ có thể ngăn lỗi runtime ở cấp độ kiểu
const genericscủa Rust haynon-type template parametercủa C++ thì cũng có thể làm được khá nhiềuTrên thực tế, ngay cả trong ngôn ngữ kiểu phụ thuộc, người ta cũng hiếm khi dùng kiểu phụ thuộc để ngăn lỗi runtime,
mà chủ yếu dùng cho bất biến của cấu trúc dữ liệu hoặc kiểm chứng sau khi định nghĩa chương trình
Tham khảo liên quan: division-by-zero in type theory FAQ, slide thuyết trình của Xavier Leroy
Ví dụ, như ở dòng 38 của đoạn mã này, có thể biểu diễn kích thước ma trận bằng kiểu
Tôi cũng đã hiện thực định nghĩa kiểu vector và
kiểu kết quả của phép nhân ma trận
Tuy vậy, đây mới chỉ là thử nghiệm ở mức dự án cá nhân và có thể không phù hợp với các dự án dữ liệu quy mô lớn
Điều này liên quan đến khái niệm Propositions as Types
Tôi tò mò kiểu phụ thuộc hoạt động thế nào ở runtime, và liệu có cần cả kiểm tra kiểu lúc biên dịch lẫn lúc runtime không
Tôi cũng băn khoăn liệu khi hiện thực có phát sinh độ phức tạp do quá nhiều gián tiếp tham chiếu hay không
Lập luận của Dr. Paulson không phải là kiểu phụ thuộc tệ, mà là không nhất thiết phải có
Giá như có thêm thảo luận về vấn đề hiệu năng của Lean hay các tranh luận quanh đẳng thức nội hàm (intensional equality) thì sẽ hay hơn
Trường hợp như HEq của Isabelle(liên kết), nơi không phải là đẳng thức định nghĩa, lại gây ra vấn đề
Vì vậy, tôi nghĩ nên dùng kiểu phụ thuộc ít nhất có thể
Ngay cả những hệ thống không có kiểu tĩnh như ACL2 vẫn có thể kiểm chứng đầy đủ
Sau cùng, điều quan trọng là cân bằng giữa tính thực dụng và khả năng kiểm chứng
Lean hay Agda hiện vẫn ít được dùng hơn cho kiểm chứng ở quy mô công nghiệp
So sánh Concrete Semantics(liên kết) với Logical Verification 2025(liên kết) cũng khá thú vị
Trong thực tế, refinement types có thể thực dụng hơn
Ví dụ: Rust Creusot, Dafny, ví dụ chứng minh leftpad của LiquidHaskell
Nhưng trong kiểm chứng chương trình, lại cần những bổ đề (lemma) phức tạp như “hai chứng minh là giống nhau”, và điều đó thường không thể chứng minh được
Điều quan trọng là tính năng đó hữu ích đến mức nào, chứ không phải có cần thiết cho sự tồn tại hay không
Cuối cùng, việc chọn công cụ là vấn đề của sở thích và hiệu suất làm việc của lập trình viên
Thật thú vị khi phần lớn tranh luận trong logic học hiện đại rốt cuộc lại quy về sở thích thẩm mỹ
Nếu lợi ích thực tế áp đảo thì đã chẳng có tranh cãi
Nhân tiện, bài báo năm 1999 của Paulson và Lamport “Typing in Specification Languages” rất đáng đọc
Sau đó còn có sự phát triển của chủ nghĩa hình thức phi hình thức như TLA+ của Lamport
Đổi lấy lợi ích là bảo đảm tại thời điểm biên dịch, ta phải trả giá bằng độ phức tạp và thời gian build tăng lên
Rốt cuộc, cốt lõi là “sự đánh đổi đó có đáng giá không”
Vấn đề của HOL (lý thuyết kiểu đơn giản) không nằm ở tính phụ thuộc mà là thiếu sức mạnh logic
Nó tương đương với một phiên bản bị hạn chế của lý thuyết tập hợp Zermelo, nên còn quá yếu để hình thức hóa đầy đủ toán học hiện đại
Đặc biệt khó xử lý các vấn đề về kích thước trong những lĩnh vực như lý thuyết phạm trù (category theory)
Tôi tò mò điều đó khác biệt đến đâu so với phong cách của các nhà toán học thực thụ
Ví dụ, thêm ‘inaccessible cardinal’ sẽ khiến nó trở nên gần với khái niệm ‘universe’ trong lý thuyết kiểu
Tôi từng học chuyên ngành formal methods và thấy kiểu phụ thuộc rất ngầu, nhưng khi dùng thực tế thì lúc nào cũng như leo dốc ngược
Khi dùng F#, tôi đã thử đưa F* vào, nhưng đồng nghiệp thấy ngại vì đường cong học tập mang tính toán học quá cao
Cuối cùng tôi đi đến kết luận khá bi quan rằng các kỹ sư không giỏi học công cụ có nhiều toán học
Nó dùng giải ràng buộc dựa trên SMT để cho phép dùng kiểu phụ thuộc theo kiểu nhẹ
Nhưng nó không trả lời được câu hỏi mang tính triết học như “điều này có thực sự đúng không”
Thế giới của chứng minh toán học và kiểm chứng phần mềm khác nhau khá nhiều
Suy cho cùng, thời gian là hữu hạn
Ở công ty chúng tôi là Phosphor, chúng tôi đang thử nghiệm kết hợp kiểu phụ thuộc với truy vấn cơ sở dữ liệu/đồ thị
Nhờ đó có thể khắc phục các giới hạn của RDF và xây dựng một hệ thống truy vấn dựa trên logic
Thực tế, chúng tôi đang dùng TypeDB(typedb.com); nó nhanh hơn MongoDB và hữu ích cho việc mô hình hóa dữ liệu phức tạp
Nó cũng khá giống với khái niệm ontology của Palantir
Rốt cuộc, bí quyết của kiểu phụ thuộc có lẽ là biết khi nào không nên dùng nó
Thay vì chỉ trích Lean hay Rocq, có lẽ tùy tình huống ta cũng có thể tiếp cận theo phong cách Isabelle
Dự án hình thức hóa Alexandria(liên kết) của nhóm nghiên cứu Paulson rất ấn tượng
Đặc biệt, nghiên cứu về hình thức hóa thuật toán điện toán lượng tử(liên kết bài báo) rất đáng chú ý
Trước đây tôi từng tin kiểu phụ thuộc là tương lai, nhưng trong các dự án thực tế, sự sụt giảm năng suất là rất lớn
Giờ tôi thích các giải pháp rõ ràng và dễ bảo trì hơn
Nếu cả nhóm có thể hiểu và mở rộng được công cụ đó, thì đó mới là công cụ tốt
Tôi thích những hệ thống kiểu nằm ở ranh giới của kiểu phụ thuộc hơn là kiểu phụ thuộc hoàn chỉnh
Ví dụ, Purescript mặc định hỗ trợ row-type mạnh hơn Haskell,
đồng thời còn hỗ trợ list, string, thậm chí cả regex ở cấp độ kiểu
Có thể tận dụng chúng theo kiểu lập trình logic dựa trên typeclass