Nền tảng toán học

Lý thuyết kiểu

Một nền tảng cho toán học và tính toán trong đó mỗi hạng đều mang một kiểu, dùng trong các trợ lý chứng minh.

Trực giácMọi giá trị đều có nhãn

Trong hầu hết ngôn ngữ lập trình, $3$ là `int` và `"hello"` là `string` — trình biên dịch từ chối `3 + "hello"` trước khi chương trình chạy. Lý thuyết kiểu biến ý tưởng thường ngày này thành một nền tảng cho toàn bộ toán học: thay vì bắt đầu từ tập hợp và quan hệ thuộc ( $x \in A$ ), bắt đầu từ hạng và kiểu ( $t : A$ , " $t$ có kiểu $A$ "). Đáng chú ý, khi kiểu đủ phong phú, một kiểu có thể mã hóa một mệnh đề toán học, và một hạng của kiểu đó trở thành một chứng minh — chương trình và chứng minh trở thành cùng một loại đối tượng.

Một dẫn xuất kiểu dưới dạng cây: mỗi đỉnh là một phán đoán

\Gamma \vdash t : A

, mỗi cạnh là một quy tắc kiểu nối hạng với các hạng con.

Đại họcPhép tính lambda đơn định kiểu

Định nghĩa: Phán đoán kiểu

Một phán đoán kiểu $\Gamma \vdash t : A$ nói "trong ngữ cảnh $\Gamma$ (danh sách cặp biến-kiểu $x_1:A_1,\dots,x_n:A_n$ ), hạng $t$ có kiểu $A$ ". Các quy tắc cốt lõi: một biến có kiểu mà ngữ cảnh gán cho nó; một trừu tượng hóa $\lambda x{:}A.\,t$ có kiểu $A\to B$ bất cứ khi nào $t$ có kiểu $B$ trong ngữ cảnh mở rộng bởi $x:A$ ; và áp dụng $f\,u$ có kiểu $B$ bất cứ khi nào $f:A\to B$ và $u:A$ .

\dfrac{\Gamma, x{:}A \vdash t : B}{\Gamma \vdash \lambda x{:}A.\,t : A\to B} \qquad \dfrac{\Gamma \vdash f : A\to B \quad \Gamma \vdash u : A}{\Gamma \vdash f\,u : B}

Lý thuyết kiểu phụ thuộc Martin-Löf tổng quát hóa điều này xa hơn: kiểu kết quả của một hàm có thể phụ thuộc vào giá trị của đối số nó. **Kiểu $\Pi$ ** (kiểu hàm phụ thuộc) $\prod_{x:A} B(x)$ gom các hàm gửi mỗi $x:A$ tới một hạng kiểu $B(x)$ — khi $B$ không nhắc tới $x$ , nó suy biến thành $A\to B$ thông thường. Đối ngẫu, **kiểu $\Sigma$ ** (kiểu cặp phụ thuộc) $\sum_{x:A} B(x)$ gom các cặp $\langle a,b\rangle$ với $a:A$ và $b:B(a)$ — một cặp mà kiểu thành phần thứ hai phụ thuộc vào thành phần thứ nhất; khi $B$ không nhắc tới $x$ , nó suy biến thành tích $A\times B$ thông thường.

\prod_{x:A} B(x), \qquad \sum_{x:A} B(x)

Kiểu phụ thuộc và cách đọc Curry–Howard
Kiến trúc kiểu	Trường hợp riêng không phụ thuộc	Cách đọc Curry–Howard
$\prod_{x:A} B(x)$	$A\to B$ (khi $B$ hằng)	$\forall x{:}A,\ B(x)$
$\sum_{x:A} B(x)$	$A\times B$ (khi $B$ hằng)	$\exists x{:}A,\ B(x)$
Tiên đề đơn trị: $(A\simeq B) \simeq (A =_{\mathcal U} B)$	—	Các kiểu tương đương được đồng nhất

Định lý: Định lý chuẩn hóa mạnh cho phép tính lambda đơn định kiểu

Nếu $\Gamma \vdash t : A$ trong phép tính lambda đơn định kiểu, thì $t$ là chuẩn hóa mạnh: mọi dãy thu gọn $\beta$ bắt đầu từ $t$ đều kết thúc sau hữu hạn bước.

Vì sao đúng?

Đây là lý do vì sao phép tính lambda đơn định kiểu, dù có áp dụng hàm và lồng kiểu đệ quy, không đầy đủ Turing — không hạng được định kiểu nào có thể chạy mãi, chính điều này làm trình kiểm tra kiểu trong mảnh này luôn dừng.

Chứng minh

