Khác biệt giữa bản sửa đổi của “Lý thuyết hình thái”

MộtGiống sốnhư các lý thuyết tập hợp tiên đề, lý thuyết hình thái cóđược thểtạo đóngra vaiđể tròtránh thaynhững thếnghịch [[lý thuyếttrong tậpcác hợp]]nền đểtảng làmtrước nềnđây tảng chocủa toán học. Hainhư [[lý thuyết nhưtập vậyhợp khángây nổi tiếng là lý thuyếtthơ]], [[PhépLogic tính lambdatoán|phép tính lambdalogic hình tháithức]] của Alonzo và lý thuyết hình thái trực giác của Per Martin-Löf.

Trong khoảng thời gian từ năm 1902 đến năm 1908, [[Bertrand Russell]] đã đề xuất nhiều "lý thuyết hình thái" khác nhau để giải quyết vấn đề mà chính ông trước đó khám phá ra: rằng phiên bản [[Lý thuyết tập hợp ngây thơ|lý thuyết tập ngây thơ]] của [[Gottlob Frege]] bị ảnh hưởng bởi [[nghịch lý Russell]].

Trong phần tiếp theo, ''từ'' và ''đối tượng'' mang cùng một nghĩa; ''loại'' và ''hình thái'' mang cùng một nghĩa.

Trong một hệ hình thái, mỗi '''từ''' có một '''loại'''. Ví dụ, <math>4</math>, <math>2+2</math> và <math>2\cdot 2</math> là các từ phân biệt đều có loại <math>\mathrm{nat}</math> của các số tự nhiên. Theo truyền thống, loại của từ được viết sau dấu hai chấm, chẳng hạn như <math>2 : \mathrm{nat}</math> nghĩa là số <math>2</math> có loại <math>\mathrm{nat}</math> .

Các hệ hình thái có các phép tính tường minh được thể hiện qua các luật viết lại. Các luật viết lại này được gọi là '''quy tắc chuyển đổi''' hoặc, nếu luật chỉ hoạt động theo một chiều, '''quy tắc rút gọn'''. Ví dụ, <math>2 + 2</math> và <math>4</math> là những từ khác nhau về mặt cú pháp, nhưng từ đầu tiên có thể được rút gọn thành từ thứ hai. Phép rút gọn này được viết là <math>2 + 2 \twoheadrightarrow 4</math> .

Các hàm trong hệ hình thái có một quy tắc rút gọn đặc biệt: một biến xuất hiện trong định nghĩa hàm sẽ được thay thế bởi đối số tương ứng. Giả sử hàm <math>\mathrm{double}</math> được định nghĩa là <math>x \mapsto x+x </math>. Phép gọi hàm <math>\mathrm{double}\ 2</math> sẽ được rút gọn bằng cách thay thế <math>2</math> cho mọi <math>x</math> trong định nghĩa hàm. Như vậy ta có phép rút gọn <math>\mathrm{double}\ 2 \twoheadrightarrow 2+2</math> .

Loại hàm được ký hiệu bằng một mũi tên <math>\to</math> từ loại tham số đến loại trả về của hàm. Như vậy, ta viết <math>\mathrm{double} : \mathrm{nat} \to \mathrm{nat}</math> (tức là, <math>\mathrm{double}</math> là một ''từ'', ''loại'' của nó là <math>\mathrm{nat}\to\mathrm{nat}</math>, tức là nó là một hàm lấy vào một từ của loại các số tự nhiên, và cho ra một từ của loại các số tự nhiên).

Có nhiều lý thuyết tập hợp khác nhau và nhiều hệ thống khác nhau của lý thuyết hình thái. Tuy nhiên, ta có thể nêu ra một số nhận xét chung.

* Lý thuyết tập hợp thường mã hóa các số dưới dạng tập hợp. (0 là tập hợp rỗng, 1 là tập hợp chứa tập hợp rỗng, v.v. ) Lý thuyết hình thái có thể mã hóa các số dưới dạng các hàm, sử dụng mã hóa Church hoặc tự nhiên hơn là các hình thái quy nạp.

