Khái niệm hình thái học

Trong các lĩnh vực toán học, logic và khoa học máy tính, một hệ hình thái hay còn gọi là lý thuyết hình thái là một hệ thống hình thức trong đó mỗi đối tượng có một hình thái (hoặc mỗi biến có một kiểu, mỗi từ có một loại,...). Hình thái của một đối tượng xác định các tác động (hoặc phép toán, cách sử dụng) có thể thực hiện trên đối tượng đó (hoặc biến, từ). 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ố lý thuyết hình thái có thể thay thế lý thuyết tập hợp như nền tảng của toán học. Hai ví dụ nổi bật là lý thuyết phép tính lambda của Alonzo và lý thuyết hình thái trực giác của Per Martin-Löf.

Tương tự như các lý thuyết tập hợp tiên đề, lý thuyết hình thái được phát triển nhằm tránh các nghịch lý trong các nền tảng toán học trước đây như lý thuyết tập hợp ngây thơ và logic hình thức.

Lý thuyết hình thái có mối liên hệ mật thiết với, và đôi khi trùng lặp với, các hệ thống kiểu trong khoa học máy tính.

Quá trình phát triển

Từ năm 1902 đến 1908, Bertrand Russell đã đề xuất nhiều 'hệ hình thái' khác nhau để giải quyết vấn đề mà ông đã phát hiện ra trước đó: phiên bản lý thuyết tập ngây thơ của Gottlob Frege bị ảnh hưởng bởi nghịch lý Russell.

Khái niệm cơ bản

Trong phần tiếp theo, từ và đối tượng được sử dụng thay thế cho nhau; loại và hình thái cũng có ý nghĩa tương tự.

Trong một hệ hình thái, mỗi từ có một loại. Ví dụ, các từ $4$, $2+2$ và $2\cdot <!--\; \cdot \; -->2$ đều là các từ phân biệt có cùng loại $nat$ của các số tự nhiên. Theo truyền thống, loại của từ được ghi sau dấu hai chấm, chẳng hạn như $2:nat$ cho thấy số $2$ thuộc loại $nat$.

Trong các hệ hình thái, các phép toán được biểu diễn qua các quy tắc viết lại. Những quy tắc này được gọi là quy tắc chuyển đổi, hoặc nếu chúng chỉ hoạt động theo một chiều, thì được gọi là quy tắc rút gọn. Ví dụ, $2+2$ và $4$ là các từ cú pháp khác nhau, 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\twoheadrightarrow <!--\; \twoheadrightarrow \; -->4$.

Các hàm trong hệ hình thái có quy tắc rút gọn riêng: biến xuất hiện trong định nghĩa hàm sẽ được thay thế bằng đối số tương ứng. Ví dụ, hàm $double$ được định nghĩa là $x\mapsto <!--\; \mapsto \; -->x+x$. Khi gọi hàm $double2$, ta thay thế $2$ bằng mọi $x$ trong định nghĩa hàm. Kết quả là $double\text{ <div class="min-w-[250px] max-w-[94vw] md:max-w-[770px]"> <ins class="adsbygoogle" style="display:block; text-align:center;" data-ad-layout="in-article" data-ad-format="fluid" data-ad-client="ca-pub-9247024304160346" data-ad-slot="4115752014"></ins> </div>}2\twoheadrightarrow <!--\; \twoheadrightarrow \; -->2+2$.

Hàm được ký hiệu bằng một mũi tên $\to <!--\; \to \; -->$ từ loại tham số đến loại trả về của nó. Ví dụ, ta viết $double:nat\to <!--\; \to \; -->nat$ (tức là, $double$ là một hàm nhận vào một từ loại số tự nhiên và trả về một từ cũng thuộc loại số tự nhiên).

So sánh với lý thuyết tập hợp

Mặc dù có nhiều lý thuyết tập hợp và hệ thống lý thuyết hình thái khác nhau, nhưng có thể đưa ra một số điểm so sánh chung.

• Lý thuyết tập hợp được xây dựng dựa trên nền tảng của logic và cần một hệ thống logic vị từ để hỗ trợ. Ngược lại, 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, do đó 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ể thuộc nhiều tập hợp khác nhau. Tuy nhiên, trong lý thuyết hình thái, mỗi đối tượng chỉ thuộc về một hình thái duy nhất.
• Lý thuyết tập hợp thường biểu diễn các số bằng các tập hợp (ví dụ, 0 là tập hợp rỗng, 1 là tập hợp chứa tập hợp rỗng, v.v.). Trong lý thuyết hình thái, các số có thể được mã hóa dưới dạng các hàm, thông qua mã hóa Church hoặc các hình thái quy nạp một cách tự nhiên hơn.
• Lý thuyết hình thái có liên hệ chặt chẽ với toán học xây dựng thông qua diễn giải BHK và có thể được kết nối với logic thông qua đẳng cấu Curry-Howard. Một số lý thuyết hình thái còn có mối quan hệ mật thiết với lý thuyết phạm trù.

Các đặc tính khác

Chuẩn hóa

Biểu thức $2+1$ có thể được rút gọn thành $3$. Biểu thức $3$ không thể rút gọn thêm, nó được gọi là 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 biểu thức đều có dạng chuẩn và bất kỳ dãy các phép rút gọn nào cũng dẫn đến dạng chuẩn. Các hệ chuẩn hóa yếu có dạng chuẩn, nhưng 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.