(Phương pháp khả quy Tait.) Định nghĩa, bằng quy nạp theo cấu trúc kiểu, một tập $\mathrm{RED}_A$ các "hạng khả quy" cho mỗi kiểu $A$ : với kiểu cơ sở $o$ , đặt $\mathrm{RED}_o$ là tập $SN$ gồm mọi hạng chuẩn hóa mạnh; với kiểu hàm, đặt $\mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\}$ .

Trước hết ta chứng minh, bằng quy nạp theo $A$ , ba tính chất kỹ thuật cùng lúc: (CR1) mọi hạng trong $\mathrm{RED}_A$ đều chuẩn hóa mạnh; (CR2) $\mathrm{RED}_A$ đóng dưới thu gọn $\beta$ (nếu $t\in\mathrm{RED}_A$ và $t\to t'$ thì $t'\in\mathrm{RED}_A$ ); (CR3) mọi hạng "trung tính" (một biến hay áp dụng, không phải trừu tượng hóa) mà mọi thu gọn một bước của nó đã nằm trong $\mathrm{RED}_A$ thì chính nó cũng nằm trong $\mathrm{RED}_A$ . Trường hợp cơ sở hiển nhiên từ định nghĩa $SN$ ; trường hợp kiểu hàm khai triển định nghĩa $\mathrm{RED}_{A\to B}$ và dùng giả thiết quy nạp trên các kiểu nhỏ hơn $A$ và $B$ .

Tiếp theo, ta chỉ ra mọi hạng được định kiểu đều khả quy dưới bất kỳ phép thế nào của các hạng khả quy cho biến tự do của nó: bằng quy nạp theo dẫn xuất kiểu của $\Gamma \vdash t:A$ , nếu $\sigma$ gán mỗi biến $x$ trong $\Gamma$ một hạng $\sigma(x)\in\mathrm{RED}_{\Gamma(x)}$ , thì $t\sigma \in \mathrm{RED}_A$ . Trường hợp biến hiển nhiên. Trường hợp áp dụng theo trực tiếp từ định nghĩa $\mathrm{RED}_{A\to B}$ . Trường hợp trừu tượng hóa cần cẩn thận nhất: với $(\lambda x.\,t)\sigma$ áp lên $u\in\mathrm{RED}_A$ bất kỳ, hạng thu gọn trong một bước $\beta$ về $t(\sigma,x{:=}u)$ , nằm trong $\mathrm{RED}_B$ theo giả thiết quy nạp (áp cho phép thế mở rộng); tính chất (CR3) — đóng dưới "mở rộng" cho các hạng mà mọi thu gọn đã khả quy — khi đó đặt chính $(\lambda x.\,t)\sigma\,u$ vào $\mathrm{RED}_B$ , nên $(\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B}$ theo định nghĩa.

Cuối cùng, áp dụng điều này cho phép thế đồng nhất: mỗi biến $x{:}A$ tự nó trung tính và không có thu gọn nào cả, nên nó nằm trong $\mathrm{RED}_A$ một cách hiển nhiên theo (CR3). Vậy với mọi dẫn xuất đóng $\Gamma \vdash t:A$ , lấy $\sigma$ gửi mỗi $x$ tới chính nó cho $t = t\sigma \in \mathrm{RED}_A$ . Theo (CR1), $\mathrm{RED}_A \subseteq SN$ , nên $t \in SN$ : mọi hạng được định kiểu đều chuẩn hóa mạnh. $\blacksquare$

Nâng caoSự tương ứng Curry–Howard

Đọc $A\to B$ là "nếu $A$ thì $B$ ", đọc $A\times B$ là " $A$ và $B$ ", và một chứng minh của một mệnh đề trở thành một chương trình được định kiểu đúng với kiểu tương ứng — đây là mệnh đề-là-kiểu, chứng minh-là-chương trình. Kiểm tra chứng minh quy về kiểm tra kiểu của một hạng; xây chứng minh quy về viết chương trình đúng kiểu.

Định lý: Sự tương ứng Curry–Howard

Cho $\varphi$ là công thức mệnh đề xây từ nguyên tử, $\wedge$ , và $\to$ , và cho $A_\varphi$ là kiểu đơn thu được bằng cách dịch nguyên tử thành kiểu cơ sở, $\wedge$ thành tích $\times$ , và $\to$ thành kiểu hàm $\to$ . Khi đó $\varphi$ chứng minh được trong logic mệnh đề trực giác khi và chỉ khi $A_\varphi$ có cư dân: tồn tại một hạng đóng $t$ với $\vdash t : A_\varphi$ .

Vì sao đúng?

