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

(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$