Lí·thuyết ngôn·ngữ lập·trình

Người·dịch: Nguyễn·Tiến·Hải

Lí·thuyết ngôn·ngữ lập·trình (tiếng Anh: Programming Language Theory, viết tắt PLT) là một nhánh khoa·học máy·tính. Nhánh này nghiên·cứu nhiều khía·cạnh liên·quan đến các ngôn·ngữ lập·trình và các đặc·trưng của chúng, đó là thiết·kế, thực·hiện, phân·tích, mô·tả đặc·điểm và phân·loại. Nhánh này phụ·thuộc vào toán·học, kĩ·nghệ phần·mềm (software engineering) và ngôn·ngữ·học (linguistics). Nhiều người cho rằng PLT đang là lĩnh·vực nghiên·cứu năng·động vì có nhiều công·trình được xuất·bản ở nhiều tạp·chí chuyên về PLT cũng·như ở các xuất·bản·phẩm về kĩ·thuật và khoa·học máy·tính nói chung. Hầu·hết các chương·trình đào·tạo cử·nhân khoa·học máy·tính đều yêu·cầu sinh·viên phải học các môn·học liên·quan chủ·đề này.

Mục·lục

1. Lịch·sử
2. Các ngành con và lĩnh·vực liên·quan
2.1. Ngữ·nghĩa·học hình·thức (formal semantics)
2.2. Lí·thuyết kiểu (type theory)
2.3. Phân·tích và chuyển·đổi chương·trình
2.4. Phân·tích đối·chiếu ngôn·ngữ lập·trình
2.5. Lập·trình meta (meta programming)
2.6. Ngôn·ngữ đặc·trưng·miền (domain-specific languages)
2.7. Xây·dựng trình·biên·dịch (compiler)
2.8. Hệ·thống thời·gian·chạy (run-time)
3. Tạp·chí chuyên·ngành, xuất·bản·phẩm và hội·thảo về PLT
4. Kí·hiệu Lambda
5. Xem thêm
6. Đọc thêm
7. Liên·kết ngoài

·····································

1. Lịch·sử

Có·thể nói rằng lịch·sử lí·thuyết ngôn·ngữ lập·trình có trước cả sự·phát·triển của chính bản·thân các ngôn·ngữ lập·trình. Phép tính lambda, do Alonzo Church và Stephen Cole Kleene phát·triển vào thập·niên 1930, được một·số người coi là ngôn·ngữ lập·trình đầu·tiên trên thế·giới, mặc·dù lúc đầu người ta chỉ định dùng nó làm mô·hình tính·toán hơn là làm phương·tiện để các lập·trình·viên mô·tả các giải·thuật dành cho các hệ·thống máy·tính. Nhiều ngôn·ngữ lập·trình hàm được mô·tả như là sự dán thêm một "lớp·gỗ·dán mỏng" (thin veneer) vào phép·tính lambda [1]. Hơn nữa, nhiều ngôn·ngữ lập·trình trong số đó có·thể được dễ·dàng mô·tả  bằng các thuật·ngữ của phép·tính lambda.

Ngôn·ngữ lập·trình đầu·tiên từng được đưa ra là Plankalkül. Ngôn·ngữ này do Konrad Zuse thiết·kế vào thập·niên 1940, nhưng công·chúng không biết·đến nó mãi·cho·đến năm 1972 (đến năm 1998 ngôn·ngữ này mới được phát·triển). 

Ngôn·ngữ lập·trình đầu·tiên nổi·tiếng và thành·công nhất phải kể đến FORTRAN. Từ năm 1954 đến năm 1957, John Backus đã dẫn đầu một nhóm các nhà·nghiên·cứu hãng IBM phát·triển nên FORTRAN. Thành·công của FORTRAN dẫn tới sự ra đời của một ủy·ban gồm các nhà·khoa·học với mục·tiêu phát·triển một ngôn·ngữ mới có "tính·chất toàn·cầu" và ALGOL 58 đã ra đời. Trong thời·gian đó John McCarthy từ MIT cũng đã phát·triển LISP dựa trên phép·tính lambda. LISP là ngôn·ngữ đầu·tiên thành·công bắt nguồn từ giới·học·viện (academia). 