Đây là phát biểu chính xác đằng sau câu "trợ lý chứng minh chỉ là một trình kiểm tra kiểu": Coq, Agda, và Lean chấp nhận một chứng minh được máy kiểm tra của một định lý đúng khi chúng chấp nhận một hạng của kiểu tương ứng, và kiểm tra kiểu (khác với chứng minh định lý nói chung) là một thuật toán nhỏ, nhanh, máy móc, và rất đáng tin cậy.

Chứng minh

(Chứng minh trở thành chương trình.) Bằng quy nạp theo dẫn xuất suy luận tự nhiên của $\vdash \varphi$ . Nếu quy tắc cuối là dẫn nhập $\to$ , dẫn $\varphi=\psi\to\chi$ từ một chứng minh con của $\chi$ dưới giả thiết $\psi$ : theo giả thiết quy nạp chứng minh con đó dịch thành hạng $t$ với $x{:}A_\psi \vdash t : A_\chi$ (giả thiết trở thành biến tự do $x$ ); khi đó $\lambda x{:}A_\psi.\,t$ đóng và có kiểu $A_\psi\to A_\chi=A_\varphi$ . Nếu quy tắc cuối là loại bỏ $\to$ (modus ponens) từ $\psi\to\chi$ và $\psi$ : theo giả thiết quy nạp ta có các hạng $t_1 : A_\psi\to A_\chi$ và $t_2 : A_\psi$ ; khi đó $t_1\,t_2 : A_\chi$ . Các quy tắc dẫn nhập $\wedge$ và loại bỏ $\wedge$ dịch đối xứng thành ghép cặp $\langle t_1,t_2\rangle$ và hai phép chiếu. Mọi quy tắc của hệ chứng minh đều có quy tắc xây hạng tương ứng, nên quy nạp theo dẫn xuất cho ra một hạng đóng được định kiểu thuộc kiểu $A_\varphi$ .

(Chương trình trở thành chứng minh.) Ngược lại, bằng quy nạp theo dẫn xuất kiểu $\vdash t : A$ . Mỗi quy tắc kiểu — biến, trừu tượng hóa, áp dụng, ghép cặp, phép chiếu — có đúng hình dạng cây như một quy tắc suy luận tự nhiên — giả thiết, dẫn nhập $\to$ , loại bỏ $\to$ , dẫn nhập $\wedge$ , loại bỏ $\wedge$ . Vậy lấy cùng cây dẫn xuất, xóa mọi hạng, và đọc mỗi kiểu như công thức nó dịch từ: đây chính xác là một chứng minh trực giác hợp lệ của $\varphi$ (với $A=A_\varphi$ ).

Vì hai phép dịch (chứng minh $\to$ hạng, và hạng $\to$ chứng minh) là nghịch đảo cấu trúc của nhau trên các cây dẫn xuất — mỗi phép hoàn tác chính xác điều phép kia làm, quy tắc theo quy tắc — $\varphi$ chứng minh được đúng khi $A_\varphi$ có cư dân. $\blacksquare$

Đại họcỨng dụng thực tiễn và Ví dụ minh họa

Hệ kiểu phong phú bắt được cả lớp lỗi trước khi chương trình chạy: kiểu sở hữu của Rust ngăn dùng-sau-giải-phóng và tranh chấp dữ liệu ngay lúc biên dịch, và ngôn ngữ định kiểu phụ thuộc có thể mã hóa bất biến như "danh sách này có đúng $n$ phần tử" hay "chỉ số này trong khoảng hợp lệ" trực tiếp vào kiểu, khiến một số lỗi runtime không thể biểu diễn được. Ứng dụng sâu nhất nằm chính trong trợ lý chứng minh: Coq, Agda, và Lean có lõi nhỏ, được kiểm toán cẩn thận, chỉ làm mỗi việc kiểm tra kiểu hạng — vì sự tương ứng Curry–Howard, chấp nhận một hạng thuộc kiểu của một định lý chính là chấp nhận một chứng minh được máy kiểm tra, nên tin một kết quả toán học cỡ định lý Feit–Thompson hay định lý bốn màu quy về tin vài trăm dòng mã kiểm tra kiểu, không phải các chiến thuật (lớn hơn, khó kiểm toán hơn nhiều) đã xây nên hạng chứng minh.

Ví dụ: Một kiểu $\Pi$ mà kiểu hàm thường không diễn đạt được

Cho $\mathrm{Vec}\,A\,n$ là kiểu danh sách độ dài $n$ gồm phần tử kiểu $A$ . Viết một hạng cư trú $\prod_{n:\mathbb N} (\mathrm{Vec}\,A\,n \to \mathrm{Vec}\,A\,n)$ — "với mọi độ dài $n$ , một hàm trên vector độ dài $n$ " — và giải thích vì sao kiểu đơn (không có $\Pi$ ) hoàn toàn không diễn đạt được đặc tả này.

