Bản mẫu:Chuyên ngànhTrong toán học, logic và khoa học máy tính, một lý thuyết hình thái hoặc một hệ hình thái là một hệ thống hình thức trong đó mọi đối tượng đều có một hình thái (hay mọi biến đều có một kiểu, mọi từ đều có một loại,…). Hình thái của một đối tượng hạn chế các tác động (hay phép toán, cách dùng) có thể được thực hiện trên đối tượng (hay biến, từ) ấy. Ngành nghiên cứu các hệ hình thái cũng được gọi là Lý thuyết Hình Thái.
Một số triết lý hình thái hoàn toàn có thể đóng vai trò sửa chữa thay thế triết lý tập hợp để làm nền tảng cho toán học. Hai triết lý như vậy khá nổi tiếng là triết lý phép tính lambda hình thái của Alonzo và triết lý hình thái trực giác của Per Martin-Löf .Giống như những triết lý tập hợp tiên đề, triết lý hình thái được tạo ra để tránh những nghịch lý trong những nền tảng trước kia của toán học như triết lý tập hợp ngây thơ, logic hình thức .
Lý thuyết hình thái có quan hệ chặt chẽ với, và đôi khi trùng lặp với, hệ thống kiểu trong khoa học máy tính.
Trong khoảng chừng thời hạn từ năm 1902 đến năm 1908, Bertrand Russell đã yêu cầu nhiều ” triết lý hình thái ” khác nhau để xử lý yếu tố mà chính ông trước đó mày mò ra : rằng phiên bản kim chỉ nan tập ngây thơ của Gottlob Frege bị ảnh hưởng tác động bởi nghịch lý Russell .
Các khái niệm cơ bản[sửa|sửa mã nguồn]
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ụ,
4
{displaystyle 4}
2
+
2
{displaystyle 2+2}
2
⋅
2
{displaystyle 2cdot 2}
n
a
t
{displaystyle mathrm {nat} }
2
:
n
a
t
{displaystyle 2:mathrm {nat} }
2
{displaystyle 2}
n
a
t
{displaystyle mathrm {nat} }
.
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ụ,
2
+
2
{displaystyle 2+2}
và
4
{displaystyle 4}
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à
2
+
2
↠
4
{displaystyle 2+2twoheadrightarrow 4}
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
d
o
u
b
l
e
{displaystyle mathrm {double} }
x
↦
x
+
x
{displaystyle xmapsto x+x}
d
o
u
b
l
e
2
{displaystyle mathrm {double} 2}
2
{displaystyle 2}
cho mọi
x
{displaystyle x}
d
o
u
b
l
e
2
↠
2
+
2
{displaystyle mathrm {double} 2twoheadrightarrow 2+2}
Loại hàm được ký hiệu bằng một mũi tên
→
{displaystyle to }
d
o
u
b
l
e
:
n
a
t
→
n
a
t
{displaystyle mathrm {double} :mathrm {nat} to mathrm {nat} }
d
o
u
b
l
e
{displaystyle mathrm {double} }
là một từ, loại của nó là
n
a
t
→
n
a
t
{displaystyle mathrm {nat} to mathrm {nat} }
Khác biệt với kim chỉ nan tập hợp[sửa|sửa mã nguồn]
Có nhiều triết lý tập hợp khác nhau và nhiều mạng lưới hệ thống khác nhau của kim chỉ nan hình thái. Tuy nhiên, ta hoàn toàn có thể nêu ra 1 số ít nhận xét chung .
- Lý thuyết tập hợp được xây dựng trên nền tảng logic. Nó đòi hỏi một hệ thống riêng như logic vị từ bên dưới nó. Trong lý thuyết hình thái, các khái niệm như “và” và “hoặc” có thể được mã hóa thành các hình thái. Tức là, lý thuyết hình thái có thể làm nền tảng cho logic.
- Trong lý thuyết tập hợp, một phần tử có thể là phần tử của nhiều tập hợp. Trong lý thuyết hình thái, mỗi đối tượng chỉ thuộc về một hình thái.
- 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ính chất khác[sửa|sửa mã nguồn]
Từ
2
+
1
{displaystyle 2+1}
3
{displaystyle 3}
3
{displaystyle 3}
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ư
x
+
1
{displaystyle x+1}
x
{displaystyle x}
được gọi là một từ mở.) Như vậy,
2
+
1
{displaystyle 2+1}
và
3
+
0
{displaystyle 3+0}
3
{displaystyle 3}
.
Các loại nhờ vào[sửa|sửa mã nguồn]
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 list n a t { displaystyle mathrm { nat } } s có độ dài 4 hoàn toàn có thể có loại khác với một list n a t { displaystyle mathrm { nat } } s có độ dài 5 .
Các loại đẳng thức[sửa|sửa mã nguồn]
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à
I
{displaystyle I}
I
A
a
b
{displaystyle I A a b}
A
{displaystyle A}
a
{displaystyle a}
b
{displaystyle b}
A
{displaystyle A}
. Một từ của loại
I
A
a
b
{displaystyle I A a b}
là một đẳng thức ”
a
{displaystyle a}
bằng
b
{displaystyle b}
“.
Trong thực tế, có thể xây dựng một loại
I
n
a
t
3
4
{displaystyle I mathrm {nat} 3 4}
3
{displaystyle 3}
khác
4
{displaystyle 4}
). 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
3
{displaystyle 3}
là một từ loại
n
a
t
{displaystyle mathrm {nat} }
, tồn tại một từ với loại
I
n
a
t
3
3
{displaystyle I mathrm {nat} 3 3}
2
+
1
{displaystyle 2+1}
là một từ loại
n
a
t
{displaystyle mathrm {nat} }
, ta có một đẳng thức đồng nhất
I
n
a
t
(
2
+
1
)
(
2
+
1
)
{displaystyle I mathrm {nat} (2+1) (2+1)}
I
n
a
t
(
2
+
1
)
3
{displaystyle I mathrm {nat} (2+1) 3}
Các kim chỉ nan hình thái[sửa|sửa mã nguồn]
- Phép tính lambda hình thái đơn, là một logic bậc cao;
- Lý thuyết hình thái trực giác;
- Hệ F;
- Phép tính xây dựng và các dẫn xuất
- Automath;
- Lý thuyết hình thái ST;
Hiện đang được điều tra và nghiên cứu[sửa|sửa mã nguồn]
- Lý thuyết hình thái đồng luân đang được nghiên cứu.
- Bell, John L. (2012). “Types, Sets and Categories” (PDF). In Kanamory, Akihiro (ed.). Sets and Extensions in the Twentieth Century (PDF). Handbook of the History of Logic. 6. Elsevier.
- Church, Alonzo (1940). “A formulation of the simple theory of types”. The Journal of Symbolic Logic. 5 (2): 56–68. JSTOR 2266170.
- Farmer, William M. (2008). “The seven virtues of simple type theory”. Journal of Applied Logic. 6 (3): 267–286.
- Aarts, C.; Backhouse, R.; Hoogendijk, P.; Voermans, E.; van der Woude, J. (December 1992). “A Relational Theory of Datatypes”. Technische Universiteit Eindhoven.
- Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Kluwer. ISBN 978-1-4020-0763-7.
- Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
- Cardelli, Luca (1996). “Type Systems”. In Tucker, Allen B. (ed.). The Computer Science and Engineering Handbook. CRC Press. pp. 2208–36. ISBN 9780849329098..
- Constable, Robert L. (2012) [2002]. “Naïve Computational Type Theory” (PDF Lưu trữ 2012-02-27 tại Wayback Machine). In Schwichtenberg, H.; Steinbruggen, R. (eds.). Proof and System-Reliability. Nato Science Series II. 62. Springer. pp. 213–259. ISBN 9789401004138.
- Coquand, Thierry (2018) [2006]. “Type Theory”. Stanford Encyclopedia of Philosophy.
- Thompson, Simon (1991). Type Theory and Functional Programming. Addison–Wesley.
- Hindley, J. Roger (2008) [1995]. Basic Simple Type Theory. Cambridge University Press.
- Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). A modern perspective on type theory: from its origins until today. Springer.
- Ferreirós, José; Domínguez, José Ferreirós (2007). “X. Logic and Type Theory in the Interwar Period”. Labyrinth of thought: a history of set theory and its role in modern mathematics (2nd ed.). Springer.
- Laan, T.D.L. (1997). The evolution of type theory in logic and mathematics (PDF) (PhD). Eindhoven University of Technology.