Từ những thành·công ban·đầu này, các ngôn·ngữ lập·trình máy·tính trở·thành chủ·đề nghiên·cứu sôi·nổi trong thập·niên 1960 và về sau.

Một·số sự·kiện chính:

Thập·niên 1950, Noam Chomsky phát·triển hệ·thống phân·cấp Chomsky (Chomsky hierarchy) trong lĩnh·vực ngôn·ngữ·học. Đây là khám·phá tác·động trực·tiếp lên lí·thuyết ngôn·ngữ lập·trình và nhiều nhánh khác của khoa·học máy·tính.

Thập·niên 1960, Ole·Johan Dahl và Kristen Nygaard phát·triển ngôn·ngữ Simula. Simula được coi là hình·mẫu đầu·tiên của một ngôn·ngữ lập·trình hướng·đối·tượng; Simula cũng đã giới·thiệu khái·niệm đồng·chương·trình·con (tiếng Anh: coroutine).

Thập·niên 1970:

• Một nhóm các nhà·khoa·học tại Xerox PARC do Alan Kay dẫn·đầu phát·triển Smalltalk, một ngôn·ngữ hướng·đối·tượng nổi·tiếng nhờ môi·trường phát·triển sáng·tạo của nó.
• Sussman và Steele phát·triển ngôn·ngữ lập·trình Scheme, một phiên·bản của Lisp hợp·nhất phạm·vi từ·vựng (tiếng Anh: lexical scoping) với một namespace (không·gian·tên) thống·nhất và các yếu·tố từ mô·hình Actor (bao·gồm các continuation lớp·nhất).
  Lập·trình logic và Prolog phát·triển cho·phép các chương·trình máy·tính được biểu·hiện như logic toán·học.
• Backus, năm 1977, trong một bài·giảng tại ACM Turing Award , đã đả·kích hiện·trạng của các ngôn·ngữ công·nghiệp lúc bấy·giờ. Backus đề·xuất một lớp mới các ngôn·ngữ lập·trình, chính là các ngôn·ngữ lập·trình mức hàm hiện nay.
• Xuất·hiện phép·tính tiến·trình, ví·dụ như Phép·tính của các Hệ·thống Giao·tiếp (Calculus of Communicating Systems) của Robin Milner, và mô·hình Các tiến·trình giao·tiếp liên·tục (Communicating sequential processes) của C. A. R. Hoare, cũng như các mô·hình song·song tương·tự, ví·dụ như mô·hình Actor của Carl Hewitt.
• Lí·thuyết kiểu bắt·đầu được áp·dụng với tư·cách một ngành·học (tiếng Anh: discipline) cho các ngôn·ngữ lập·trình, nhờ công đầu của  Milner; ứng·dụng này dẫn đến những tiến·bộ to·lớn trong lí·thuyết kiểu suốt nhiều năm qua.

Thập·niên 1980:
Bertrand Meyer tạo·ra phương·pháp·học Thiết·kế theo hợp·đồng (Design by contract) và hợp·nhất nó vào ngôn·ngữ lập·trình Eiffel.

Thập·niên 1990:
Gregor Kiczales, Jim Des Rivieres và Daniel G. Bobrow xuất·bản cuốn·sách Nghệ·thuật của Giao·thức Đối·tượng·meta (tựa tiếng Anh: The Art of the Metaobject Protocol).
Philip Wadler đề·xuất dùng các monad cho việc·cấu·trúc các chương·trình viết bằng các ngôn·ngữ lập·trình hàm.

2. Các ngành con và lĩnh·vực liên·quan
Có nhiều lĩnh·vực nghiên·cứu hoặc nằm trong hoặc có ảnh·hưởng sâu·sắc lên lí·thuyết ngôn·ngữ lập·trình; nhiều lĩnh·vực trong số này có sự·chồng·chéo đáng·kể. PLT còn sử·dụng nhiều nhánh khác của toán·học, gồm lí·thuyết tính·toán, lí·thuyết thể·loại, và lí·thuyết tập·hợp.