Lời giải

Hạng $\lambda n{:}\mathbb N.\,\lambda v{:}\mathrm{Vec}\,A\,n.\,v$ hoạt động: với mỗi số tự nhiên $n$ , nó nhận một vector độ dài $n$ là $v$ và trả về nguyên vẹn — rõ ràng được định kiểu tốt, vì $v : \mathrm{Vec}\,A\,n$ được trả về ở kiểu $\mathrm{Vec}\,A\,n$ , với bất kỳ $n$ nào được cung cấp.

Điều làm đây là một sử dụng thật sự của $\Pi$ thay vì kiểu hàm thường là kiểu của đối số thứ hai ( $\mathrm{Vec}\,A\,n$ ) nhắc tới giá trị của đối số thứ nhất ( $n$ ). Trong phép tính lambda đơn định kiểu, kiểu đối số và kết quả của một hàm được cố định một lần cho mãi mãi — $A\to B$ với $A,B$ chọn trước khi biết giá trị nào của kiểu $A$ . Không có cách nào viết "cho tôi số tự nhiên $n$ , và tùy vào số bạn cho, tôi sẽ đòi một vector đúng độ dài đó" chỉ dùng $\to$ : bạn cần một kiểu cố định duy nhất $\mathrm{Vec}\,A\,n$ nào đó hoạt động cho mọi $n$ cùng lúc, không phải điều $\mathrm{Vec}$ có nghĩa.

Cụ thể, nếu bạn thử viết điều này bằng kiểu hàm thường, tốt nhất bạn được $\mathbb N \to (\mathrm{Vec}\,A\,? \to \mathrm{Vec}\,A\,?)$ với một độ dài giữ chỗ CỐ ĐỊNH — vô dụng, vì nó sẽ từ chối vector độ dài khác, hoặc chấp nhận vector sai độ dài. Kiểu $\Pi$ , $\prod_{n:\mathbb N}(\cdots)$ , chính xác là kiến trúc kiểu cho phép miền đích "nhìn lại" giá trị cụ thể của $n$ nhận được, đúng là sự phụ thuộc mà kiểu đơn không diễn đạt được.

Ví dụ: Curry–Howard cho phép hợp thành hàm

Công thức $(A\to B)\to((B\to C)\to(A\to C))$ diễn đạt tính bắc cầu của kéo theo. Theo Curry–Howard, tìm hạng $\lambda$ chứng minh nó, và kiểm tra dẫn xuất kiểu từng bước.

Lời giải

Hạng là $t = \lambda f{:}A\to B.\,\lambda g{:}B\to C.\,\lambda x{:}A.\,g\,(f\,x)$ — chính xác là hợp thành hàm $g\circ f$ áp lên $x$ .

Dẫn xuất kiểu từ trong ra ngoài. Trong ngữ cảnh $f{:}A\to B,\,g{:}B\to C,\,x{:}A$ : vì $f:A\to B$ và $x:A$ , áp dụng cho $f\,x:B$ . Vì $g:B\to C$ và $f\,x:B$ , áp dụng cho $g\,(f\,x):C$ .

Giờ giải phóng các trừu tượng hóa từ trong ra ngoài. $\lambda x{:}A.\,g\,(f\,x)$ có kiểu $A\to C$ trong ngữ cảnh $f{:}A\to B,\,g{:}B\to C$ . Rồi $\lambda g{:}B\to C.\,(\cdots)$ có kiểu $(B\to C)\to(A\to C)$ trong ngữ cảnh $f{:}A\to B$ . Cuối cùng $\lambda f{:}A\to B.\,(\cdots)$ có kiểu $(A\to B)\to((B\to C)\to(A\to C))$ không còn giả thiết tự do nào — một hạng đóng.

Vậy $\vdash t : (A\to B)\to((B\to C)\to(A\to C))$ , nghĩa là $t$ là một chứng minh Curry–Howard của tính bắc cầu: "nếu $A$ kéo theo $B$ , và $B$ kéo theo $C$ , thì $A$ kéo theo $C$ " — cùng hạng mà một lập trình viên hàm sẽ viết để hợp thành hai hàm.

Lỗi hay gặp. Đừng nhầm

\Pi_{x:A}B(x)

và

\Sigma_{x:A}B(x)

