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

Từ VLOS
Bước tới: chuyển hướng, tìm kiếm
Phép-tính lambda là một hệ-thống hình-thức dùng để định-nghĩa hàm, ứng-dụng hàm và đệ-quy được Alonzo Church đề-xuất vào những năm 193x.

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.

Lịch-sử[sửa]

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 đầu-tiên được đề-cử là Plankalkül, do Konrad Zuse thiết-kế vào những năm 194x, 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-hiện cho-đến năm 1998). Ngôn-ngữ lập-trình đầu-tiên được biết-đến rộng-rãi và thành-công là Fortran, được phát-triển 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 của FORTRAN dẫn đến sự-hình-thành của ủy-ban các nhà-khoa-học nhằm phát-triển một ngôn-ngữ máy-tính "thế-giới"; kết-quả cho những cố-gắng của họ là ALGOL 58. Một cách độc-lập, John McCarthy của MIT đã phát-triển ngôn-ngữ lập-trình Lisp (dựa trên phép-tính lambda), ngôn-ngữ đầu-tiên thành-công với các khởi-điểm từ giới-học-viện. Với sự-thành-công của những cố-gắng khởi-nguồn này, các 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 trong những năm 196x 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à các lĩnh-vực liên-quan[sửa]

Có nhiều lĩnh-vực nghiên-cứu hoặc nằm trong lí-thuyết ngôn-ngữ lập-trình, hoặc có ảnh-hưởng sâu-sắc lên nó; nhiều lĩnh-vực 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, bao-gồm lí-thuyết tính-toán, lí-thuyết thể-loại, và lí-thuyết tập-hợp.

Ngữ-nghĩa-học hình-thức[sửa]

Ngữ-nghĩa-học hình-thức là đặc-điểm hình-thức của 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ập đến việc-nghiên-cứu ngôn-ngữ hình-thức.

Lí-thuyết kiểu[sửa]

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à chuyển-đổi[sửa]

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 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).

Phân-tích ngôn-ngữ lập-trình so-sánh[sửa]

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[sửa]

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]

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.

Xây-dựng trình-biên-dịch[sửa]

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-gian-chạy[sửa]

Hệ-thống thời-gian-chạy đề-cập đế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.

Tạp-chí chuyên-ngành, xuất-bản-phẩm và hội-thảo PLT[sửa]

Các tạp-chí xuất-bản nghiên-cứu nguyên-bản trong lí-thuyết 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]

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.

Xem thêm[sửa]

Đọc thêm[sửa]

Liên kết ngoài[sửa]

  • « Mới nhất
  • ‹ Mới hơn
  • Cũ hơn ›
Lấy từ “https://tusach.thuvienkhoahoc.com/index.php?title=Lí_thuyết_ngôn_ngữ_lập_trình&oldid=135573”