* Lý thuyết hình thái có quan hệ gần với toán học xây dựng thông qua diễn giải BHK . Nó có thể được kết nối với logic bởi đẳng cấu Curry Howard. Một số lý thuyết hình thái có quan hệ chặt chẽ với [[lý thuyết phạm trù]] .

Từ <math>2 + 1</math> được rút gọn về <math>3</math> . Từ <math>3</math> không thể được rút gọn hơn nữa, nó được gọi là một '''dạng chuẩn'''. Một hệ hình thái được gọi là ''chuẩn hóa mạnh'' nếu tất cả các từ đều có dạng chuẩn và bất kỳ một dãy các phép rút gọn nào đều sẽ dẫn đến dạng chuẩn. Các hệ ''chuẩn hóa yếu'' là các hệ có dạng chuẩn, tuy nhiên các phép rút gọn có thể tạo thành vòng lặp và không dẫn đến dạng chuẩn.

Đối với một hệ chuẩn hóa, một '''phần tử''' là một lớp các từ có cùng một dạng chuẩn hóa. Một '''từ đóng''' là một từ không có tham số. (Một từ như <math>x + 1</math> với tham số <math>x</math> được gọi là một '''từ mở''' . ) Như vậy, <math>2 + 1</math> và <math>3 + 0</math> là hai từ khác nhau của phần tử <math>3</math> .

Một '''loại phụ thuộc''' là một loại mà phụ thuộc vào một từ hoặc loại khác. Ví dụ, loại trả về của một hàm có thể phụ thuộc vào đối số đưa vào hàm.

Ví dụ, một danh sách <math>\mathrm{nat}</math> s có độ dài 4 có thể có loại khác với một danh sách <math>\mathrm{nat}</math> s có độ dài 5.

Nhiều hệ hình thái có một loại đại diện cho ''sự bằng nhau'' của các loại và các từ. Loại này khác với quy tắc chuyển đổi, và được gọi là ''đẳng thức mệnh đề''.

Trong lý thuyết hình thái trực giác, loại đẳng thức được gọi là <math>I</math>. Có một loại <math>I\ A\ a\ b</math> với <math>A</math> là một loại và <math>a</math>, <math>b</math> là các từ có loại <math>A</math> . Một từ của loại <math>I\ A\ a\ b</math> là một đẳng thức "<math>a</math> bằng <math>b</math>".

Trong thực tế, có thể xây dựng một loại <math>I\ \mathrm{nat}\ 3\ 4</math> nhưng loại đó sẽ không có từ nào cả (vì <math>3</math> khác <math>4</math>). Trong lý thuyết loại trực giác, ta xây dựng các từ đẳng thức bắt đầu từ các đẳng thức đồng nhất. Nếu <math>3</math> là một từ loại <math>\mathrm{nat}</math>, tồn tại một từ với loại <math>I\ \mathrm{nat}\ 3\ 3</math> . Các đẳng thức phức tạp hơn có thể được tạo ra bằng cách tạo ra một từ đồng nhất rồi thực hiện rút gọn một bên. Ví dụ, nếu <math>2+1</math> là một từ loại <math>\mathrm{nat}</math>, ta có một đẳng thức đồng nhất <math>I\ \mathrm{nat}\ (2+1)\ (2+1)</math>, và bằng cách rút gọn, ta có một từ mới loại <math>I\ \mathrm{nat}\ (2+1)\ 3</math> . Do đó, trong hệ này, loại đẳng thức thể hiện rằng hai giá trị cùng loại có thể được chuyển đổi bằng phép rút gọn.

* Phép tính xây dựng và các dẫn xuất

* Automath ;

* Lý thuyết hình thái ST ;

* Cardelli, Luca (1996). "Type Systems". In Tucker, Allen B. (ed.). ''The Computer Science and Engineering Handbook''. CRC Press. pp. &nbsp;2208–36. ISBN <bdi>9780849329098</bdi>..

* Constable, Robert L. (2012) [2002]. "Naïve Computational Type Theory" ([http://www.nuprl.org/documents/Constable/naive.pdf PDF]). In Schwichtenberg, H.; Steinbruggen, R. (eds.). ''Proof and System-Reliability''. Nato Science Series II. '''62'''. Springer. pp. &nbsp;213–259. ISBN <bdi>9789401004138</bdi>.