với những lượng từ đơn thuần gắn vào một vũ trụ tập hợp đã có sẵn — chúng là các phép toán tạo kiểu mới, và trường hợp riêng không phụ thuộc của chúng (

\Pi\to

kiểu hàm thường,

\Sigma\to

tích thường) chính là điều nên khiến bạn nghi ngờ nếu một lập luận "kiểu phụ thuộc" thực ra chưa bao giờ dùng tới sự phụ thuộc. Một nhầm lẫn phổ biến thứ hai: Tiên đề đơn trị

(A\simeq B)\simeq(A=_{\mathcal U}B)

nói về đẳng thức mệnh đề

=_{\mathcal U}

của các kiểu (một đường đi/đồng nhất hóa có thể tính toán được), không phải đẳng thức định nghĩa (phán đoán) chặt hơn nhiều mà trình kiểm tra kiểu dùng tự động — tiên đề đơn trị cần được viện dẫn, nó không tự có từ riêng các quy tắc kiểu.

Ghi chú lịch sử

Alonzo Church giới thiệu kiểu đơn năm 1940 để tránh nghịch lý của phép tính lambda không định kiểu. "Phép diễn dịch Dialectica" năm 1958 của Kurt Gödel dùng một phép tính định kiểu các hàm tử đệ quy nguyên thủy — tổ tiên trực tiếp của các diễn dịch chứng minh định kiểu — để đưa ra chứng minh nhất quán kiến thiết cho số học. Năm 1972, Per Martin-Löf công bố lý thuyết kiểu phụ thuộc của ông, hợp nhất logic và tính toán bằng kiểu $\Pi$ và $\Sigma$ . Quan sát rằng chương trình định kiểu và chứng minh logic là cùng một đối tượng thường được ghi công cho Haskell Curry (1958) và William Howard (viết 1969, công bố 1980), cho sự tương ứng cái tên của nó. Năm 2013, "Sách HoTT" của Chương trình Nền tảng Đơn trị, theo sau Tiên đề đơn trị của Vladimir Voevodsky, đề xuất Lý thuyết kiểu Đồng luân như một nền tảng ứng viên mới cho toán học.

Kurt Gödel

Nghiên cứuNghiên cứu hiện nay

Hiện trạng nghiên cứu tính đến năm 2026

Lý thuyết kiểu Đồng luân và chương trình Nền tảng Đơn trị của Voevodsky tiếp tục được phát triển như một nền tảng ứng viên cho toán học song song với (chưa thay thế) lý thuyết tập hợp ZFC, với lý thuyết kiểu lập phương (từ khoảng 2015 trở đi) mang lại nội dung tính toán thực sự cho Tiên đề đơn trị — một bài toán mở lâu năm — bằng cách xây đẳng thức của các kiểu trực tiếp từ một kiểu khoảng, và cách trình bày tính toán này vẫn đang được tinh chỉnh và mở rộng tới các kiến trúc kiểu phong phú hơn tính đến 2026. Các nỗ lực hình thức hóa quy mô lớn đang chứng minh sức mạnh của lý thuyết kiểu như hạ tầng toán học làm việc: thư viện `mathlib` dựa trên Lean đã lớn thành một trong các khối toán học hình thức hóa lớn nhất, "Thí nghiệm Tensor Lỏng" 2020–2022 của Peter Scholze và Dustin Clausen đã kiểm chứng hình thức một định lý khó trong toán học ngưng tụ bằng Lean, và các nỗ lực cộng đồng (bao gồm một nỗ lực do Kevin Buzzard dẫn dắt) hướng tới hình thức hóa đầy đủ Định lý lớn Fermat vẫn hoạt động tính đến giữa thập niên 2020. Riêng biệt, nghiên cứu tiếp tục về kiểu quy nạp cao cấp và lý thuyết đồng luân tổng hợp (tính nhóm đồng luân của mặt cầu trực tiếp trong lý thuyết kiểu) và về tăng cường lý thuyết kiểu phụ thuộc để hỗ trợ nhiều hơn thực hành toán học thông thường mà không hy sinh tính kiểm tra kiểu quyết định được.

Trong phép tính lambda đơn định kiểu, nếu $f : A \to B$ và $a : A$ , kiểu của $f\,a$ là gì?

Vì sao một trợ lý chứng minh như Coq, Agda, hay Lean có thể tin một chứng minh được máy kiểm tra dài hàng nghìn dòng?

Khi $B(x)$ thực ra không phụ thuộc $x$ , $\prod_{x:A} B(x)$ suy biến thành gì?

Tiên đề đơn trị $(A\simeq B) \simeq (A =_{\mathcal U} B)$ nói rằng...

Tài liệu tham khảo

The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics
Wikipedia contributors (2024). Curry–Howard correspondence
Wikipedia contributors (2024). Intuitionistic type theory