2. 1. Ngữ·nghĩa·học hình·thức (formal semantics)
Ngữ·nghĩa·học hình·thức là đặc·trưng có tính hình·thức về hành·vi của các chương·trình máy·tính và các ngôn·ngữ lập·trình, có liên·quan đến việc·nghiên·cứu ngôn·ngữ hình·thức. Có ba phương·pháp miêu·tả ngữ·nghĩa·học hay "ý·nghĩa" của một chương·trình máy·tính đó là: ngữ·nghĩa·học biểu·diễn (denotational semantics), ngữ·nghĩa·học thao·tác (operational semantics) và ngữ·nghĩa·học tiên·đề (axiomatic semantics).

2. 2. Lí·thuyết kiểu (type theory)
Lí·thuyết kiểu là sự·nghiên·cứu các hệ·thống kiểu, "là các phương·pháp cú·pháp dễ·kiểm·soát nhằm chứng·minh sự·vắng·mặt của các hành·vi chương·trình nào·đó bằng·cách phân·loại các ngữ tuân·theo các loại giá·trị mà chúng tính được." (theo Các kiểu và các Ngôn·ngữ lập·trình, tiếng Anh: Types and Programming Languages, MIT Press, 2002). Nhiều ngôn·ngữ lập·trình được phân·biệt nhờ các đặc·điểm của các hệ·thống kiểu.

2. 3. Phân·tích và chuyển·đổi chương·trình 
Chuyển·đổi chương·trình là quá·trình chuyển·đổi một chương·trình từ dạng (ngôn·ngữ) này sang dạng (ngôn·ngữ) khác; phân·tích chương·trình là vấn·đề toàn·cục của việc·khảo·sát một chương·trình và xác·định các đặc·điểm mấu·chốt (như sự·vắng·mặt các lớp lỗi chương·trình).

2. 4. Phân·tích đối·chiếu ngôn·ngữ lập·trình 
Phân·tích đối·chiếu ngôn·ngữ lập·trình tìm·cách phân·chia ngôn·ngữ lập·trình thành các loại khác·nhau dựa trên đặc·điểm của chúng; thể·loại rộng của ngôn·ngữ lập·trình thường được gọi là mô·hình lập·trình.

2. 5. Lập·trình·meta
Lập·trình·meta là sự·phát·sinh chương·trình có bậc cao hơn, khi thực·hiện chương·trình đó sẽ sinh ra một chương·trình khác (có·thể trong ngôn·ngữ khác, hoặc trong một tập·hợp·con của ngôn·ngữ gốc).

2. 6. Ngôn·ngữ đặc·trưng·miền (domain-specific languages)
Ngôn·ngữ đặc·trưng·miền là ngôn·ngữ được xây·dựng để giải·quyết các vấn·đề một·cách hiệu·quả trong một miền vấn·đề riêng.

2. 7. Xây·dựng trình·biên·dịch (compiler)
Lí·thuyết Trình·biên·dịch là lí·thuyết viết các trình·biên·dịch (compiler) (hoặc tổng·quát hơn, máy·dịch (translator)). Trình·biên·dịch là một chương·trình dùng để dịch các chương·trình khác được viết trong một ngôn·ngữ sang dạng khác. Các hành·động của một trình·biên·dịch theo·truyền·thống được chia·nhỏ thành phân·tích cú·pháp (quét (scan) và phân·tích từ·loại (parse)), phân tích ngữ·nghĩa (xác·định chương·trình nên làm gì), tối·ưu·hóa (cải·tiến hiệu·suất của chương·trình theo các chỉ·số, điển·hình là tốc·độ thực·hiện) và Phát·sinh mã (Phát·sinh và xuất một chương·trình tương·đương trong ngôn·ngữ đích nào·đó; thường là tập·hợp lệnh của một CPU).

2. 8. Hệ·thống thời·gian·chạy (run-time)
Hệ·thống thời·gian·chạy nói đến việc·phát·triển các môi·trường thời·gian·chạy ngôn·ngữ lập·trình và các thành·phần của chúng, bao·gồm các máy ảo, thu·thập dữ·liệu·rác, và các giao·diện ngoại·hàm.

3. Tạp·chí chuyên·ngành, xuất·bản·phẩm và hội·thảo về PLT
Các tạp·chí chuyên·ngành lí·thuyết ngôn·ngữ lập·trình đáng chú·ý gồm có:

• ACM Transactions on Programming Languages and Systems (Giao·dịch ACM trên các Ngôn·ngữ Lập·trình và các Hệ·thống)
• 
  
