Lý thuyết ngôn ngữ lập trình – Wikipedia tiếng Việt

Lý thuyết ngôn ngữ lập trình (thường được biết tới bởi chữ viết tắt tiếng Anh PLT (Programming language theory) là một nhánh của khoa học máy tính nghiên cứu việc thiết kế, thực hiện, phân tích, mô tả đặc điểm, và phân loại các ngôn ngữ lập trình và các đặc trưng của chúng. Lý thuyết ngôn ngữ lập trình phụ thuộc và chịu ảnh hưởng của toán học, kĩ nghệ phần mềm và ngôn ngữ học. Nó là một nhánh của khoa học máy tính được công nhận và là một khu vực nghiên cứu tích cực, với các kết quả được xuất bản trong nhiều tạp chí dành riêng cho PLT, cũng như trong các xuất bản phẩm kĩ thuật và khoa học máy tính chung. Hầu hết các chương trình đào tạo cử nhân khoa học máy tính yêu cầu phải học các môn học trong chủ đề này.

Trong một số cách, 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 các ngôn ngữ lập trình. Phép tính lambda, được phát triển bởi Alonzo Church và Stephen Cole Kleene trong những năm 193x, được một số người coi là ngôn ngữ lập trình đầu tiên của thế giới, mặc dù nó từng được dự định dùng làm mô hình tính toán hơn là phương tiện cho các lập trình viên mô tả các giải thuật cho một hệ thống máy tính. Nhiều ngôn ngữ lập trình hàm được mô tả như sự cung cấp một “lớp gỗ dán mỏng” lên phép tính lambda [1], và nhiều trong số đó dễ dàng được mô tả bằng những thuật ngữ của phép tính lambda.

Ngôn ngữ lập trình tiên phong được đề cử là Plankalkül, do Konrad Zuse phong cách thiết kế vào những năm 194 x, nhưng không được công chúng biết đến mãi cho đến năm 1972 ( và không được thực thi cho đến năm 1998 ). Ngôn ngữ lập trình tiên phong được biết đến thoáng đãng và thành công xuất sắc là Fortran, được tăng trưởng từ năm 1954 đến năm 1957 bởi một nhóm nhà nghiên cứu IBM được dẫn dắt bởi John Backus. Sự thành công xuất sắc của FORTRAN dẫn đến sự hình thành của ủy ban những nhà khoa học nhằm mục đích tăng trưởng một ngôn ngữ máy tính ” quốc tế ” ; tác dụng cho những nỗ lực của họ là ALGOL 58. Một cách độc lập, John McCarthy của MIT đã tăng trưởng ngôn ngữ lập trình Lisp ( dựa trên phép tính lambda ), ngôn ngữ tiên phong thành công xuất sắc với những khởi điểm từ giới học viện chuyên nghành. Với sự thành công xuất sắc của những nỗ lực khởi nguồn này, những ngôn ngữ lập trình máy tính đã trở thành một chủ đề tích cực của việc nghiên cứu và điều tra trong những năm 196 x và về sau .

Một số sự kiện chủ chốt trong lịch sử của lý thuyết ngôn ngữ lập trình kể từ lúc đó:

Các môn con và những nghành tương quan[sửa|sửa mã nguồn]

Có nhiều nghành nghiên cứu và điều tra hoặc nằm trong triết lý ngôn ngữ lập trình, hoặc có ảnh hưởng tác động thâm thúy lên nó ; nhiều nghành trong số này có sự chồng chéo đáng kể. Thêm vào đó, PLT sử dụng nhiều nhánh khác của toán học, gồm có kim chỉ nan giám sát, kim chỉ nan thể loại, và kim chỉ nan tập hợp .

Ngữ nghĩa học hình thức[sửa|sửa mã nguồn]

Ngữ nghĩa học hình thức là đặc thù hình thức của hành vi của những chương trình máy tính và những ngôn ngữ lập trình, đề cập đến việc nghiên cứu và điều tra ngôn ngữ hình thức .

Lý thuyết kiểu[sửa|sửa mã nguồn]

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 bằng các đặc điểm của các hệ thống kiểu.

Phân tích chương trình và quy đổi[sửa|sửa mã nguồn]

Chuyển đổi chương trình là quy trình quy đổi một chương trình từ dạng ( ngôn ngữ ) này sang dạng khác ; nghiên cứu và phân tích chương trình là yếu tố toàn cục của việc khảo sát một chương trình và xác lập những đặc thù mấu chốt ( như sự vắng mặt những lớp lỗi chương trình ) .

Phân tích ngôn ngữ lập trình so sánh[sửa|sửa mã nguồn]

Phân tích ngôn ngữ lập trình so sánh tìm cách phân loại các ngôn ngữ lập trình thành các loại khác nhau dựa trên các đặc điểm của chúng; các thể loại rộng của các ngôn ngữ lập trình thường được biết đến như là các mô hình lập trình.

Lập trình meta là sự phát sinh chương trình bậc cao hơn, mà kết quả sinh ra khi thực hiện chương trình đó là 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).

Ngôn ngữ đặc trưng miền[sửa|sửa mã nguồn]

Ngôn ngữ đặc trưng miền là ngôn ngữ được thiết kế xây dựng để xử lý những yếu tố một cách hiệu suất cao trong một miền yếu tố riêng .

Xây dựng trình biên dịch[sửa|sửa mã nguồn]

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)) chương trình dịch chương trình đượ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).

Hệ thống thời hạn chạy[sửa|sửa mã nguồn]

Hệ thống thời hạn chạy đề cập đến việc tăng trưởng những thiên nhiên và môi trường thời hạn chạy ngôn ngữ lập trình và những thành phần của chúng, gồm có những máy ảo, thu thập dữ liệu rác, và những giao diện ngoại hàm .

Tạp chí chuyên ngành, xuất bản phẩm và hội thảo chiến lược PLT[sửa|sửa mã nguồn]

Các tạp chí xuất bản nghiên cứu và điều tra nguyên bản trong triết lý ngôn ngữ lập trình gồm :

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í của 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ư trong nhiều lĩnh vực của Khoa học Máy tính, các cuộc hội thảo đóng vai trò quan trọng, đôi khi là lãnh đạo. Có lẽ các cuộc hội thảo nổi tiếng nhất trong PLT 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, 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)).

Ký hiệu Lambda

[sửa|sửa mã nguồn]

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 sử dụng rộng rãi bởi các nhà nghiên cứu ngôn ngữ lập trình. 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 sử dụng lambda theo mốt nào đó. Nó làm vẻ vang trang bìa của văn bản cổ điể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), được viết bởi Gerald Jay Sussman và Guy Steele, các nhà phát triển của Ngôn ngữ lập trình Scheme. Một trang mạng nổi tiếng về lý thuyết ngôn ngữ lập trình được gọi là Lambda the Ultimate nhằm vinh danh công trình của Sussman và Steele.

Liên kết ngoài[sửa|sửa mã nguồn]