Trong hệ chuẩn hóa, một phần tử là tập hợp các từ có cùng dạng chuẩn. Một từ đóng là một từ không chứa tham số (ví dụ, từ $x+1$ với tham số $x$ là một từ mở). Ví dụ, $2+1$ và $3+0$ là hai từ khác nhau thuộc cùng một phần tử $3$.

Các loại phụ thuộc

Một loại phụ thuộc là loại mà giá trị của nó phụ thuộc vào một từ hoặc loại khác. Chẳng hạn, kiểu trả về của một hàm có thể thay đổi tùy thuộc vào đối số đầu vào của hàm.

Ví dụ, một danh sách $nat$ có độ dài 4 có thể có kiểu khác với một danh sách $nat$ có độ dài 5.

Các loại đẳng thức

Nhiều hệ hình thái có một loại đặc biệt để biểu diễn sự bằng nhau giữ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$. Có một loại $IAab$ với $A$ là một loại và $a$, $b$ là các từ thuộc loại $A$. Một từ thuộc loại $IAab$ biểu thị sự đẳng thức '$a$ bằng $b$'.

Trong thực tế, có thể định nghĩa một loại $Inat34$ nhưng loại này không có từ nào (vì $3$ khác $4$). Trong lý thuyết loại trực giác, chúng ta xây dựng các từ đẳng thức từ các đẳng thức đồng nhất. Nếu $3$ là một từ thuộc loại $nat$, tồn tại một từ thuộc loại $Inat33$. Các đẳng thức phức tạp hơn có thể được tạo ra bằng cách bắt đầu từ một từ đồng nhất và thực hiện các phép rút gọn. Ví dụ, nếu $2+1$ là một từ thuộc loại $nat$, ta có một đẳng thức đồng nhất $Inat(2+1)(2+1)$, và bằng cách rút gọn, ta có một từ mới thuộc loại $Inat(2+1)3$. Như vậy, trong hệ thống này, loại đẳng thức cho thấy rằng hai giá trị cùng loại có thể chuyển đổi bằng cách rút gọn.

Các lý thuyết hình thái

Chính

• 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

Phụ lục

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

Đang trong quá trình nghiên cứu

• Lý thuyết hình thái đồng luân hiện đang được tiếp tục nghiên cứu.

• Bell, John L. (2012). 'Types, Sets and Categories' (PDF). Trong Kanamory, Akihiro (biên tập). 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.

Tài liệu bổ sung

• Aarts, C.; Backhouse, R.; Hoogendijk, P.; Voermans, E.; van der Woude, J. (tháng 12 năm 1992). 'Lý thuyết quan hệ về các kiểu dữ liệu'. Technische Universiteit Eindhoven.
• Andrews B., Peter (2002). Giới thiệu về Logic Toán học và Lý thuyết Loại: Đến Sự Thật Qua Chứng Minh (ấn bản thứ 2). Kluwer. ISBN 978-1-4020-0763-7.
• Đề cập chi tiết về lý thuyết loại, bao gồm các mở rộng loại đa hình và phụ thuộc. Cung cấp ngữ nghĩa phân loại.
• Cardelli, Luca (1996). 'Hệ thống loại'. Trong Tucker, Allen B. (biên tập). Cẩm nang Khoa học Máy tính và Kỹ thuật. CRC Press. tr. 2208–36. ISBN 9780849329098.
• Constable, Robert L. (2012) [2002]. 'Lý thuyết Loại Tính Toán Ngây Thơ' (PDF Lưu trữ 2012-02-27 tại Wayback Machine). Trong Schwichtenberg, H.; Steinbruggen, R. (biên tập). Chứng Minh và Độ Tin Cậy của Hệ Thống. Nato Science Series II. 62. Springer. tr. 213–259. ISBN 9789401004138.
• Coquand, Thierry (2018) [2006]. 'Lý thuyết Loại'. Bách khoa toàn thư Stanford về Triết học.
• Thompson, Simon (1991). Lý thuyết loại và Lập trình hàm. Addison–Wesley.
• Hindley, J. Roger (2008) [1995]. Lý thuyết Loại Cơ Bản. Cambridge University Press.
• Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). Quan điểm hiện đại về lý thuyết loại: từ nguồn gốc đến hiện tại. Springer.
• Ferreirós, José; Domínguez, José Ferreirós (2007). 'X. Logic và Lý thuyết Loại trong thời kỳ giữa hai cuộc chiến'. Labyrinth of thought: một lịch sử của lý thuyết tập hợp và vai trò của nó trong toán học hiện đại (ấn bản thứ 2). Springer.
• Laan, T.D.L. (1997). Sự phát triển của lý thuyết loại trong logic và toán học (PDF) (Luận án Tiến sĩ). Eindhoven University of Technology.

Các liên kết bên ngoài

Tiếng Việt

• Bài viết trên SocialLife.
• Luận văn về tư tưởng Russel, trang 12 có đề cập đến 'lý thuyết hình thái logic'.

Tiếng Anh

• Robert L. Constable (biên tập). 'Lý thuyết loại tính toán'. Scholarpedia.
• Diễn đàn TYPES — diễn đàn qua email được điều hành, tập trung vào lý thuyết loại trong khoa học máy tính, hoạt động từ năm 1987.
• Sách Nuprl: 'Giới thiệu về Lý thuyết Loại.'
• Tài liệu giảng dạy của Dự án Types từ các trường hè 2005–2008
  • Trường hè 2005 có các bài giảng cơ bản