• Computer Languages, Systems, and Structures (Các ngôn·ngữ máy·tính, Các hệ·thống, và các Cấu·trúc)


• Journal of Functional Programming (Tạp·chí Lập·trình hàm)


• Journal of Functional and Logic Programming (Tạp·chí Lập·trình Logic và Hàm)


• Journal of Symbolic Computation (Tạp·chí Tính·toán kí·hiệu)

Các bài·báo PLT về các cú·hích quan·trọng hoặc về sự·quan·tâm tổng·quát hơn có·thể xuất·hiện trong các tạp·chí bách·khoa hơn như Tạp·chí ACM (Journal of the ACM), Thông·tin và Tính·toán (Information and Computation), hay Khoa·học Máy·tính Lí·thuyết, (Theoretical Computer Science). Xem thêm danh·sách các xuất·bản·phẩm trong khoa·học máy·tính.

Cũng·như nhiều lĩnh·vực Khoa·học Máy·tính khác, các cuộc·hội·thảo đóng vai·trò quan·trọng, đôi·khi là vai·trò lãnh·đạo. Các cuộc·hội·thảo nổi·tiếng nhất trong PLT có·lẽ là Hội·nghị·chuyên·đề về các Nguyên·lí của các Ngôn·ngữ Lập·trình (tiếng Anh: Symposium on Principles of Programming Languages) (POPL)) và Hội·thảo Quốc·tế về Lập·trình Hàm (tiếng Anh: International Conference on Functional Programming (ICFP)). Các cuộc·hội·thảo khác có ảnh·hưởng liên·quan PLT gồm Hội·thảo về Thiết·kế và Thực·hiện Ngôn·ngữ Lập·trình (Conference on Programming Language Design and Implementation (PLDI)) và Hội·nghị Quốc·tế về Lập·trình Hướng·đối·tượng, về các Hệ·thống, các Ngôn·ngữ và các Ứng·dụng (tiếng Anh: International Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA)).

4. Kí·hiệu Lambda

Một biểu·tượng không chính·thức của lĩnh·vực lí·thuyết ngôn·ngữ lập·trình là chữ·cái Hi·Lạp viết·thường λ (lambda). Cách dùng này bắt·nguồn từ phép·tính lambda, một mô·hình tính·toán được các nhà·nghiên·cứu ngôn·ngữ lập·trình sử·dụng rộng·rãi. Nhiều văn·bản, bài·báo về lập·trình và các ngôn·ngữ lập·trình đã từng sử·dụng lambda theo một phong·cách nào đó. Nó đã làm·vẻ·vang trang·bìa của văn·bản cổ·điển có tên Cấu trúc và Thuyết·minh các Chương·trình Máy·tính (Structure and Interpretation of Computer Programs), và tiêu·đề của nhiều cái gọi là các bài·báo Lambda (Lambda Papers), do Gerald Jay Sussman và Guy Steele, các nhà·phát·triển của Ngôn·ngữ lập·trình Scheme., viết. Một website nổi·tiếng về lí·thuyết ngôn·ngữ lập·trình là Lambda the Ultimate, nhằm vinh·danh công·trình của Sussman và Steele.

5. Xem thêm

• SIGPLAN
• Thời·gian·biểu của các ngôn·ngữ lập·trình
• Ngôn·ngữ lập·trình bậc rất cao

6. Đọc thêm

• Mitchell, John C.. Foundations for Programming Languages.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.
• Pierce, Benjamin C. Advanced Topics in Types and Programming Languages.
• Pierce, Benjamin C. et al. (2010). Software Foundations.
• Programming Language Pragmatics, 2nd Edition by Michael Scott (Morgan·Kaufmann, 2006)
• Essentials of Programming Languages by Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes (MIT Press 2001)

7. Liên·kết ngoài

• Lambda the Ultimate, một weblog cộng·đồng dành·cho thảo·luận chuyên·nghiệp và kho·lưu·trữ tài·liệu về lí·thuyết ngôn·ngữ lập·trình.
• Lịch·sử ngôn·ngữ máy·tính
• Các sách lí·thuyết lập·trình miễn·phí
• Lịch·sử Haskell

Ngày viết bài: 13 tháng 12 năm 2010

Bài dịch từ wikipedia tiếng Anh http://en.wikipedia.org/wiki/Programming_language_theory